CdFormal | Reservoir

Creative Determinant — Lean 4 Formalization

Formal verification of the existence theory from:

N. Spence, "The Creative Determinant: Autopoietic Closure as a Nonlinear Elliptic Boundary Value Problem with Lean 4-Verified Existence Conditions," 2026.

What is verified

Fifteen theorems and lemmas proved with zero sorry, organized in five dependency tiers:

Tier 1 — Pure mathematics (no domain axioms)

Result	Declaration	File	Topic
Spectral characterization (1D)	`spectral_characterization_1d`	`Theorems`	Algebra
Scaling algebraic contradiction	`scaling_algebraic_contradiction`	`Theorems`	Algebra
v^{p−1} ≤ b/c from PDE inequality	`rpow_le_of_mul_rpow_le`	`LinftyAlgebraic`	Real analysis
v ≤ (b/c)^{1/(p−1)}	`linfty_bound_algebraic`	`LinftyAlgebraic`	Real analysis
nextFixed ≤ super-fixed point	`OrderHom.nextFixed_le_of_le`	`MonotoneFixedPoint`	Order theory
Fixed point between sub/super	`monotone_fixed_point_between`	`MonotoneFixedPoint`	Order theory

Tier 2 — Operator lemmas (from abstract linearity/homogeneity)

Result	Declaration	File
Laplacian of zero	`laplacian_zero`	`OperatorLemmas`
Laplacian linearity	`laplacian_linear`	`OperatorLemmas`
Gradient norm of zero	`gradNorm_zero`	`OperatorLemmas`

Tier 3 — Coefficient bounds (from [0,1] field constraints)

Result	Declaration	File
a(x) nonneg	`SemioticContext.a_nonneg`	`CoefficientLemmas`
a(x) ≤ 1	`SemioticContext.a_le_one`	`CoefficientLemmas`
p − 1 > 0	`SemioticContext.p_sub_one_pos`	`CoefficientLemmas`

Tier 4 — PDE-level results (from `SemioticOperators` / `PDEInfra`)

Result	Declaration	File	Dependencies
Scaling uniqueness (kΦ impossible for k > 1)	`scaling_uniqueness`	`ScalingUniqueness`	`SemioticOperators` axioms
Existence of weak coherent configurations	`SemioticBVP.exists_isWeakCoherentConfiguration`	`Theorems`	`PDEInfra`
Nontrivial configurations	`SemioticBVP.exists_pos_isWeakCoherentConfiguration`	`Theorems`	`PDEInfra`

All definitions (semiotic manifold, BVP, operators, weak coherent configuration) are machine-checked against Mathlib.

The monotone fixed-point theorems depend only on [propext, Quot.sound] — no Classical.choice — making them candidates for constructive upstream contribution.

Axiom boundary

The PDEInfra typeclass in CdFormal/Axioms.lean packages five classical PDE results not yet in Mathlib:

Axiom	Classical source	Mathlib status
`T_compact`	Schauder estimates + Arzelà–Ascoli	Uses `IsVonNBounded` + `IsCompact` (bornological typing, credit: Aaron Lin)
`linfty_bound`	Maximum principle (Gilbarg–Trudinger)	No max. principle for manifolds
`schaefer`	Schaefer 1955	Not in Mathlib (draft issue)
`fixed_point_nonneg`	Strong maximum principle	No max. principle for manifolds
`monotone_iteration`	Amann 1976	No sub-/super-solution theory

The existence theorems explicitly carry [PDEInfra bvp solOp] so the axiom surface is visible to Lean's kernel. Run #print axioms in CdFormal/Verify.lean to confirm no sorryAx — all theorems depend only on [propext, Classical.choice, Quot.sound] (monotone fixed-point theorems use only [propext, Quot.sound]).

Building

Requires Lean 4 (v4.28.0) and Mathlib.

lake build
lake build --wfail   # fail on any sorry or warning

Project structure

CdFormal/
  Basic.lean              — Definitions (manifold, coefficients, operators, BVP)
  Axioms.lean             — PDEInfra typeclass (explicit axiom surface)
  Theorems.lean           — Existence and algebraic theorems
  OperatorLemmas.lean     — Laplacian/gradient-norm derived properties
  CoefficientLemmas.lean  — Bounds from [0,1] field constraints
  ScalingUniqueness.lean  — PDE-level scaling impossibility
  MonotoneFixedPoint.lean — Knaster-Tarski fixed point between sub/super
  LinftyAlgebraic.lean    — L∞ bound algebraic core (Paper Lemma 3.10)
  Verify.lean             — #print axioms dashboard (17 declarations)
artifacts/
  aristotle/              — Proved outputs from the Aristotle theorem prover
drafts/                   — Mathlib issue drafts + Lean proof sketches
  mathlib_issue_schaefer.md, BornologyBridge_sorry.lean
  MonotoneFixedPoint_sorry.lean, LinftyAlgebraic.lean, OperatorLemmas.lean
  ScalingUniqueness.lean, ScalingUniqueness_v2.lean, ScalingUniqueness_v3.lean

Development Process

What the author did: The original equations, proof strategy, and formalization architecture — choosing to axiomatize via PDEInfra, identifying which five classical PDE results to package, designing the typeclass hierarchy, and structuring the Schaefer → L∞ bound → existence → sub/super-solution → nontriviality proof chain — are the core intellectual contribution. These are mathematical architecture decisions that require understanding where the real difficulty lies. The underlying equations and theory are documented in the paper.

What AI tools did: Claude Opus assisted with Lean 4 syntax, Mathlib API navigation, and proof term synthesis. Aristotle (Harmonic.fun) automated proving of standalone algebraic lemmas. These roles are analogous to omega, aesop, and other proof automation — the strategy is human, the term-level search is machine-assisted.

Verification: The final arbiter is the Lean compiler, not trust:

lake build --wfail   # type-checks or it doesn't — zero sorry

Run #print axioms in CdFormal/Verify.lean to confirm the axiom surface. Every assumption is explicit in PDEInfra. Nothing is hidden.

CdFormal0.2.0