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
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerExtended Calculus of Indications
Contributor
Francisco Varela
CNRS / University of Paris (posthumous, 1946–2001)
Core insight: Spencer-Brown’s two-valued calculus of indications admits a third value—the autonomous state—arising from self-referential re-entry. This value is a fixed point of the crossing operation while simultaneously witnessing the failure of excluded middle.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerSelf-Reference and the Self: Eigenform Theory
Contributor
Louis H. Kauffman
University of Illinois at Chicago, Department of Mathematics
The theory layer reframes Varela’s re-entry through Kauffman’s eigenform framework: self-referential entities are fixed points of recursive distinctions. The autonomous value is the eigenform of the crossing operation.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerLean 4 Nucleus Bridge Formalization
Contributor
Apoth3osis Labs
R&D Division
Machine-checked formalization in 11 modules with 50+ sorry-free theorems. Key contribution: honest nucleus bridge construction placing ECI inside a four-element ambient stage lattice with a genuine closure operator whose fixed-point sublocale is order-isomorphic to the ECI carrier.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Ontological EngineerTransport Witness and Finite Companions
Contributor
Apoth3osis Labs
R&D Division
Transport witness packaging, bridge exemplar, Genesis and OTM finite companions. These modules do not instantiate the full abstract Genesis/OTM bridge—they provide honest finite witnesses that future abstract work can be checked against.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
Ontological Engineer(M,R)-System Semantic Closure Bridge and ATP Targets
Contributor
Apoth3osis Labs
R&D Division
Bridge to Rosen (M,R)-system semantic closure operators via existing selector-closure nucleus infrastructure. 10 named ATP regression targets for automated theorem proving.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026
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.