GIFT core 3.4.28

b₂-side rigidity companion to realises_iff_cocycleDim_77 in the Donaldson link-cohomology module.

The module already characterised b₃ = 77 purely by the discriminant link's cocycle dimension (realises_iff_cocycleDim_77), while b₂ = 21 entered only as the bare definition b2Donaldson := 21 (cited to Donaldson 2017 §4.1). This release adds the matching b₂ characterisation: for a reflection monodromy with vanishing-cycle span of rank spanRank in the rank-22 K3 lattice, b₂ = 22 − spanRank, and b₂ = 21 ↔ spanRank = 1 — i.e. the value b₂ = 21 forces uniform monodromy (a single reflection ρ = s_{α₁}), it does not merely assume it. Together the two theorems show the two Betti numbers are governed by independent data (b₂ by the span rank, b₃ by the link cocycle dimension).

Added to GIFT/Foundations/G2DonaldsonLinkCohomology.lean: b2FromSpanRank, b2FromSpanRank_uniform, b2_eq_21_iff_uniform_monodromy (the rigidity bi-conditional, by omega), b2_nonuniform_ne_21.

No new axioms (15), zero sorry, no behavioural change. The geometric identity dim Fix = 22 − rank(span) remains a definition (research-level lattice/reflection formalisation, not attempted here); the arithmetic consequence is certified on top of it.

GIFT core 3.4.27

[3.4.27] - 2026-06-17
Summary

K3 explicit-model module removed from public package; Koide R1c machine-falsified; observables.json reconciliation; doc cleanups. No new axioms, no behavioural change in the certificate. The release consolidates research-only code into the canonical workspace and records the new Koide assembly certificate.
Removed (public API)

gift_core.geometry.k3_explicit (18 451 lines) — direct Donaldson-metric computation for the K3 quartic. Research-only, not part of the certified exports. Moved to canonical workspace.
gift_core.examples.verify_phase_a1_explicit_k3 / verify_phase_a2_route — sibling verification drivers. Moved alongside.
contrib/docs/PHASE_A_2_MODEL_B_ROUTE.md — companion design note.

Added

GIFT/Relations/KoideAssembly.lean — 12 theorems, 0 sorry. Assembles Q_Koide from the certified GIFT mass formulas (27^φ, 3477), proves the algebraic reduction Q < 2/3 ⟺ a²+b²+1 < 4a+4b+4ab, an enclosure 0.665 < Q_gift < 0.668, and the strict koideQ_gift < 2/3 via a transcendental chain (Taylor degree-6 → log3 > 1.0986 → 27^φ > 206.9 → nlinarith). Side-quest R1c (Koide-from-masses) machine-falsified.
contrib/dev_history.md — archived per-version sprint logs (v3.0–v3.3.32) extracted from contrib/CLAUDE.md.

Changed

contrib/CLAUDE.md reduced to current conventions only (1 393 lines → ~180); historical content preserved verbatim in dev_history.md.
GIFT.lean header comment: version 3.4.12 → 3.4.27, axiom/relation counts refreshed.
GIFT/Relations/LeptonSector.lean, GIFT/Foundations/GoldenRatioPowers.lean, GIFT/Hierarchy/AbsoluteMasses.lean — fix 27^φ ≈ 206.77 (experimental value mislabelled as prediction) → ≈ 207.01 (actual GIFT prediction).
GIFT/Spectral/ComputedWeylLaw.lean — drop internal "P3 target" jargon.
observables.json (in private/): six exp-target reconciliations to primary sources (sin²θ₁₃ NuFIT 6.1, σ₈ Planck VI, A_Wolf PDG main fit, m_W/m_Z, m_s/m_d band, m_c/m_s scale-consistent). Type-I headline 0.92% → 0.99%, global 1.24% → 1.28%. gift_value + Lean/giftpy unchanged (no exp values are used in any proof).
Homepage / docs headline numbers refreshed to canonical (NuFIT 6.1, v3.4.27, Arithmon-program banner).

Stats

