From fb567346e7df9f190aa54d7df24227545179c078 Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Mon, 28 Sep 2026 13:55:13 -0500 Subject: [PATCH] docs: move documentation links to docs.projectnavi.ai The docs sites are now served at docs.projectnavi.ai; the old github.io URLs redirect there. Update site_url and the links in the README and docs. --- README.md | 4 ++-- zensical.toml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 5474f18..6054f03 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,12 @@ # Creative Determinant: Lean 4 formalization -A Lean 4 and Mathlib (v4.34.1) formalization of the existence theory in N. Spence, *The Creative Determinant: Autopoietic Closure as a Nonlinear Elliptic Boundary Value Problem with Lean 4-Verified Existence Conditions* (2026). The problem is −ΔΦ = a|∇Φ| + bΦ − c(Φ₊)ᵖ in M with Φ = 0 on ∂M, where a = κγμ and p > 1. Documentation: [project-navi.github.io/cd-formalization](https://project-navi.github.io/cd-formalization/). +A Lean 4 and Mathlib (v4.34.1) formalization of the existence theory in N. Spence, *The Creative Determinant: Autopoietic Closure as a Nonlinear Elliptic Boundary Value Problem with Lean 4-Verified Existence Conditions* (2026). The problem is −ΔΦ = a|∇Φ| + bΦ − c(Φ₊)ᵖ in M with Φ = 0 on ∂M, where a = κγμ and p > 1. Documentation: [docs.projectnavi.ai/cd-formalization](https://docs.projectnavi.ai/cd-formalization/). - **Continuum results (conditional).** `SemioticBVP.exists_isWeakCoherentConfiguration` gives a nonnegative solution when `b` is bounded above, and `SemioticBVP.exists_pos_isWeakCoherentConfiguration` one that is positive at some interior point when a supplied principal eigenvalue is negative. Both are derived from the hypotheses `PDEInfra` and `SolutionOperator`, which stand in for elliptic results not proved here; the manifold's Laplacian, gradient norm and boundary are abstract data. - **Finite graphs (proved).** For the discretization selected here, on a finite weighted graph with a Dirichlet boundary, `SemioticGraph.exists_pos_graph` gives a solution positive at every interior vertex when the interior graph is connected, the principal eigenvalue of L − diag(b) is negative, and a(x) ≤ √w(x,y) and a(y) ≤ √w(x,y) for every edge of positive weight between distinct interior vertices x and y. The operators and eigendata are constructed. The edge condition is sufficient for this proof, not claimed necessary, and holds for 0/1 weights (`SemioticGraph.exists_pos_graph_of_unweighted`). - **Supporting lemmas**, among them `spectral_characterization_1d`, `linfty_bound_algebraic`, `monotone_fixed_point_between` (Knaster–Tarski) and `scaling_uniqueness`. -The [assumption boundary](https://project-navi.github.io/cd-formalization/explanation/axiom-boundary/) page states what each hypothesis says and what is not formalized. +The [assumption boundary](https://docs.projectnavi.ai/cd-formalization/explanation/axiom-boundary/) page states what each hypothesis says and what is not formalized. ## Verify diff --git a/zensical.toml b/zensical.toml index 74d414e..8a5f3b8 100644 --- a/zensical.toml +++ b/zensical.toml @@ -5,7 +5,7 @@ name = "cd-formalization" site_name = "cd-formalization" description = "Lean 4 formalization of the Creative Determinant framework" -site_url = "https://project-navi.github.io/cd-formalization" +site_url = "https://docs.projectnavi.ai/cd-formalization" repo_url = "https://github.com/Project-Navi/cd-formalization" repo_name = "Project-Navi/cd-formalization" copyright = "Copyright 2025-2026 Nelson Spence"