Euclids-path

🇷🇺 Русская версия: README.ru.md · 🇬🇧 You are reading the English version. On the documentation site a language switcher is available; on GitHub the prose links below point straight to the English *.en.md chapters.

A consolidation of the proof programme for the twin-prime conjecture, built around Euclid's perpetual engine (the impossibility of an infinite "clean" descent — a version of Fermat's infinite descent).

This is not a finished proof. It is a machine-checkable assembly in which the conjecture is reduced to a single open node, and the whole path — from the engine's laws to the final reduction — is visible across the numbered files.

Paper. An arXiv-style write-up of the whole programme (LaTeX + PDF) is attached to the latest release and is being prepared for publication. What still changes is mostly the prose — the exposition is being refined; the mathematical content and the machine-checked results are settled.

Euclid's-path fractal · genealogy ornament: the full old-peel descent of every centre $6m\pm1$, woven with chords on the circle of centres; the colour is the Euclid prime of the step $6m\mp1=p\cdot(6t\pm1)$. The yellow points on the circle are the twin-centres with empty genealogy (those whose descent breaks off at once): their infinitude is exactly the twin conjecture. The other five kinds live in tools/fractal/.

★ Main theorem: "Higher-energy incompatibility" (higherEnergyIncompatibility_main, core 🟢). It proves, strictly, exactly this: you cannot know that the twins are infinite; but if the non-knowledge of the first cause is taken for truth — they are infinite, and that is strict. To learn the first cause from within would cost a perpetual engine, which does not exist — so it is unknowable; and a finite observer tells even a single twin apart only by a whole clean class. Both walls are of one nature; the load-bearing edge closes the circle: this very incompatibility plus the accepted causal boundary ⟹ the twins are infinite (higherEnergyIncompatibility_twins 🟡 — conditional on the axiom, not a proof).

Cosmologically (strict theorems, chapter 33): the number line and the impossibility of the engine together encode space and time. The strict traversal order is space (with a floor-singularity at 0); the irreversible arrow of time is proved strictly (engine_never_returns — height is strictly antimonotone, there is no way back), with an unreachable end at ∞, which only a perpetual engine could reach. The first cause is the instant when the engine emerges from the singularity 0 and sets off forward without turning; it cannot be given from within (self-start = perpetual engine, no_internalisedOriginEvent), so it is accepted from outside — by the single axiom. Hence, inside the system, the infinitude of the twins can be neither proved nor refuted: both actions would require a perpetual engine. There is no tower of causes beneath the first cause — the regress is well-founded (no_rankedMetaFractalBranch); the universe is one.

