Penumbra
The Universal Information Shadow of Non-Boolean Projection
A 10-layer machine-checked synthesis proving that every non-Boolean nucleus on a Heyting algebra produces an irreducible information gap — the penumbra — and that this gap appears with identical algebraic structure across neural network quantization, spacetime, fluid dynamics, matter stability, dimensional emergence, causal invariance, spinor structure, control systems, and RG flow.
Formal Verification Certificate
This research has been formally verified and integrated into production systems. Every claim is backed by machine-checked proof.
Penumbra • Lean 4 + Mathlib • Apoth3osis Labs
Explore Full Proof Corpus
Interactive 3D projection of all 1,486 declarations across 8 researcher contributions. Filter by contributor to isolate their theorems, lemmas, and definitions. Hover to scan, click to lock.
The 10-Layer Argument
Noneist Ground → Generative Emergence
Golden ratio, 3D closure, 4D barrier, π·φ propagation
Spinor Bridge (SU(2) from Re-Entry)
Oscillator-spinor equivalence, CG coupling, dimensionality
Heyting Gap (Hossenfelder No-Go)
Non-Boolean → non-empty boundary, gapNonZero
Wolfram Causal Confluence
Confluence ⊥ causal invariance, shared fixed-point obstruction
Neural Networks / Nucleus Grafting (qReLU)
qReLU as nucleus on discrete lattices, quantization gap = Heyting gap
Two-Clock Physics (Al-Mayahi UDT)
τ-projection as nucleus, mass generation gap
Fluid Undecidability (Miranda Dynamics)
NS trajectory undecidable, periodic orbit nucleus
PM-Bounded τ-Control
Saturation as nucleus, bounded control signals
Prime Stability (Matter from Periodicity)
Prime period → stability, electron as terminal
Asymptotic Safety (RG Fixed Points)
RG flow as nucleus, β = 0 at Ω_R
Resources
GitHub
162 Lean 4 files, independently verifiable via lake build
Paper → Proof → Code
Interactive proof blueprint with KaTeX, C, and Rust artifacts
Build & Verify
git clone https://github.com/Abraxas1010/penumbra-lean cd penumbra-lean/lean lake build
Heritage
Heritage researchers whose published work has been independently formalized, verified, and connected through this synthesis. These researchers have not been consulted or affiliated unless otherwise noted on their individual project pages.
Al-Mayahi
Two-Clock Physics
Veselov
Number Theory
Miranda
Fluid Dynamics
Hossenfelder
Foundations of Physics
Eichhorn & Piskunov
Quantum Gravity
Wolfram
Computational Physics
Penrose
Mathematical Physics
Tzouvaras
Set Theory
MENTAT Contribution Certificates
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Nucleus-as-Universal-Gap Thesis
Contributor
Goodman
Apoth3osis Labs
The conceptual insight that the Heyting algebra nucleus operator generates a structurally identical information gap across every non-Boolean projection domain, and that this gap can be formally unified across neural networks, spacetime, fluid dynamics, matter stability, causal invariance, control systems, and renormalization group flow.
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Complete 10-Layer Lean 4 Formalization
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of the full Penumbra synthesis. 162 files, 1,486 declarations, 733 theorems/lemmas, zero sorry/admit. Mathlib v4.24.0 as sole dependency. All declarations independently verifiable via lake build.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
8-Substrate Cross-Domain Bridge Verification
Contributor
Apoth3osis Labs
R&D Division
Formal verification that the Heyting gap instantiation is structurally identical across all 8 substrates. Each bridge proves that two or more domain-specific nucleus instances share the same fixed-point obstruction, establishing the gap as universal rather than domain-specific.
Builds Upon
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Union Dipole Theory — Two-Clock Framework
Contributor
Al-Mayahi
Union Dipole Theory Foundation
The τ-clock framework projecting internal time onto observer-local (t, x) coordinates. Independently formalized and connected to the nucleus structure in Layer 5.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Turing Completeness of Fluid Dynamics
Contributor
Miranda
The insight that Navier-Stokes dynamics encode universal computation, making trajectory prediction and periodicity detection undecidable. Formalized in Layer 6.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Superdeterminism No-Go Structure
Contributor
Hossenfelder
Frankfurt Institute for Advanced Studies
The no-go framework for spacetime networks establishing non-Boolean boundaries. Formalized and connected to the nucleus boundary in Layer 2.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Meinongian Noneist Foundations
Contributor
Tzouvaras
Noneist theory of non-existent objects providing the oscillation-from-Nothing framework formalized in Layer 0.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Asymptotic Safety Program
Contributor
Eichhorn, Piskunov
The asymptotic safety conjecture for quantum gravity and Wolfram multiway causal invariance analysis. Formalized in Cross-cutting F and Layer 3 respectively.
Governed by MENTAT-CA-001 v1.0 · March 2026
Related Projects
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.