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