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
Empirical Validation Programme
Independent of the formal synthesis, the Penumbra programme runs a deterministic Rust test harness against 21 dynamical systems spanning integrable and chaotic regimes. All experiments use pre-registered thresholds, exact permutation statistics over every combinatorial partition, and honest verdict logic: Pass, Fail, or Inconclusive. The programme ran across 5 phases and 27 experiments. Failures are permanently closed with evidence; passes survive adversarial audit.
STABLE PASSES
| Experiment | Verdict | Key Measurement |
|---|---|---|
| Bitwidth Monotonicity | Pass | Gap ratio decreases strictly with increasing bitwidth across all substrates |
| Born Ground-State Correspondence | Pass | Hydrogen 1s RMS error 0.33% (ground state only) |
| Möbius → SU(2) Emergence | Pass | Lean-verified algebraic chain connecting re-entry geometry to SU(2) |
| Wolfram Confluence-Causality Gap | Pass | Real correlation between computational depth and gap ratio |
| Binary LOSO Classifier (21 substrates) | Pass | KNN held-out-substrate accuracy 0.810, record accuracy 0.757 |
| Binary Gap Ratio (21 substrates) | Pass | Chaotic CV 0.291 < 0.30 gate; exact Welch p = 1.87 × 10⁻³ over 116,280 permutations |
PERMANENT CLOSURES
| Lane | Verdict | Reason |
|---|---|---|
| Mass Hierarchy Modulations | Fail | Required f(3)/f(2) = 0.00725, but monotone families force ≥ 1. Lean-proved impossibility. |
| Born Excited States | Fail | Detector fitted on 1s cannot produce the 2s radial node or 2p angular boundary |
| Three-Class Taxonomy | Fail | "Nested" class statistically indistinguishable from "classical" under LOSO |
| Class-Conditional Universality | Fail | Within-class CV exceeds 1.0; gap ratio separable between classes but not universal within them |
LEAN FORMAL VERIFICATION
| Module | Verdict | Contribution |
|---|---|---|
| LyapunovClassifierBoundary | Pass | Exhaustive 21-case proof that integrable/chaotic boundary is exactly the sign partition of the maximum Lyapunov exponent |
| MonotoneCouplingObstruction | Pass | Algebraic proof that monotone-increasing couplings cannot achieve f(3)/f(2) < 1, permanently closing the mass hierarchy lane |
PHASE 5 SUBSTRATE ENSEMBLE (21 SYSTEMS)
7 integrable + 14 chaotic dynamical systems. All Lyapunov exponents computed numerically, not assumed. Binary class boundary formally verified in Lean.
Methodology: Pre-registered thresholds (CV < 0.30, p < 0.01, accuracy ≥ 0.65). Exact combinatorial permutation tests over all C(21,7) = 116,280 partitions. Deterministic Rust implementation. Two independent adversarial audits with byte-identical reproduction. All results, code, and audit trail publicly available.
Companion repo: penumbra-experiments (25 Rust crates, deterministic test harness)
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