cd-formalization¶

A Lean 4 formalization of the Creative Determinant existence theory.

What this formalizes¶

The Creative Determinant models coherent presence as a solution of the boundary value problem

\[ -\Delta\Phi = a(x)\,|\nabla\Phi| + b(x)\,\Phi - c(x)\,\Phi_+^{\,p} \quad \text{in } M, \qquad \Phi = 0 \quad \text{on } \partial M, \]

where care \(\kappa\), coherence \(\gamma\) and contradiction \(\mu\) take values in \([0,1]\), the creative drive is \(a = \kappa\gamma\mu\), \(b\) is the viability potential, the capacity satisfies \(c \geq c_0 > 0\), and \(p > 1\).

Conditional existence. Two theorems derive solutions from the hypotheses PDEInfra and SolutionOperator, which stand in for classical elliptic results that are not proved here. The assumption boundary states what each one says.
Unconditional lemmas. The algebraic, real-analytic and order-theoretic steps are proved outright. See the theorem catalog.
Finite-graph existence. For the discretization selected here, on a finite weighted graph, SemioticGraph.exists_pos_graph proves that the discrete problem has a solution positive at every interior vertex when the interior graph is connected, the principal eigenvalue of \(L - \operatorname{diag}(b)\) is negative, and \(a(x) \le \sqrt{w(x,y)}\) and \(a(y) \le \sqrt{w(x,y)}\) for every edge of positive weight between distinct interior vertices \(x\) and \(y\). Every operator and the principal eigendata are constructed. See the proof strategy.

Every module compiles under lake build --wfail, and CI checks the axioms of the selected declarations against propext, Classical.choice and Quot.sound. That check cannot see hypotheses, so it does not discharge PDEInfra.

Documentation¶

Page	Contents
Quickstart	Build, verify, project layout
Proof strategy	How each result is proved
Assumption boundary	What each hypothesis says, and what is not formalized
Theorem catalog	Statements and Lean signatures
Verification audit	Paper-to-Lean alignment and what CI checks
Changelog	Version history