docs: move documentation links to docs.projectnavi.ai

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
 

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"