Varela Re-Entry Nucleus
Self-Reference Formalized as an Honest Heyting Algebra Nucleus Bridge
Formal Verification Certificate
All 50+ theorems machine-checked by the Lean 4 kernel with zero sorry gaps. Includes counterexample surface and ATP regression targets.
Varela Re-Entry Nucleus • Lean 4 + Mathlib • Apoth3osis Labs
The Research Arc
This project formalizes a complete research arc from Francisco Varela's 1979 Extended Calculus of Indications through to verified executable artifacts and automated theorem proving regression infrastructure.
Five Phases
1. Honest Nucleus Formalization
The crossing operation is not a nucleus (it fails monotonicity). Rather than force it, we embed the three-valued ECI carrier into a four-element ambient stage lattice and construct a genuine closure operator whose fixed-point sublocale is order-isomorphic to the ECI. This is the honest bridge: cross is not a nucleus, but the ECI arises as the fixed-point algebra of a real one.
Modules: ECI.lean, ReentryNucleus.lean, Waveforms.lean
2. Hostile Audit and Corrections
The formalization underwent hostile audit for vacuity, overclaim, and scope inflation. The Counterexamples module exposes the exact claims that fail when made too strong: not every stage is fixed, not every stage has an ECI preimage, and nonclassicality survives all transport layers.
Modules: Counterexamples.lean, Fixtures.lean
3. Transport Witness
The transport witness packages the nucleus formalization as a finite honesty oracle for the repo’s broader re-entry transport vocabulary. It does not instantiate the full abstract Genesis/OTM bridge stack. Its purpose is to provide an executable witness that future abstract bridge work can be checked against.
Modules: TransportWitness.lean, BridgeExemplar.lean
4. Genesis/OTM Finite Companions
Finite companion modules scoped to the Varela witness. Genesis companion packages stabilization/closedness equivalence. OTM companion packages reclassification vocabulary where the latent stage reclassifies to autonomous. These are finite witnesses, not claims about the full abstract bridges.
Modules: GenesisCompanion.lean, OTMCompanion.lean
5. ATP/Tooling Pack
10 named prove/refute targets for automated theorem proving regression. (M,R)-system semantic closure bridge connecting to existing selector-closure nucleus infrastructure. 40+ sanity regression examples in the test suite.
Modules: ATPTargets.lean, MRBridge.lean, Tests/Varela/Sanity.lean
What Remains Future Work
- ●Full abstract Genesis/OTM bridge: The finite companions prove local properties. The full categorical bridge connecting Varela to the abstract Genesis/OTM transport stack is not yet formalized.
- ●Higher-arity ECI extensions: The current formalization handles the three-valued carrier. Extensions to n-valued chains or non-linear lattices are scoped out.
- ●Categorical (M,R) bridge completion: The MRBridge module connects to existing infrastructure but does not yet prove the full categorical beta-b theorem for the Varela instance.
Provenance Chain
Resources
Related Projects
Semantic Closure in Lean 4
Rosen (M,R)-system formalization. The semantic closure operators that MRBridge connects to.
Stack Theory (Bennett 2026)
Delegation bounds via Heyting nuclei. A different application of the same algebraic machinery.
Computational No-Coincidence
Nucleus structure in computational hardness. Another instance of Heyting gap witnessing.