Formal Verification Certificate
Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.
Varela Re-Entry Nucleus • Lean 4 + Mathlib • Apoth3osis Labs
Varela Re-Entry Nucleus
Machine-checked formalization of Francisco Varela's self-referential re-entry as an honest Heyting algebra nucleus bridge. The autonomous value—the self-referential fixed point of the crossing operation—witnesses the failure of excluded middle in a three-valued carrier that is order-isomorphic to the fixed-point sublocale of a genuine closure operator.
11
Lean Modules
972
Source Lines
50+
Theorems
0
sorry / admit
Self-Reference as Algebraic Fixed Point
Varela's key insight: when the operation (Spencer-Brown's mark/unmark toggle) is applied to its own output, it produces a third value—the autonomous state—that is neither marked nor unmarked but is a fixed point of the crossing. This is self-reference made algebraic.
The autonomous value satisfies self-reference (crossing fixedness) while simultaneously witnessing the failure of excluded middle. This is not a contradiction—it is the characteristic behavior of a Heyting algebra that is not Boolean.
THE NUCLEUS BRIDGE
The crossing operation is not itself a nucleus (it fails monotonicity). The formalization resolves this honestly: embed the three-valued ECI carrier into a four-element ambient stage lattice with a genuine closure operator whose only non-trivial action is .
The fixed-point sublocale recovers exactly the ECI carrier, with an order isomorphism that preserves meet, join, bot, and top. The nucleus bridge is honest: it does not claim that is a nucleus, only that the ECI carrier arises as the fixed-point algebra of a genuine one.
Key Theorem Correspondence
| Lean Name | Statement | Significance |
|---|---|---|
| cross_fixed_iff | Self-reference = unique fixed point | |
| autonomous_not_classical | Excluded middle fails at self-reference | |
| omegaOrderIsoECI | Nucleus bridge recovers ECI exactly | |
| stageClosure_fixed_iff | Fixed = ECI-image characterization | |
| latent_not_fixed | Genuine counterexample exists | |
| cross_waveI_eq_waveJ | Temporal self-reference = waveform swap | |
| semantic_closure_fixed_iff | (M,R)-system closure bridge | |
| transport_stageClosed_order_reflects | Order-faithful transport witness |
Proof Blueprint
11 modules, 972 lines, 50+ theorems. Click to expand definitions and theorems.
Finite Witness Artifacts
These artifacts extract the computational finite witness surfaces from the Lean formalization: ECI carrier operations, waveform toggles, stage closure, and fixed-point checks. They are not transpilations of the proof terms—they are correct-by-construction implementations of the decidable operations that the proofs establish.
Provenance Chain
Francisco Varela
Principles of Biological Autonomy (1979) — three-valued re-entry calculus
Louis H. Kauffman
"Self-Reference and the Self" (Constructivist Foundations 13(1), 2017) — self-reference as eigenform
Apoth3osis Labs
11 Lean 4 modules, 972 lines, 0 sorry. Nucleus bridge, transport witness, counterexamples.
Apoth3osis Labs
Hostile audit: vacuity checks, overclaim detection, counterexample surface, ATP regression.
Apoth3osis Labs
Verified C (3 headers, 35 assertions) + safe Rust (1 crate, 10 tests). Finite witness operations only.
Related Projects
Semantic Closure in Lean 4
Rosen (M,R)-system formalization — the semantic closure operators that the MRBridge module connects to.
Computational No-Coincidence
Nucleus structure in computational hardness — another instance of Heyting gap witnessing.
Stack Theory (Bennett 2026)
Delegation bounds via Heyting nuclei — a different application of the same algebraic machinery.