Repository navigation
PVL: prove all 7 escape-allowlist axioms (DPO x3, f16 bound, NF4 x3) instead of confirming them #4347
Closed as not planned
Description
Operator, verbatim, 2026-09-25: "why not prove all"
crates/aprender-contracts-staging/lean/escape-allowlist.yaml (B3 #4317) holds 7 confirmed_by: pending axioms. pv discharge check --strict (EV-9) stays RED until each one is confirmed or removed. This ticket removes them by proof.
| decl | plan |
|---|---|
| DPO.sigmoid_bounded | prove from Real.exp_pos |
| NF4.nf4_lut | replace the axiom with a concrete def holding the 16 bitsandbytes constants (as rationals of the published f32 literals) |
| NF4.nf4_lut_monotone / nf4_lut_bounded | prove by decide/norm_num over the concrete table (their "Status: proved" comments are false today) |
| DPO.dpo_gradient_formula | prove with Mathlib HasDerivAt |
| DPO.dpo_loss_zero_at_strong_preference | prove with Mathlib Tendsto |
| CooperativeMatrix.f16_accumulation_error_bound | prove under the standard rounding model |
Done when:
- The allowlist holds at most 1 entry (the rounding model).
pv discharge check --strictis green, or red only on that 1 entry.- The proofs pass the leanchecker re-check.
Base: B3 (the file exists only there). It lands after #4317 merges, the same way as #4244.
Folded sub-tickets (TRIAGE-100, 2026-10-14)
These open sub-tickets were folded here as checklist rows and closed as not planned so the open count stays at or under 100. Reopen one when its work resumes; an open PR for it reopens it.
- PVL-001 EV-9 — PVL-9: provable-ladder required on main #4083 — PVL-001 EV-9 — PVL-9: provable-ladder required on main (branch:
52/4083-ladder-fanin,a2/4083-ev9-one-owner) - PVL-001 EV-6c — PVL-6c: Kani assume baseline #4197 — PVL-001 EV-6c — PVL-6c: Kani assume baseline (branch:
0d/4197-ev6c-pt2,a01/070-4197-ev6c)
Activity
test(pvl): the real-tree probe pins PENDING (3) -- #4347 discharged N…
Merge remote-tracking branch 'origin/fix/4347-prove-nf4-f16' into GH-…
Merge fix/4347-prove-nf4-f16 (guard self-exclusion, #4348) into GH-4347…
Merge fix/4347-prove-nf4-f16 (leanchecker caps are ceilings, #4348) i…
fold(B3): #4347 NF4+f16+DPO proofs, #4348 leanchecker caps, #4244 orp…
ont10 (ii) staged: move 26 of the 27 bound modules out of the root im…
fix(#4502): allowlist the 54 ruling-(ii) Lean orphans; check_lean_mod…
fix(#4502): allowlist the 54 ruling-(ii) Lean orphans; check_lean_mod…
fix(#4502): delete the dead cooperative-matrix GEMM chain (#4347)
fix(split): move 29 contracts whose tests or bins live in PR-2 out of…
2 remaining items
noahgift commentedon Oct 14, 2026
Status of the 7 axioms, read on
main@8c3b19c8c1(2026-10-14).6 of 7 are proved on
main.DPO.leanholdssigmoid_bounded,dpo_loss_zero_at_strong_preferenceanddpo_gradient_formulaas theorems.Quantization/NF4Dequant.leandefinesnf4_lutas a concrete table, andnf4_lut_monotoneandnf4_lut_boundedare theorems.escape-allowlist.yamlhas 0 entries.pv discharge check --strict --no-lakeexits 0.The 7th was removed, not proved.
f16_accumulation_error_boundwas inMatMul/CooperativeTiling.lean. That file was deleted with the dead cooperative-matrix GEMM chain (601334e, folded in #4655). The kernel had never been compiled, and the rest of the file proved onlyrfltautologies. The proofs that replaced the axiom never reachedmain.Restore: branch
fix/4347-f16-rounding-model@48f049edb8, no PR yet.Theorems/F16/RoundingModel.leanwith the four lemmas, unchanged:RoundingModel, a hypothesis and never an axiom;roundingModel_id, which shows the hypothesis is satisfiable;rounded_product_error;f16_input_rounding_error_bound.pv discharge check --strict --no-lakeexits 0.lake buildand leanchecker on this branch.This lane does not close the issue.
🤖 Generated with Claude Code
noahgift commentedon Oct 14, 2026
Merged into #5308 (TRIAGE-100, 2026-10-14): same theme, so this master's scope and every checklist row now live on #5308, and this ticket is closed as not planned. Reopen it if the theme splits again.
Agent: aprender-clerk