v3.3.28: L4 torsion reduction chain formalization

[gift-framework]

Fill two gaps in the Lean certificate chain connecting the explicit metric to G₂ holonomy:

1. NK parameter decomposition: β (0.02962), η (3.16e-5), ω (0.0713) with product formula verification h = β·η·ω < 1/2

2. Joyce iteration table: T₁-T₄ intermediate values with full monotone convergence proof T₀ > T₁ > T₂ > T₃ > T₄ > T₅

Two convergence regimes identified:

• Steps 0→2: modest linear-like reduction (T₀/T₂ > 2)
• Steps 3→5: dramatic quadratic acceleration (T₂/T₅ > 1000)

14 new definitions, ~20 new theorems, 0 new axioms. NK master: 7→11 conjuncts. K3 master: 10→16 conjuncts. Certificate/Foundations: 26→28 conjuncts.
Build: 2657/2657, zero errors.

---

Note

Medium Risk
Touches core certificate propositions/structures and adds new exported symbols, which may break downstream proofs/imports if they depended on prior certificate shapes. Proofs remain native_decide-backed and no new axioms are introduced, limiting correctness risk.

Overview
Adds L4 torsion reduction chain formalization by filling two missing proof links in the Lean certificate path.

Foundations/NewtonKantorovich.lean now exposes separate β/η/ω rational bounds, proves their product implies the existing h < 1/2 contraction, extends NKCertificate with these fields, and expands the NK master certificate (7→11 conjuncts). Foundations/K3HarmonicCorrection.lean adds intermediate torsion bounds T1–T4, proves the full monotone chain T0 > … > T5, and adds regime/acceleration checks, expanding the K3 master certificate (10→16).

Wires these into the public surface by extending exports in Foundations.lean, adding new abbrevs and two new conjuncts in Certificate/Foundations.lean (26→28), and bumps docs/versioning (CHANGELOG, docs/USAGE.md, README, gift_core/_version.py) to 3.3.28.

^{Written by Cursor Bugbot for commit 52f917c. This will update automatically on new commits. Configure here.}