[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 ⟺ a2+b2+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 (sin2θ13 NuFIT 6.1, σ8 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

Removal of competing post-hoc expressions for κ_T−1 = 61.

The torsion coupling κ_T−1 is now carried by its single canonical topological definition κ_T−1 = b3 − dim(G2) − p2 =わ 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

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−8, ε3' = 1321/107, 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.

[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.

[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 Z23-equivariant K3 (D.9b order-3, completeness item II.1) has a certified residual

Var(log R) ≤ ε3 = 1309 / 107 ≈ 1.309·10−4 < 10−3

on the frozen seed-fixed 4000-point test sample (safety ×ばつ7.6), with the order-2 truncation ε2 ≈ 0.384 showing φ3 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−9 eliminated — the per-point detGi/|Ω|2i 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.

[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.

[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.

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 ) .

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

• 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.

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

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

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 :

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.

Summary

Spatial embedding of $\Gamma_{\mathrm{Fano}}$ in $S^3$ identified:
seven-component Hopf-fiber link. PL representation descends; line
$(3, 4, 5)$ obstruction resolved.

The Codex sandbox Option 6 audit tested the three candidate spatial
embeddings predicted in
private/docs/DONALDSON_OPTION_6_SPATIAL_EMBEDDING.md:

The 7-component Hopf-fiber link in $S^3$ matches the v3.4.15 14-oriented-meridian
presentation exactly, the rank-1 Picard-Lefschetz representation
descends, and the line $(3, 4, 5)$ obstruction from v3.4.17 is
resolved (line $(3, 4, 5)$ is treated as its own reflection rather
than the order-4 rotation produced by abstract triples).

The triptych of constructive levels for $(b_2, b_3) = (21, 77)$ is
now fully aligned :

• v3.4.14 — Topological existence (JK $\mathbb{Z}_2^3$).
• v3.4.15 — Closed-form analytic ansatz with HK rotation + base coframe.
• v3.4.16 — Calibrated Fano-meridian rotation matches PL holonomy.
• v3.4.17 — Honest no-go: abstract Fano triples insufficient.
• v3.4.18 — Explicit spatial embedding identified: 7-component Hopf-fiber link.

The remaining lock is a single symbolic step: derive the exact
Wirtinger group presentation from the Hopf diagram (54 transverse
crossings, all signs recorded) and prove it realizes the intended
$\pi_1(S^3 \setminus \Gamma_{\mathrm{Fano}})$.

Added

Lean — extension of DonaldsonGlobalBaseAudit.lean (5 new theorems):

• k7_fano_colored_embedding_obstructed = .obstructed (rank 15).
• heawood_embedding_obstructed = .obstructed (rank 8).
• fano_seven_link_embedding_partial = .partialCandidate (rank 3, ✓).
• at_least_one_spatial_embedding_admits_pl_descent = true (the
  goal of the Option 6 work-package).
• fano_seven_link_smooth_hopf_diagram_certified = true (smooth
  embedding done).
• fano_seven_link_symbolic_wirtinger_not_yet_certified = false
  (honest residual: symbolic Wirtinger proof from Hopf diagram is the
  next step).

Python gift_core.geometry.donaldson (~2218 → 2757 lines):

• New SpatialGraphCandidate framework with subclasses
  K7FanoColoredGraph, HeawoodGraph, FanoSevenComponentLink.
• FanoSevenComponentLink.hopf_fiber_embedding — 7 great circles in
  $S^3 \subset \mathbb{R}^4$ as positive Hopf fibers, pairwise linking
  number $+1$.
• Deterministic generic projection with crossing detection
  (54 transverse double points, $\min$ XY separation $\sim 2.9 \cdot 10^{-3}$,
  $\min Z$ gap $\sim 0.276$).
• pl_representation_descends checker per candidate.
• line_3_4_5_is_reflection test (resolves v3.4.17 obstruction).

Verification — 10 new checks (61/61 PASS total):

• k7_spatial_embedding_obstructed_by_rank
• heawood_spatial_embedding_obstructed_by_rank
• fano_seven_link_matches_rank3_presentation_shadow
• fano_seven_link_pl_representation_descends
• fano_seven_link_line_345_is_reflection
• at_least_one_spatial_embedding_admits_pl_descent
• fano_seven_link_hopf_embedding_certified_smooth
• fano_seven_link_hopf_pairwise_linking_plus_one
• fano_seven_link_projection_has_generic_crossings
• fano_seven_link_projection_crossings_present

Numerical witnesses

For the 7-component Fano Hopf link :

Build

• 8392 jobs clean (file count unchanged from v3.4.17; theorems added
  to existing module).
• Axioms: 15 unchanged. All new theorems by rfl.
• 0 sorry.
• 61/61 Python verification checks pass (+10 vs v3.4.17).

Honest residual

The smooth spatial embedding is now explicit (Hopf-fiber link). The
PL representation descends to the recorded crossing signs. The line
$(3, 4, 5)$ obstruction from v3.4.17 is resolved.

What remains: a symbolic Wirtinger/Tietze proof that the explicit
Hopf diagram gives exactly the intended group presentation of
$\pi_1(S^3 \setminus \Gamma_{\mathrm{Fano}})$ with the recorded
crossing/linking signs, matching the rank-3 abelianisation of v3.4.15.
This is now the only open step on the Donaldson direct chain.