cd-formalization¶
Machine-checked existence theory for coherent presence on Riemannian manifolds.
15 theorems. Zero sorry. Five explicit axioms. CI-enforced via lake build --wfail.
What this formalizes¶
The Creative Determinant framework models coherent presence as a solution to a nonlinear elliptic boundary value problem on a compact Riemannian manifold \(M\):
where \(\Phi = 0\) on \(\partial M\), and the coefficient fields encode care (\(\kappa\)), coherence (\(\gamma\)), and contradiction (\(\mu\)).
This Lean 4 + Mathlib formalization verifies the existence theory --- the proof that nontrivial solutions exist when viability exceeds dissipation.
Theorem summary¶
| Tier | What's proved | Count | Axiom dependencies |
|---|---|---|---|
| Pure algebra | Spectral characterization, scaling contradiction | 2 | propext, Quot.sound, Classical.choice |
| Real analysis | \(bv \geq cv^p \Rightarrow v \leq (b/c)^{1/(p-1)}\) | 2 | propext, Quot.sound, Classical.choice |
| Order theory | Knaster-Tarski between sub/super-fixed points | 2 | propext, Quot.sound --- no Classical.choice |
| Operator lemmas | \(\Delta(0) = 0\), \(\Delta\) linearity, \(\|\nabla 0\| = 0\) | 3 | SemioticOperators axioms |
| Coefficient bounds | \(a(x) \geq 0\), \(a(x) \leq 1\), \(p - 1 > 0\) | 3 | SemioticContext bounds |
| PDE existence | Nonneg solutions exist (Thm 3.12), positive solutions exist (Thm 3.16), scaling uniqueness | 3 | PDEInfra typeclass |
| Total | 15 |
Key equations in Lean¶
| Paper concept | Lean definition | LaTeX |
|---|---|---|
| Creative drive | SemioticContext.a |
\(a(x) = \kappa(x)\,\gamma(x)\,\mu(x)\) |
| Viability potential | SemioticContext.canonicalViability |
\(b(x) = \kappa\gamma - \lambda\mu\) |
| BVP (V1') | SemioticBVP.equation |
\(-\Delta\Phi = a\|\nabla\Phi\| + b\Phi - c\Phi_+^p\) |
| Viability threshold | viabilityThreshold |
\(\beta^* = (\pi/L)^2 / b\) |
| L∞ bound | linfty_bound_algebraic |
\(v \leq (b/c)^{1/(p-1)}\) |
| Spectral condition | spectral_characterization_1d |
\(\lambda_1 = (\pi/L)^2 - \beta b < 0\) |
The axiom boundary¶
Five classical PDE results --- not yet in Mathlib for abstract Riemannian manifolds --- are packaged as the PDEInfra typeclass. Every theorem that depends on these axioms carries [PDEInfra bvp solOp] in its signature, making the assumption surface visible to Lean's kernel.
The axiom boundary page documents each axiom, its classical source, and its Mathlib status.
Documentation¶
| Section | What you'll find |
|---|---|
| Quickstart | Build, verify, project structure |
| Proof Strategy | How the proof chain works --- from definitions to existence |
| Axiom Boundary | The five PDEInfra axioms --- what's proved, what's assumed, and why |
| Theorem Catalog | All 15 theorems with Lean signatures and LaTeX statements |
| Verification Audit | Paper-to-Lean alignment table and axiom dependency dashboard |
| Changelog | Release history |