Map of the path: prose/00_Overview.en.md — the main navigator. Source of truth: the primary records in f:/Primes/*.md/*.csv (not edited).

---

Map: one engine — seven branches, a zoo and geometry

At the foundation lies a single physical prohibition: the impossibility of a perpetual engine (no_infinite_descent, the bare Lean core). Seven great questions turn out to be its shadows on different objects. The structural half of each is proved green (where the engine is forbidden, there is no deviation); and the last step — the tie to a real object — is either accepted by the single first-cause axiom step00FirstCause (ONE yellow decree boundary — the twins), or remains a green conditional theorem, or stays an open 🔴 input. A through-line discussion is in the prologue.

Universal form (Engine/UniversalEngine): the engine is defined over ANY relation (PerpetualEngine), and its impossibility follows from an internal cause: the definition is an infinite strict descent, and well-foundedness is exactly its prohibition (no_perpetual_engine_of_wellFounded; perpetualEngine_iff_not_wellFounded). It carries into any space with an ℕ-rank (no_perpetual_engine_of_rank — every front is a corollary of one theorem; EPMI is shown as an instance). But not "everywhere": on the continuum ℝ the engine works (perpetualEngine_on_real) — which makes Euclid's path a controller (universal_engine_dividing_line, M6): it decides where motion is forbidden (the discrete) and where it is realised (the continuum). The core is mathlib well-foundedness; the contribution is formalisation-unifying; the taint is unchanged.

flowchart TD
    ROOT["⚙️ no_infinite_descent · EPMI<br/>Euclid’s perpetual engine is impossible · bare Lean core 🟢"]

    ROOT --> MT["★ MAIN THEOREM · higherEnergyIncompatibility_main 🟢 · core with NO axiom<br/>knowing the first cause from within = a perpetual engine (forbidden)<br/>⟹ the first cause is unknowable; from inside, twins can be neither proved nor refuted"]
    MT ==>|"PRESSES ON THE AXIOM: since it is impossible from within, the first cause can only be ACCEPTED from outside, never derived"| FC{{"step00FirstCause · the SINGLE axiom<br/>first cause 0 → 1 · ONE living boundary (twins, seriality form)"}}

    FC --> TP["Twins 🟡 · taken — the ONLY decree boundary<br/>SerialTwinBoundaryObligation ⟺ twin conjecture (two-sided, non-vacuous)<br/>irreducible node · incompatibility barrier"]
    MT -.->|"load-bearing face 🟡: incompatibility + boundary ⟹ twins are infinite"| TP

    FC -.->|"the decree carries ONLY twins — here is why"| WHY
    WHY["WHY RH and NS ARE NOT DECREED (Option A)<br/>Only the twin boundary is provably ⟺ its conjecture with BOTH sides non-vacuous,<br/>so postulating it = postulating exactly twins. RH and NS lack this, so they were<br/>WITHDRAWN from the axiom and kept as honest green CONDITIONAL fronts — not results.<br/>Machine-checked in Engine/Step00FrontClosureAudit"]
    WHY -.-> RH
    WHY -.-> NS

    ROOT --> RH["Riemann 🟢/🔴 · DETACHED front (was decreed, withdrawn)<br/>manifestationLaw ⟺ RH only UNDER the twin boundary, and its reverse is vacuous;<br/>the unconditional bridge = RH renamed (circular). A conditional reduction, not a result"]
    ROOT --> NS["Navier–Stokes 🟢/🔴 · DETACHED front (was decreed, withdrawn)<br/>gate law ⟹ surrogate only (forward); reverse UNKNOWN (no ℝ³ divergence theorem);<br/>manifestation form ⟹ ¬twin boundary. Real gap: GlobalVorticityControl (BKM)"]

    ROOT --> PNP["P/NP 🟢<br/>rank-fast traversal ≠ full certificate payment"]
    ROOT --> YM["Yang–Mills 🟢<br/>spectral quantisation ⟺ mass gap"]
    ROOT --> HC["Hodge 🟢<br/>descent law ⟺ payment by cycles"]
    ROOT --> BSD["Birch–Swinnerton-Dyer 🟢/🔴 · the eighth mask<br/>descent-without-engine on a real curve<br/>🔴 analytic rank = ord L (outside mathlib)"]

    ROOT --> MP["Mersenne ⏸️ · DEFERRED<br/>reason for refusal: the heuristic sign is negative<br/>(Σ over pairs converges; 5∣2^p−3) · witness ≥ 29, unpresentable"]
    ROOT --> ZOO["Arithmetic zoo 🟢 · fields NOT taken (§17)<br/>Polignac · Sophie Germain — sign «for»<br/>Goldbach · Legendre · perfect — witness by decide (strongest unpresentability)<br/>Fermat ⏸️ — sign «against» (strictly stronger than twins)"]

    ROOT --> CL["Collatz ✗ · THE DECREE FELL<br/>reason: the rope law was over-strong + decidable<br/>refuted at n=27 (ropeLaw_universal_refuted, decide)<br/>boundary removed, conjecture still open"]

    ROOT --> GEO["Geometry of the path 🟢<br/>arrow · curvature κ=1−outdeg (χ=−5)<br/>twin ± flip ⟂ time (C, not T)"]
    GEO -. the same twin boundary .-> TP

    ROOT --> WF["Well-foundedness canon 🟢<br/>Goodstein/hydra (ω-worm, transfinite rank) · Markov descent · Poincaré line<br/>the engine reaches classical termination"]
    WF -. underpins the one prohibition .-> MT

    classDef green fill:#0b3d0b,stroke:#4caf50,color:#eaffea;
    classDef apex fill:#0b3d0b,stroke:#ffd700,stroke-width:2px,color:#eaffea;
    classDef yellow fill:#4d3b00,stroke:#ffc107,color:#fff8e1;
    classDef deferred fill:#2a2a2a,stroke:#9e9e9e,color:#e0e0e0,stroke-dasharray: 6 4;
    classDef fallen fill:#3d0b0b,stroke:#e57373,color:#ffebee;
    classDef rootnode fill:#1a1a1a,stroke:#888,color:#ffffff;
    classDef detached fill:#12333a,stroke:#4dd0e1,color:#e0f7fa,stroke-dasharray: 5 3;
    classDef note fill:#2b2b3a,stroke:#b39ddb,color:#ede7f6;
    class ROOT,PNP,YM,HC,BSD,ZOO,GEO,WF green;
    class MT apex;
    class TP yellow;
    class RH,NS detached;
    class WHY note;
    class MP deferred;
    class CL fallen;
    class FC rootnode;

Loading

Colours: 🟢 — machine-proved under standard axioms (the structural part / a green conditional theorem); 🟡 — AXIOM-TAINTED, conditional on the first cause (the object accepted by decree at an honestly disclosed price); 🔴 — an open input (the real object: the QFT spectrum, the primes' Hamiltonian, a Leray solution, the (p,p)-classes, a Turing machine — absent from the formalisation). 🔵 dashed — a DETACHED front: it once sat on the decree but was WITHDRAWN (Option A) because it lacks a two-sided boundary ⟺ conjecture; it survives as an honest green/red conditional reduction, never as a decree result (Riemann, Navier–Stokes; the reason is the WHY block in the graph). ⏸️ — the problem is examined but its boundary is NOT taken: deferred by heuristic sign (Mersenne, Fermat) or a zoo front with no field (§16–17). ✗ — the decree was taken and FELL (Collatz, refuted at n = 27). Collatz went through the full cycle of the discipline: its rope law was the fourth boundary of step00FirstCause — and it was machine-REFUTED (ropeLaw_universal_refuted, witness n = 27); the tripwire fired, the boundary was removed, the decree path closed by a forged refutation. The green front is Engine/CollatzTugOfWar, the post-mortem Engine/CollatzFirstCause (chapters 55–56).

The arithmetic zoo (ch. 44–48, all 🟢, no fields taken). The same manifestation apparatus is run through six new number-theoretic stories: cousins and sexy primes (Polignac), Sophie Germain, Goldbach, Legendre, odd perfect numbers, Fermat numbers. All are green and conditional only on the definitions of the laws; not a single open problem is solved or declared. The gem is the green Euler–Lagrange classic: SG-primes with p ≡ 3 (mod 4) divide the Mersenne number M_p (23 ∣ M₁₁), a formal fragment of the very heuristic whose sign defers the Mersenne boundary (§16). The trilemmas are passed everywhere, but no fields are taken, deliberately (§17): five stories carry the sign "for" (like Riemann), Fermat the sign "against" (stronger than Mersenne); for Goldbach/Legendre/perfect the witness is pointwise decidable (decide) — the strongest non-presentability. The only unconditional green theorem about primes here is Bertrand (a prime desert does not survive doubling), and it is disclosed honestly why Legendre needs more than it.

Geometry of the path (ch. 49, 🟢 + 2 🟡). The concrete descent graph is read geometrically: the arrow of time (lexRank only falls), the computed curvature κ = 1 − outdeg (spectrum from −8 to +1, discrete Gauss–Bonnet χ(cone3) = −5), "flatness everywhere ⟹ a perpetual engine", and the irony — Euclid's path violates Euclid's own second postulate (a line cannot be extended without bound), and so there are no parallels. The intersection of lines is proved 🟡 from the same first cause (exactly two axiom-tainted declarations, no new field), but it cannot be known from within (🟢) — the knowledge would cost an engine. Navier–Stokes on ℝ³ (a postscript to ch. 41): the box-class energy balance is derived green, the divergence theorem genuinely engaged; the cascade smoothness of this class is decree-free. The Clay reduction (Engine/NavierStokesClayReduction): the exact Clay-(A) statement is encoded, and the logical reduction "known theory (Kato + Beale–Kato–Majda) + one criterion GlobalVorticityControl ⟹ Clay-(A)" is proved green — the single open theorem is isolated and named (vorticity control, the supercriticality barrier). NS is not solved and not declared solved; it is machine-recorded that the engine surrogate is strictly weaker than the criterion (greenBudget_strictly_weaker_than_vorticityControl, via a non-uniform cascade) — the engine reading does not close the problem. A discrete fluid model (Engine/CascadeBudget, Engine/DyadicBlowup, Engine/DyadicFirstCause, chapter 52): probably the first formalisation of a fluid model in a proof assistant (known mathematics: the budget principle + the Katz–Pavlović model). A machine map of the boundary of the engine reading: where it works (budget ⟹ finite time under UNIFORM dissipation) and where it breaks (superlinear_blowup_sq + dyadic_blowup — the cascade blows up, the engine is REALISED). The connecting cascade-drive y'≥C·y² is now derived from the raw λⁿ relations — for the exact self-similar solution (ssLead_drive) and for a whole class through a front invariant (frontDrive_of_invariant): a monolithic named hypothesis is narrowed to a smaller, coordinate-close invariant; the only isolated input left open is front persistence for infinitely many modes (the moving KP front). And the source of the cascade (the pump n=0, uncausable from within — 🟢 dyadicOrigin_uncausable_from_inside) was once decreed via the first cause (DyadicFirstCause, via nsBoundary) — but that decree projection was WITHDRAWN with NS (Option A); only the green wall dyadicOrigin_uncausable_from_inside survives, so the dyadic source is now an open/conditional front, not a decree result. There is no new MATHEMATICS (the Tao barrier); the novelty is in the formalisation. NS is not solved.

Structure

• EuclidsPath/Engine/*.lean — the main (proved) line: the engine and its laws → reduction to the twins → attack lines → the final node. Imported by the root EuclidsPath.lean in the order of the proof's progression.
• prose/NN_*.md — the paired prose, the same through numbering 00→50 (+ appendix A), a single academic narrative: engine → twins → first cause and THE MAIN THEOREM → side branches → the arithmetic zoo (44–48) → the geometry of the path (49) → the coda (50). English siblings live in prose/NN_*.en.md.
• tools/ — numerical harnesses (*_harness.py) and results (RESULTS_*.md); tools/fractal/ — visualisation of Euclid's fractal (8 kinds: descent forest, rank field, twin spiral, load landscape, the line of centres with genealogies, the ornament of genealogies — and two conceptual cosmological views for the coda: an observer with an event horizon and an arrow of time pointing inward, a time-sphere with observer/singularity antipodes; the last two are a superstructure over the real substrate, euclid_cosmology.py).

The path (prose ↔ Lean)

№	Topic	Prose	Lean	Status
00	Goal, map of the path, definitions	00	Step00_Overview	🔴 goal
01	Impossibility of the engine (EPMI)	01	Engine/EPMI	🟢
02	Carrier of two gcd∣2	02	Engine/Carrier	🟢
03	Conservation of two XY−ZW=2	03	Engine/TwoGap	🟢
04	Descent + boundary-law	04	Engine/Descent	🟢
05	Irreversibility / 2 laws	05	Engine/Irreversibility	🟢
06	No way back (exclusivity)	06	Engine/NoBackward	🟢
07	Short train (squeeze)	07	Engine/Squeeze	🟢
08	Bounded cycle	08	Engine/BK	🟢
09	Factor-repeat rigidity	09	Engine/Cycle	🟢
10	survivor ⇒ twin; the ∞ bridge	10	Engine/NonCover	🟢
11	Conjecture ⟸ block core	11	Engine/TwoTransport	🟢
12	Four-corner (negative association)	12	Engine/FourCorner	🟢
13	Fractal layer / model	13	Engine/ModelFourCorner	🟢
14	Remainder decomposition	14	Engine/RealFourCorner	🟢
15	Chain to the twins (conditional H)	15	Engine/ToTwins	🟢
16	By contradiction: finite∧H⇒False	16	Engine/FiniteContradiction	🟢
17	Payment law (ledger)	17	Engine/PaymentLedger	🟢
18	SNOL — shifted-neighbour node	18	Engine/SNOL	🟢
19	Old-peel: catch as a descent step	19	Engine/OldPeel	🟢
20	NOPSL: no old-peel sink	20	Engine/NOPSL	🟢
21	Regeneration dichotomy (Ω_A)	21	Engine/Regeneration	🟢
22	Residuals: start, sink⇒twin	22	Engine/Residuals	🟢
23	Clean/boundary graph	23	Engine/CleanGraph	🟢
24	Boundary decomposition + global node	24	Engine/BoundaryDecomp, Engine/LabelledFanIn, Engine/AtomicSNOL, Engine/ConcreteComponents, Engine/BadCoverDescent, Engine/ObstructionClosure, Engine/ManyUnresolved, Engine/HigherEnergy, Engine/HigherTower, Engine/EngineTower, Engine/ParityBarrier, Engine/ReverseTower, Engine/AboveConflict, Engine/JumpBarrier, Engine/PaidDynamics, Engine/ClosedUniverse, Engine/BoundaryDefectPayment, Engine/BoundaryLedgerCollision, Engine/ConcreteStep00Graph, Engine/DichotomyEngine, Engine/DissipativeCascade	🟢 decomp.; 🔴 node
25	Rigid closure (reaches_twin)	25	Engine/RigidClose	🟢
26	Separating scale ⟹ ¬ProductHall	26	Engine/SeparatingScale	🟢
27	Product-core: the whole machine	27	Engine/ProductCore	🟢
28	Factorisation → RankNode	28	Engine/MkNode	🟢
29	The last link + boundary	29	Engine/CarrierBridge	🔴 the single node
30	Riemann: contraposition (engine)	30	Engine/RiemannBranch, Engine/RiemannEngine, Engine/RiemannImpossibleEngine, Engine/RiemannImpossibleEngineOff, Engine/RankJumpBridge	🔴 RH input
31	Riemann via Liouville (λ=(−1)^rank)	31	Engine/RiemannLiouville	🔴 RH input
32	Unified rank-parity node (epilogue)	32	— (synthesis)	🔴 unity conjecture
33	First cause + THE MAIN THEOREM	33	Engine/CausalClosureAxiom (quarantine), Engine/FiniteKnowledgeBarrier	🟢 core; 🟡 corollaries
34	Mersenne branch	34	Engine/MersenneBranch, MersennePaymentConflict, MersennePeelPressure, MersenneForwardFront	🟢 bridge; 🔴 inputs; ⚠️ vacuity №3
35	P/NP: node and classical bridge	35	Engine/LocalPNPNode, ClassicalPNPBridge, CanonicalSelfReduction, ClassicalFrontierRoutes, RankClosureFront	🟢 assembly; 🔴 frame+reconstruction
36	Navier–Stokes	36	Engine/NavierStokes	🟢 skeleton; 🔴 EnergyBalanceLaw
37	Riemann fronts	37	Engine/RiemannTrivialZeros (input №1 CLOSED), RiemannRankProjection(+Audit), RiemannTwoTransportFront, RiemannArithmeticTwoTransport, RiemannSpectralAnchorAudit, RiemannLayerBoxFront, RiemannTerminalRankFront	🟢 arithmetic; 🔴 two inputs; ⚠️ vacuity №2
38	Riemann via the first cause	38	Engine/RiemannManifestationFront (green chain), Engine/RiemannLawEpistemic, Engine/RiemannDualEngineFront	🟢 chain (RH ⟺ manifestation law only UNDER the twin boundary, reverse vacuous); 🔵 DETACHED — RH decree withdrawn (Option A); 🔴 dual packages
39	P/NP: rank certificate payment	39	Engine/PNPRankPaymentFront (green separation A ≤ 4 + trilemma), Engine/PNPFirstCause (epistemic complement)	🟢 separation in the rank model; 🟢 the decision is unknowable from inside a finite-fuel machine (pnpCause_unknowable, ch. 56); 🔵 P/NP decree projection withdrawn (Option A); ⚠️ vacuity №4
40	Yang–Mills: mass gap via the engine	40	Engine/YangMillsFront (green chain + trilemma), Engine/CausalClosureAxiom §12	🟢 quantisation⟹gap; 🟡 decree language; 🔴 spectral data-anchor
41	NS: smoothness via cascade + integral	41	Engine/NavierStokesFront (identity + trilemma + COMPLETION: two forgings and the gate law), Engine/Step00FrontClosureAudit	🟢 identity+cascade+forgings; 🔵 DETACHED — NS decree withdrawn (Option A); the gate law ⟹ surrogate only (forward, reverse unknown), manifestation form refutes the twin boundary
42	Hodge: quantised charges and payment	42	Engine/HodgeFront (hero + collapse + trilemma), Engine/CausalClosureAxiom §14	🟢 descent⟹payment, the engine dead unconditionally; 🟡 tripwire; 🔴 DescentLaw
43	Mersenne: refutation = engine	43	Engine/MersenneManifestationFront (Π-witness, law, essence M3), Engine/CausalClosureAxiom §16 (comment)	🟢 chain + "the 4c+1 chain does not peel"; a field is ADMISSIBLE but DEFERRED (heuristic sign against)
41′	(postscript) NS: integral assembled on ℝ³ (box)	41	Engine/NavierStokesR3Assembly	🟢 R1 derivative under the integral + R2 divergence (faces vanish) + three integrations by parts DERIVED (pressure/convection/viscosity) ⟹ box-class energy balance unconditional ⟹ cascade smoothness WITHOUT the decree; 🔴 only the box→ℝ³ limit and TimeDomination remain
44	Sides and Polignac (cousins p+4, sexy p+6)	44	Engine/SideInfinitude, Engine/PolignacBranch, Engine/PolignacManifestationFront	🟢 Dirichlet: the sides are separately infinite; classification, constellation, essence; NO field (§17, no chain — nothing to forge)
45	Sophie Germain: the gem of the series	45	Engine/SophieGermainBranch, Engine/SophieGermainManifestationFront	🟢 SG-primes with p≡3 (mod 4) DIVIDE Mersenne (23∣M₁₁) — the Euler–Lagrange classic; centre doubling; anti-Mersenne restriction ("two bets")
46	Goldbach and Legendre	46	Engine/GoldbachManifestationFront, Engine/LegendreDesertFront	🟢 the witness is pointwise DECIDABLE (decide up to 52/up to 10); GREEN Bertrand (a desert does not double), but shorter than Legendre; NO field
47	Perfect numbers: Euclid–Euler	47	Engine/PerfectNumberBranch, Engine/OddPerfectManifestationFront	🟢 BOTH directions of Euclid–Euler (Archive); Mersenne primes ⟺ even perfect numbers unbounded; odd witness ≥ 101
48	Fermat numbers: a second bet against	48	Engine/FermatBranch, Engine/FermatManifestationFront	🟢 F_k ≡ 5 (mod 6) minus-side; the quadratic chain does not peel; localisation ≥ 65537; the sign is INVERTED more strongly than Mersenne — NO field
49	★ Geometry of the path: curvature, arrow, intersection	49	Engine/GeometryFront	🟢 arrow of time; κ=1−outdeg COMPUTED (−8…+1, χ=−5); flatness⟹engine; Euclid's SECOND postulate falls; 🟡 intersection from the first cause, but it cannot be known (2 declarations)
50	★ Coda: Euclid's path and the structure of spacetime	50	— (synthesis)	a philosophical/physical summary: one prohibition — seven masks + zoo + geometry; a possible TOE
—	Appendices & later fronts			the synthesis is closed; what follows extends the core
51	Numerical data	51	tools/RESULTS_*	—
52	Discrete fluid model	52	Engine/CascadeBudget, Engine/DyadicBlowup, Engine/DyadicFirstCause	🟢 budget+Katz–Pavlović blow-up, the drive DERIVED from the relations; 🔵 dyadic decree projection withdrawn (Option A) — the source is uncausable from within (green wall dyadicOrigin_uncausable_from_inside)
53	Birch–Swinnerton-Dyer (the eighth mask)	53	Engine/BSDFront	🟢 descent-without-engine on a REAL curve (Mordell–Weil) + a parity bridge to Liouville; 🔴 analytic rank = ord L (outside mathlib); NO boundary (trilemma); NOT a solution of BSD
54	Neighbours beyond the horizon (5 shadows)	54	Engine/{Chowla,Abc,Beal,Lehmer,Landau}Front	🟢 REAL mathlib anchors (Mason–Stothers, Polynomial.flt_catalan, Northcott+Kronecker, Dirichlet, Liouville); 🔴 the conjectures themselves (Chowla/abc/Beal/Lehmer/Landau) are open; no decrees; NOT solutions
55	Collatz: an engine on bounded fuel	55	Engine/CollatzEngine, Engine/CollatzFuel, Engine/CollatzTugOfWar	🟢 engine/rope laws + window budget ⟹ descent + "refutation = perpetual engine"; 🟢 the universal rope law is REFUTED (not_ropeCountingLaw_27)
56	The Collatz first cause: the decree that fell	56	Engine/CollatzFirstCause, Engine/CausalClosureAxiom §18	🟢 post-mortem: the boundary taken and REMOVED (the tripwire fired, the law is false); 🟢 the "verification, not derivation" epistemics survived; the conjecture 🔴 open

🟢 = machine-checked, without sorry (standard axioms). 🟡 = AXIOM-TAINTED (conditional on step00FirstCause; exactly 16 declarations, ALL asserting twins through the single accepted twin boundary — 13 in the quarantine (CausalClosureAxiom: the decree-consequence family …_generates_twins / causalClosureAxiom_asserts_twins_at_every_scale / twinLowersInfinite_…, step00CausalClosure, plus the status slogans) + the corollary FiniteKnowledgeBarrier.higherEnergyIncompatibility_twins + 2 geometry declarations of ch. 49 (GeometryFront.twin_vertices_beyond_every_horizon, lines_meet_but_unknowable_from_inside, via the same twin boundary). There are NO Riemann, NO Navier–Stokes/dyadic and NO Collatz declarations in the taint any more: RH and NS were WITHDRAWN from the decree (Option A) and the Collatz boundary fell — the axiom now decrees only twins. 🔴 = an open node / input.

Status — honestly

Three colours run through the whole programme, and here we name them plainly.

The green corpus — machine-proved, under standard axioms, without sorry. The whole of Euclid's engine and its laws (EPMI: the impossibility of infinite descent, irreversibility, finiteness in a finite number of steps); the reduction of the twin conjecture to a single block core; the entire product-core machine (rank-descent 4→1, pigeonhole); the infinitude of the carrier. The former walls — parity, circular payment, the three rank-descent defects — are all removed. This is the genuinely checked part: a "green" module cannot be forged, and the verifier's axiom tracker does not let a decree hide behind a green label.

The single open node. The whole twin branch is machine-reduced to one statement — TheLastStep00Obligation: a finite semantic key resolves genealogy collisions. It is honest: at every scale M0 it itself exhibits a twin-centre above M0 (that is, it is scale-wise no weaker than the goal) and exists in a dozen and a half equivalent forms — energetic, embedded, seam. The small branch A ≤ 4 we machine-refuted (a five-adic chain gives infinitely many genealogies without a single twin hypothesis), so the node lives only at A ≥ 5; its satisfiability there is genuinely open. twin_prime_conjecture remains a sorry — this is an honest reduction, not a proof. In detail — chapter 24 and 29.

The single axiom — the first cause (chapter 33). The node cannot be closed from within: its self-grounding would build a perpetual engine, and that is a proved impossibility. So we accept it from outside, by the single axiom step00FirstCause — a deliberate "0 → 1" event carrying exactly ONE causal boundary: the twins, in the transparent seriality form causalBoundary : SerialTwinBoundaryObligation. Earlier drafts also hung Riemann and Navier–Stokes on the decree; both were WITHDRAWN (Option A), because only the twin boundary is provably ⟺ its conjecture with both directions non-vacuous (see "Riemann and Navier–Stokes — detached, honestly" below). A would-be fourth boundary — the Collatz rope law — was taken and REMOVED: the law was machine-refuted (ropeLaw_universal_refuted), the tripwire fired (chapters 55–56). The axiom is locked in a quarantine module; the verifier marks every declaration that depends on it (exactly 16, ALL asserting twins: 13 in the quarantine + the corollary higherEnergyIncompatibility_twins + 2 geometry of ch. 49, all through the single twin boundary) — there are no leaks into the green line. The honesty is machine-level: the strength of the decree is exactly the twin conjecture, no weaker and no stronger — to accept the axiom = to accept exactly the twins (serialTwinBoundary_iff_unboundedTwinCenters). Knowing the cause from within is impossible as a theorem (cause_unknowable); hence the main theorem above.

Riemann and Navier–Stokes — detached, honestly. The twin closure works because the seriality boundary is provably equivalent to the twin conjecture with BOTH directions carrying content (forward = rank exhaustion, reverse = build a singleton engine): serialTwinBoundary_iff_unboundedTwinCenters. So "postulate the boundary" = "postulate exactly twins" — honest and meaningful. Neither Riemann nor Navier–Stokes admits this, so both were withdrawn from the decree and kept as green conditional fronts. The asymmetry is machine-recorded in Engine/Step00FrontClosureAudit:

• Riemann. The only equivalence to RH is manifestationLaw_iff_RH_of_boundary — and it holds ONLY under the twin-strength hypothesis TheStrictLastStep00Obligation, with a vacuous reverse (under RH there are no off-critical zeros, so the quantifier is empty). The unconditional bridges (offCriticalBridge_iff_RH and kin) are RH literally renamed — the engine dressing is a no-op, and the repo flags them circular. RH honesty is therefore parasitic on twin honesty; there is no independent two-sided boundary ⟺ RH.
• Navier–Stokes. There is no equivalence at all. The gate law implies only the surrogate NoSingularCascade (forward; noSingularCascade_of_nsSolutionBalanceLaw), and the reverse is UNKNOWN — blocked by the absence of an ℝ³ divergence theorem in mathlib — so the decree "may overpay". Worse, the NS manifestation form is INCOMPATIBLE with the twin boundary (nsManifestationLaw_refutes_boundary), so it cannot even be bundled. The genuine open gap is GlobalVorticityControl (the supercritical BKM estimate); the Clay reduction clayA_of_regularityTransfer_and_vorticityControl is honest-forward only.

The honest closure is therefore the asymmetry itself: one conjecture (twins) admits a transparent two-sided equivalence; the other two do not, and we say exactly why — rather than dress a renaming or an overpayment as a result.

Seven branches around one engine. Every great question is a shadow of the perpetual-engine prohibition on its own object, and the outcome is honestly different in each case:

• Twins — the ONE decree boundary 🟡: the node is green non-presentable and the seriality boundary is provably ⟺ the twin conjecture (two-sided), so it can be honestly accepted by axiom (33).
• Riemann — 🔵 a DETACHED front (was decreed, withdrawn): manifestationLaw ⟺ RH holds only UNDER the twin boundary and its reverse is vacuous, so RH is an honest conditional reduction, not a decree result (see "Riemann and Navier–Stokes — detached, honestly" above; 38).
• P/NP — 🟢 a theorem with no decree at all: fast rank traversal provably does not pay for an unbounded family of certificates (39).
• Yang–Mills and Hodge — 🟢 conditional theorems: spectral quantisation ⟹ mass gap, the descent law ⟹ payment by cycles (40, 42).
• Navier–Stokes — 🔵 a DETACHED front (was decreed, withdrawn): the cascade and the assembled box integral are green, but the gate law reaches only a surrogate (forward, reverse unknown) and its manifestation form refutes the twin boundary — an open/conditional front, not a decree result (36, 41).
• Mersenne — a side branch: an honest bridge, all load-bearing inputs 🔴 (34).

The recurring lesson, machine-proved across all fronts: an honest decree boundary exists only where the "deviation" itself is green non-presentable. Where the deviation can be forged — frames for P/NP, spectra for Yang–Mills, profiles for Navier–Stokes, charges for Hodge — the decree either explodes or is empty, and what remains is a green conditional theorem with an honestly named 🔴 input. The missing object is every time the same — a data anchor: a constructed YM spectrum, a Leray solution, the (p,p)-classes, a machine model — mathlib has none of them. Not a single Millennium problem is solved or declared solved.

Adversarial honesty. Four times the internal audit found an empty wrapper before it reached the showcase — vacuities №1–№4 (a degenerate peel of the node; an uninhabited Riemann rank-jump; a free witness for Mersenne; classically empty decider-fronts for P/NP). All were exposed by machine and documented in the modules themselves, not painted over — and that is the best argument to trust the parts that did pass the showcase.

Build

lake exe cache get    # precompiled mathlib oleans (v4.31.0)
lake build            # the whole Engine line; exit 0 = checked
lake env lean EuclidsPath/Engine/EPMI.lean   # a quick check of the engine core

Verification

lake env lean scripts/VerifyAll.lean   # enumerates declarations, counts the taint, self-checks the invariants

The verifier walks over every non-internal EuclidsPath* theorem/definition, collects the axioms it depends on, and prints: total declarations, sorryAx-tainted, tainted by a non-standard axiom. Then it self-checks the two eternal honesty invariants and fails with a non-zero code if either is violated: (1) the only non-standard axiom in the whole repository is step00FirstCause; (2) the only sorryAx-tainted declaration is twin_prime_conjecture. Current run: sorryAx 1, tainted by a non-standard axiom 16 (all asserting twins through the single accepted twin boundary — the number itself changes with the content and is not hard-pinned; only the two invariants are).