nkWitnessCheck uses the kernel-reducible Hex.Dyadic.invFloor (one integer division) where the SPEC's completeness contract 1 − w·c₁ ∈ [0, 2⁻⁸) is stated through floor-rounding bounds. The companion's cited lemmas (Dyadic.invAtPrec_mul_le_one, Dyadic.one_lt_invAtPrec_add_inc_mul) are about invAtPrec. Commit either Dyadic.invFloor_eq_invAtPrec_of_pos or a direct floor contract for invFloor when the Newton-Kantorovich completeness item is picked up. Deferrable: soundness does not depend on the quality of w.
🤖 Prepared with Claude Code
nkWitnessCheckuses the kernel-reducibleHex.Dyadic.invFloor(one integer division) where the SPEC's completeness contract1 − w·c₁ ∈ [0, 2⁻⁸)is stated through floor-rounding bounds. The companion's cited lemmas (Dyadic.invAtPrec_mul_le_one,Dyadic.one_lt_invAtPrec_add_inc_mul) are aboutinvAtPrec. Commit eitherDyadic.invFloor_eq_invAtPrec_of_posor a direct floor contract forinvFloorwhen the Newton-Kantorovich completeness item is picked up. Deferrable: soundness does not depend on the quality ofw.🤖 Prepared with Claude Code