Penumbra: Machine-checked proof that every non-Boolean projection through a nucleus produces a universal, irreducible information gap. 162 files, 1,486 declarations, zero sorry. Lean 4 + Mathlib.
Formal verification framework for Neyman's Computational No-Coincidence Conjecture in Lean 4 — advice strings as Heyting algebra nucleus operators on reversible circuits
Lean 4 formalization of Bennett's Stack Theory proving hard bounds on delegation in multi-layer intelligence architectures, with novel Heyting nucleus bridge theorems
P-adic Functional Decoupling — 28 theorems verified in Lean 4. Depth-truncation nuclei, ultrametric light cones, Hamiltonian conservation, bridges to Hossenfelder no-go and Miranda dynamics.
Formally verified asymptotic safety for quantum gravity in Lean 4. RG flow as a nucleus operator, calibrated particle-physics prediction bounds, and constructive dark-matter exclusion.
Formally verified Hossenfelder no-go theorem for Poincaré-invariant spacetime networks in Lean 4. Axiom-free proof + constructive Heyting boundary non-Booleanity witness from asymptotic safety.
Varela Re-Entry Nucleus: Machine-checked formalization of self-referential re-entry as an honest Heyting algebra nucleus bridge. 11 Lean 4 modules, 972 lines, zero sorry.
Verified INT8 Quantization Gap Analysis via Heyting Algebra Nuclei — Lean 4 proofs connecting qReLU nucleus operators to the Hossenfelder no-go theorem
Add a description, image, and links to the heyting-algebra topic page so that developers can more easily learn about it.
To associate your repository with the heyting-algebra topic, visit your repo's landing page and select "manage topics."