Penumbra
The Universal Information Shadow of Non-Boolean Projection
Machine-checked proof that every non-Boolean nucleus on a Heyting algebra produces an irreducible information gap — a penumbra — and that this gap appears with identical algebraic structure across neural network quantization, spacetime geometry, fluid dynamics, matter stability, dimensional emergence, causal invariance, spinor structure, controlled system saturation, renormalization group flow, and two-clock relativistic projection.
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
162
Lean Files
Across 10 layers
1,486
Declarations
Theorems, defs, instances
733
Theorems
Machine-verified
0
Sorry Count
Zero unproved claims
16,768
Lines
Pure Lean 4
8+
Substrates
Cross-domain instantiations
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 Central Thesis
The boundary ∂ΩR — the set of elements projected but not absorbed by the nucleus — is non-empty whenever the underlying algebra is non-Boolean. This non-emptiness is the penumbra: an irreducible information shadow that cannot be eliminated by changing the nucleus, the algebra, or the domain. It is structural.
The 10-Layer Argument
Noneist Ground → Generative Emergence
Spinor Bridge (SU(2) from Re-Entry)
Heyting Gap (Hossenfelder No-Go)
Wolfram Causal Confluence
Neural Networks / Nucleus Grafting (qReLU)
Two-Clock Physics (Al-Mayahi UDT)
Fluid Undecidability (Miranda Dynamics)
PM-Bounded τ-Control
Prime Stability (Matter from Periodicity)
Asymptotic Safety (RG Fixed Points)
Cross-Cutting Connections
| ID | Connection | Layers | Key Result |
|---|---|---|---|
| A | Neural ↔ Spacetime | 2, 3, 4 | qReLU gap = Hossenfelder gap = Wolfram obstruction |
| B | Oscillation ↔ Spinor | 0, 1 | Re-entry involution carries SU(2) |
| C | τ-Clock ↔ RG Flow | 5, F | Both are nuclear projections |
| D | Fluid ↔ Control | 6, 7 | Undecidability boundary = saturation boundary |
| E | Born Rule ↔ Stability | 8 | Surviving fraction = Born probability |
| F | Prime Period ↔ Mass | 8 | Mass = trapped asymmetry at prime period > 1 |
Proof Blueprint
Representative modules from each layer. Click to expand Mathematics/Lean views. Full 162-file source available on GitHub.
Verified C Artifacts
Representative verified artifacts for core modules (Layers 2, 7, 8). The complete Lean source is the authoritative artifact; C transpilations for additional layers are available via the CAB pipeline. Provenance: Lean 4 → LambdaIR → MiniC → C.
Safe Rust Artifacts
Representative modules with memory-safe Rust and ownership semantics. Includes #[cfg(test)] modules. Additional layer transpilations available on request.
Provenance Chain
Lean 4 v4.24.0 + Mathlib v4.24.0
162 files, 733 theorems, 0 sorry
LambdaIR Extraction
Computational content preserved
MiniC Translation
4 verified C files
Safe Rust Transpilation
4 modules with tests
Archive Downloads
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.