Commit 6d3f6ff
Brieuc
release: v3.4.15 — Donaldson direct analytic ansatz integration
Integrates parallel Codex sandbox progress on Donaldson direct route:
explicit closed-form G₂ ansatz on K3-coassociative neck with all
torsion residuals (det, dφ, d⋆φ) to machine precision in cohomogeneity-1.
10 new Lean modules:
- Foundations/DonaldsonCoassociativeFibration (b₂=21 alternative route)
- Foundations/MetricGapClosure, MetricCandidateSearch, MetricCatalogueSources
- Foundations/ExtraTwisted{Metric,GeometricCore,KernelPromotion}
- Foundations/K3AutomorphismPackage (JK side branch support)
- Foundations/K7NuBar (Bismut-Dai template, δ_CP track)
- Predictions/CP/DeltaCPNuBarConjecture (197 ≡ ν̄(K₇) mod 360)
Python workbench (~1500 lines, gift_core.geometry.donaldson):
- FanoMeridianModel: 14×11 integer relation matrix, primitive ℤ
- DonaldsonTopology: b₂=21, b₃=77, H*=99 closure
- DonaldsonG2Ansatz: explicit φ + ⋆φ sparse components
- ChebyshevProfile: deterministic min-energy solver
- DonaldsonRadialSolution: det(g)=65/32 exact (3.6e-15)
- DonaldsonSO3Connection: symmetric branch, exposes signed obstruction
- HyperkahlerRotation: SO(3) Lie-Euler integration + SVD reprojection
(|det R - 1| < 1e-12, ν(±1) = 0)
- BaseCoframeVariation: c_{i,jk}(t) = ±ν_k(t) cancelling dφ residual
- RotatingCoframeDonaldsonSolution: Option 2 + 4 combined, all PASS
Verification:
- lake build: 8391 jobs clean (+10 vs v3.4.14)
- Axioms: 15 unchanged (4 main + 11 interval)
- 0 sorry
- Python verify_donaldson_direct: 34/34 PASS
Honest scope: cohomogeneity-1 neck level certified; global Donaldson
base geometry on S³ with Fano-link discriminant deferred (Option 5
work-package in private/docs/). Complementary to v3.4.14 JK route.1 parent fda4743 commit 6d3f6ff
23 files changed
Lines changed: 4997 additions & 7 deletions
File tree
- GIFT
- Foundations
- Predictions/CP
- contrib
- docs
- python/gift_core
- constants
- examples
- geometry
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
40 | 40 | | |
41 | 41 | | |
42 | 42 | | |
| 43 | + | |
43 | 44 | | |
44 | 45 | | |
45 | 46 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
55 | 55 | | |
56 | 56 | | |
57 | 57 | | |
| 58 | + | |
| 59 | + | |
| 60 | + | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
| 64 | + | |
| 65 | + | |
| 66 | + | |
| 67 | + | |
| 68 | + | |
| 69 | + | |
| 70 | + | |
| 71 | + | |
| 72 | + | |
| 73 | + | |
58 | 74 | | |
59 | 75 | | |
60 | 76 | | |
| |||
0 commit comments