lake build: 8 392 / 8 392, exit 0
Sorry: 0
Axioms: 15 across 4 files (4 prediction-chain + 11 K3 interval-cert) — unchanged
.lean files: 144 (143 + 1 new KoideAssembly)
Lean toolchain: leanprover/lean4:v4.29.0

GIFT core 3.4.26

Removal of competing post-hoc expressions for κ_T⁻¹ = 61.

The torsion coupling κ_T⁻¹ is now carried by its single canonical topological definition κ_T⁻¹ = b₃ − dim(G₂) − p₂ = 77 − 14 − 2 = 61, already used by the master certificate. Three modules offering alternative numerology-style derivations of the same integer (base-13 / Structure A/B / T_61) are deleted. No mathematical change to any prediction, no behavioural change, no new axioms — the master certificate certified (56 conjuncts) is unchanged.

• Removed YukawaDuality.lean, BaseDecomposition.lean, MassFactorization.lean.
• ExceptionalChain.lean: m_τ/m_e relations now reference Core.kappa_T_den (same value, same native_decide).
• Predictions.lean / GIFT.lean: dropped the three imports/abbrevs (none were part of certified).
• lake build: 8391/8391, 0 sorry, 15 axioms across 4 files (unchanged), 143 .lean files.

Full changelog: contrib/CHANGELOG.md

GIFT core 3.4.25

Academic-terminology cleanup follow-up. Completes the v3.4.24 purge of internal planning labels. No mathematical change, no behavioural change — no change to any theorem, definition, axiom, or proof.

