cff-version: 1.2.0
title: "Creative Determinant: Lean 4 Formalization"
message: "If you use this formalization, please cite it using the metadata from this file."
type: software
authors:
  - family-names: Spence
    given-names: Nelson
    email: nelson@projectnavi.ai
    affiliation: Project Navi LLC
repository-code: "https://github.com/Project-Navi/cd-formalization"
abstract: >-
  Lean 4 and Mathlib formalization of the Creative Determinant boundary
  value problem. Existence of a nonnegative solution, and of one that is
  positive at an interior point when a principal eigenvalue is negative,
  is derived from explicit hypotheses (the PDEInfra class and a solution
  operator) that stand in for classical elliptic results not proved here.
  For a discretization on finite weighted graphs selected for this
  formalization, existence of a solution positive at every interior vertex
  is proved outright under connectivity, spectral and edge-weight
  conditions. Supporting algebraic, real-analytic and order-theoretic
  lemmas are proved outright.
keywords:
  - Lean 4
  - Mathlib
  - formal verification
  - theorem proving
  - elliptic PDE
  - fixed-point theorems
  - autopoiesis
license: Apache-2.0
version: "0.2.0"
date-released: "2026-03-06"
preferred-citation:
  type: report
  authors:
    - family-names: Spence
      given-names: Nelson
  title: "The Creative Determinant: Autopoietic Closure as a Nonlinear Elliptic Boundary Value Problem with Lean 4-Verified Existence Conditions"
  year: 2026
  institution:
    name: Project Navi LLC
  address: Austin, Texas