• GIFT/Foundations.lean: three import comments still carried (Plan A / Plan A P0 / Plan A P1 2026-05-30) tags next to the K3ClosedFormWitness, K3ClosedFormBoxEnclosures and K3KrawczykContainment imports. The planning tags are removed; the mathematical descriptions (box-local at r=10⁻⁸, ε₃' = 1321/10⁷, trust-boundary narrowing, 28000 strict integer inequalities) are kept.

Verification: lake build GIFT.Foundations → 2535/2535, 0 sorry, axiom set unchanged. Blueprint sync: 314/314 decls, 0 errors.

GIFT core 3.4.24

[3.4.24] - 2026-06-01
Summary

Academic-terminology cleanup of the K3 closed-form witness modules. No mathematical change, no behavioural change. Internal planning labels ("Plan A", "P0", "P1", "bulletproof", IA-review references) are removed from module docstrings and from one theorem name, so that what ships through lean --doc / doc-gen is purely the mathematical content.

K3ClosedFormWitness.lean : header docstring rewritten (no more "Phase D.9b / completeness item II.1", "Plan A box-local (2026-05-30)", "IA-review-1", "P0 (2026-05-30, 'bulletproof')", "Trust boundary after P0") ; inline docstrings on eps3_num, cy_order3_safety_margin_sharp, k3_closed_form_witness cleaned ; status string rewritten. Theorem rename: eps3_agrees_with_p0_envelope → eps3_agrees_with_variance_envelope (same statement, same rfl proof).
K3ClosedFormBoxEnclosures.lean : header docstring and the variance_envelope_bound theorem docstring cleaned.
K3KrawczykContainment.lean : header docstring and the krawczyk_containment_all theorem docstring cleaned.

lake build GIFT.Foundations: 2535/2535, 0 sorry, 0 added axiom.

GIFT core 3.4.23

[3.4.23] - 2026-05-19
Summary

Closed-form K3 CY-residual witness — interval-certified, δ forfait eliminated.

Adds GIFT/Foundations/K3ClosedFormWitness.lean (wired in GIFT/Foundations.lean): a native_decide certificate that the explicit 667-parameter closed-form Kähler metric on the Z₂³-equivariant K3 (D.9b order-3, completeness item II.1) has a certified residual

Var(log R) ≤ ε₃ = 1309 / 10⁷ ≈ 1.309·10⁻⁴ < 10⁻³

on the frozen seed-fixed 4000-point test sample (safety ×7.6), with the order-2 truncation ε₂ ≈ 0.384 showing φ₃ is structurally essential.

cy_order3_below_target, cy_order3_margin, cy_order3_safety_margin (+ sharp ×7.6), cy_order3_tighter_than_order2, cy_order2_trunc_far_above_target, fwd_inflation_below_residual.
ClosedFormCertificate structure + k3_closed_form_witness_certificate master (all native_decide).
Provenance upgrade: the bound is now interval-rigorous with the NS-1b forfait δ = 10⁻⁹ eliminated — the per-point detGᵢ/|Ω|²ᵢ are forward-interval-certified on Krawczyk-certified exact K3 points (full N=4000 run; the δ-free bound is bit-identical to NS-1b). The remaining whole-K3 global bound is mapped, off the critical path.

lake build GIFT.Foundations: 2532 jobs, 0 sorry, 0 added axiom.

v3.4.22 — Donaldson discriminant-family characterisation

[3.4.22] - 2026-05-18

Summary

Donaldson discriminant-family characterisation — general LinkType theorem.

Extends GIFT/Foundations/G2DonaldsonLinkCohomology.lean with the
discriminant-family characterisation: a discriminant link L realises the
GIFT target $(b_2, b_3) = (21, 77)$ iff $\mathrm{cocycleDim}(L) = 77$
(equivalently $b_1(\Sigma_2(L)) = 76$).

• realisesTarget : LinkType → Bool (decide-based).
• realises_iff_cocycleDim_77 — the general equivalence over all
  LinkType, proved by omega (not native_decide): LinkType is
  infinite, so this is a genuine universally-quantified statement, not a
  finite check. This characterises the complete admissible family and
  subsumes any explicit unlink-plus-units parametrisation.
• Family witnesses (native_decide): 77-unlink; 75-unlink ⊔ Hopf ⊔
  trefoil; 74-unlink ⊔ Hopf ⊔ Hopf ⊔ trefoil. Off-family: 76-unlink and
  77-unlink ⊔ Hopf.
• Aggregate realisesTargetCharacterisation discharged by native_decide.

The underlying Leray / double-branched-cover derivation remains a
definition (research-level Mathlib formalisation, explicitly not
attempted); this section certifies the combinatorial characterisation on
top of it. lake build GIFT.Foundations: 2531 jobs, 0 sorry, 0 added
axiom.

v3.4.21 — K3 Z₂³-isotype Lefschetz certificate

[3.4.21] - 2026-05-17

Summary

K3 $\mathbb{Z}_2^3$-isotype Lefschetz certificate — $H^2(K3)=22$ decomposition machine-checked.

New module GIFT/Foundations/K3IsotypeLefschetzCertificate.lean formalises,
as pure Int arithmetic verified by native_decide, the topological-Lefschetz
$\mathbb{Z}_2^3$-isotype decomposition of $H^2(K3)$ for the equivariant K3
surface $\widetilde X = V(Q_1,Q_2,Q_3)\subset\mathbb{P}^5$.

• Fixed-locus Euler characteristics via complete-intersection adjunction:
  genus-5 curves ($|S|\in{1,5}$, $\chi=-8$), 8 points ($|S|\in{2,4}$,
  $\chi=8$), empty ($|S|=3$), the K3 itself ($\chi=24$).
• Trace identity $\mathrm{tr}(g\mid H^2)=\chi(\mathrm{Fix},g)-2 =
  [22,-10,6,6,-2,-2,6,-10]$.
• The eight character multiplicities $[2,8,2,2,2,2,0,4]$ (sum $22$),
  self-dual count $3$ ($\omega_I\in\chi_{000}$, $\omega_J,\omega_K\in\chi_{100}$),
  anti-self-dual profile $[1,6,2,2,2,2,0,4]$ (sum $19$),
  and $\dim H^2(K3)^{V_4}=m_{000}+m_{100}=10$.
• Composite Boolean k3IsotypeLefschetzCertificate discharged by
  native_decide. Independently re-verified by an external formal-reasoning
  audit. Wired into Foundations.lean after G2IrrepLatticeCertificate.

The rank-15 Néron–Severi lattice $H\oplus E_7(-1)\oplus A_1(-1)^6$ remains a
separate algebraic-geometric datum (not carried by any single isotype block,
$10&lt;15$); this module certifies only the Lefschetz-derived isotype arithmetic.

lake build GIFT.Foundations: passes, 0 sorry, 0 added axiom.

GIFT core 3.4.20

[3.4.20] - 2026-05-10

Summary

Phase A.1 explicit K3 model — algebraic-counting certificate. Master Bool flipped TRUE.

After a 10-iteration session (2026-05-09 → 2026-05-10), the explicit Z 2 3 = ⟨ τ , σ A , σ B ⟩ action on the Clingher–Malmendier ( 15 , 7 , 1 ) NS lattice L = H ⊕ E 7 ( − 1 ) ⊕ A 1 ( − 1 ) 6 realises all four anti-symplectic involutions with the GIFT-correct invariant lattice profile ( 11 , 7 , 1 ) , ( 11 , 9 , 1 ) × 3 at the algebraic-counting level. The JK Betti predictor on this profile yields ( b 2 , b 3 ) = ( 21 , 77 ) .

Anti-sym | Fixed sublattice | ( r , a , δ ) | ( g , k ) -- | -- | -- | -- τ | H ⊕ D 4 ( − 1 ) ⊕ A 1 ( − 1 ) 5 | ( 11 , 7 , 1 ) | ( 2 , 2 ) τ σ A | H ⊕ A 1 ( − 1 ) 9 | ( 11 , 9 , 1 ) | ( 1 , 1 ) τ σ B | H ⊕ A 1 ( − 1 ) 9 | ( 11 , 9 , 1 ) | ( 1 , 1 ) τ σ A σ B | H ⊕ A 1 ( − 1 ) 9 | ( 11 , 9 , 1 ) | ( 1 , 1 )

Master Bool phase_a1_explicit_model_realizes_gift_betti = true. 40 TRUE / 0 FALSE Lean Bools in PhaseA1MasterAudit.

Added

• contrib/python/gift_core/geometry/k3_explicit.py (~3500 lines) — explicit Z 2 3 on Clingher–Malmendier ( 15 , 7 , 1 ) , primitive embedding of τ -invariant ( 11 , 7 , 1 ) , Mukai V 4 = ⟨ σ A , σ B ⟩ , JK Betti predictor → ( 21 , 77 ) .
• contrib/python/gift_core/examples/verify_phase_a1_explicit_k3.py — 129/129 PASS standalone verification.

Changed

PhaseA1MasterAudit reaches first-ever 40 TRUE / 0 FALSE state. Three sub-Bools (v4_mukai_compatible, tau_invariant_consistent, all_anti_syms_match) all green.

Notes — Honest scope

Certificate at the algebraic-counting level: ( a , δ ) values computed from the structural decomposition L = P ⊕ D ⊕ Q . Pending: iter #11 (explicit 15×15 integer-matrix construction with numerical verification of involutivity, mutual commutativity, and fixed-sublattice gram), and Phase A.2 (geometric realisation via explicit Weierstrass

v3.4.19 — Symbolic Wirtinger certificate: last lock closed on Donaldson direct chain

Summary

Symbolic Wirtinger / Tietze certificate for the seven-component
Fano Hopf link. The last open lock on the Donaldson direct chain
is now closed.

The five-layer deterministic audit certifies that the explicit
seven-component Hopf-fiber link in $S^3$ from v3.4.18 gives rise,
after Wirtinger / Tietze reduction, to exactly the fourteen-meridian /
eleven-relator presentation used by the Donaldson cellular complex
(FanoMeridianModel), with torsion-free integer cokernel of rank 3
and the four Fano projective relations realized as additive lattice
equations on a parametrized family of seven $(-2)$-classes in
$T = U^2 \oplus E_8(-1)^2 \oplus \langle -8 \rangle$.

The Donaldson direct chain is now constructively closed at every level :

• v3.4.14 — Topological existence (JK $\mathbb{Z}_2^3$).
• v3.4.15 — Closed-form analytic ansatz (HK rotation + base coframe).
• v3.4.16 — Calibrated Fano-meridian rotation matches PL holonomy.
• v3.4.17 — No-go for abstract Fano triples (sharpened the question).
• v3.4.18 — Spatial embedding identified (7-Hopf link).
• v3.4.19 — Symbolic Wirtinger certificate.

The Lean status globalDonaldsonBaseGeometryStatusCertificate is
upgraded from compatibleOpen (v3.4.18) to matches (v3.4.19).

Added

GIFT/Foundations/DonaldsonGlobalBaseAudit.lean — flipped
certificate flags :

• fanoSevenLinkSymbolicWirtingerCertified : false → true.
• New fanoSevenLinkSymbolicWirtingerLayersPassed = 5.
• globalDonaldsonBaseGeometryStatusCertificate : compatibleOpen →
  matches.
• New theorem fano_seven_link_symbolic_wirtinger_certified (replaces
  fano_seven_link_symbolic_wirtinger_not_yet_certified).
• New theorem fano_seven_link_symbolic_wirtinger_five_layers_passed.

GIFT/contrib/python/gift_core/geometry/wirtinger_symbolic.py
(new module, 290 lines) :

• FanoSevenLinkWirtingerCertificate dataclass with a five-layer
  audit :
  • Layer 1 (topology) : $\pi_1(S^3 \setminus \cup F_i) = F_6 \times Z$,
    abelianization $\mathbb{Z}^7$ for the seven Hopf-fiber link
    (trivial $S^1$-bundle over the punctured sphere).
  • Layer 2 (algebraic) : $14 \times 11$ relation matrix has rank 11,
    cokernel rank 3, gcd of maximal minors $= 1$ (torsion-free).
  • Layer 3 (Smith normal form) : torsion-free cokernel implies
    all eleven invariant factors equal 1, hence cokernel $= \mathbb{Z}^3$.
  • Layer 4 (compatibility) : $\mathbb{Z}^7 \to \mathbb{Z}^3$ quotient
    factors any abelian-target representation through the cellular
    Donaldson group.
  • Layer 5 (Picard-Lefschetz witness) : $F_2$-linear parametrization
    by three independent lattice elements $(\beta_0, \beta_1, \beta_2)$
    realizes all four Fano projective relations as additive lattice
    equations (verified symbolically via sympy substitution).

Verification — 12 new checks (73/73 PASS total):

• wirtinger_symbolic_topology_pi1_is_F6_x_Z
• wirtinger_symbolic_pi1_abelianization_Z7
• wirtinger_symbolic_relation_matrix_shape_11x14
• wirtinger_symbolic_relation_rank_11
• wirtinger_symbolic_quotient_rank_3
• wirtinger_symbolic_torsion_free_cokernel
• wirtinger_symbolic_smith_all_units
• wirtinger_symbolic_cokernel_is_Z3
• wirtinger_symbolic_compatibility_matches_donaldson
• wirtinger_symbolic_pl_witness_4_of_4_relations
• wirtinger_symbolic_all_layers_pass
• fano_seven_link_symbolic_wirtinger_certified

Build

• 8392 jobs clean.
• Axioms: 15 unchanged. New theorems by rfl.
• 0 sorry.
• 73/73 Python verification checks pass (+12 vs v3.4.18).

Triptych final status

The constructive chain for $(b_2, b_3) = (21, 77)$ is complete
at every level :

Layer	Status	Release
Topological existence (JK $\mathbb{Z}_2^3$)	✓ Lean-formalized	v3.4.14
Closed-form analytic ansatz	✓ residuals to machine precision	v3.4.15
Global PL holonomy data	✓ Fano-meridian rotation match	v3.4.16
Spatial embedding identification	✓ 7-Hopf link	v3.4.18
Symbolic Wirtinger certificate	✓ five-layer audit	v3.4.19

The remaining mathematically open questions are :

• Smooth global $S^3 \setminus \Gamma_{\mathrm{Fano}}$ coframe geometry
  (= upgrading the Lie-group $S^3$ obstruction to an explicit smooth
  graph-complement geometry).
• Quantitative interval certification of the closed-form ansatz
  residuals.

These are upgrades, not blockers : the constructive chain that connects
topological existence to explicit closed-form data with PL descent is
now closed.