diff --git a/HeatEquation_Step1.lean b/HeatEquation_Step1.lean new file mode 100644 index 0000000..0e51f8f --- /dev/null +++ b/HeatEquation_Step1.lean @@ -0,0 +1,252 @@ +/- + HeatEquation_Step1.lean + ------------------------------------------------------------------ + Formal companion to: + "Formal Verification of the Heat Equation: Formulation, + Discretization, and Conditioning in Lean 4, with an Application + to Compression Operators." (heat_equation_monograph.pdf) + + Model (paper, Part I). One backward-Euler step of the 1D heat + equation u_t = u_xx on (0,1), u(0,t)=u(1,t)=0, reduces to the + elliptic problem + w - τ w'' = u_prev on (0,1), w(0) = w(1) = 0, + with weak form: find w ∈ H¹₀(0,1) such that + a_τ(w,v) = ⟨f,v⟩ for all v ∈ H¹₀(0,1). + + STATUS. This file mirrors the paper's own §17 "Honest Accounting" + ledger exactly, declaration for declaration: + · H¹₀(0,1) and the bilinear form a_τ are axiom-backed placeholders. + The paper is explicit that constructing the real H¹₀(0,1) Hilbert + space is the genuinely hard part of Part I; everything after it + is comparatively mechanical (Remark 1.1). + · The discrete Laplacian A_h (Parts II-III) is a real, concrete + object — an explicit tridiagonal matrix over ℝ^N — so those + results are stated with no placeholder needed. + · Part V's compression non-injectivity result (Remark 21.7 of the + *companion* helix paper's pattern, applied here per this paper's + own Remark 21.7) is likewise concrete and is proved outright + below, not left as sorry, since the paper itself calls it + "close to mechanical." + · The H-theorem (Prop. 20.1) needs no H¹₀ machinery at all — the + paper's own Remark 20.2 checks it on the explicit solution + u(x,t) = sin(πx) e^{-π²t}; that check is proved outright below. + + This file has NOT been machine-checked (no toolchain available in + the authoring environment). A Mathlib build is required to verify + every declaration, sorry-tagged or not. + + TRACKED ISSUES (mirror of AXLE issue tracker; §, Prop/Thm numbers + refer to the monograph): + #E1 a_coercive (Part I, Prop. 3.1) + #E2 a_bounded (Part I, Prop. 3.2) + #E3 weak_solution_exists_unique (Part I, Thm. 3.3 — needs exact + Lax–Milgram API surface) + #E4 truncation_error (Part II, Prop. 7.1 — Taylor + remainder, needs Mathlib's + taylor_mean_remainder family) + #E5 energy_stability (Part II, Prop. 8.1 — PosSemidef + spectral bound on Ah) + #E6 lax_equivalence_specialized (Part II, Thm. 9.1 — depends on + #E4, #E5) + #E7 discreteLaplacian_eigenpairs (Part III, Prop. 12.1 — Toeplitz + diagonalisation) + #E8 conditioning_bound (Part III, Thm. 13.1 — depends + on #E7) + ------------------------------------------------------------------ +-/ +import Mathlib + +noncomputable section +open Real Filter Topology BigOperators + +namespace HeatEquationStep1 + +/-! ## Part I — Continuous formulation: H¹₀(0,1), weak form, well-posedness -/ + +/-- **Axiom-backed placeholder** for H¹₀(0,1) (paper, Remark 1.1). A full + Lean construction of H¹₀(0,1) as a complete inner-product space is its + own formalization milestone; Mathlib's `MeasureTheory` and + `Analysis.Calculus.FDeriv` machinery supplies the pieces (weak + derivatives, L² norms) but assembling them into the right complete + Hilbert space is real work, deliberately deferred here so downstream + statements typecheck. -/ +axiom H10 : Type + +axiom H10_normedAddCommGroup : NormedAddCommGroup H10 +attribute [instance] H10_normedAddCommGroup + +axiom H10_innerProductSpace : InnerProductSpace ℝ H10 +attribute [instance] H10_innerProductSpace + +axiom H10_completeSpace : CompleteSpace H10 +attribute [instance] H10_completeSpace + +/-- **Axiom-backed placeholder** for the bilinear form + a_τ(w,v) = ∫ w'v' + τ⁻¹ ∫ wv (paper, Remark 2.1). Recorded abstractly + rather than as the literal integral, since the literal form requires + the real H¹₀(0,1) construction above. -/ +axiom a (τ : ℝ) : H10 →L[ℝ] H10 →L[ℝ] ℝ + +/-- **Issue #E1.** Coercivity of a_τ (paper, Prop. 3.1): a_τ(w,w) ≥ α‖w‖². + Once `H10` and `a` carry real definitions this is a two-line + computation (`a_τ(w,w) = ‖w'‖² + τ⁻¹‖w‖² ≥ min(1,τ⁻¹)‖w‖²_{H¹}`, no + Poincaré inequality needed — see the paper's proof sketch). -/ +theorem a_coercive (τ : ℝ) (hτ : 0 < τ) : + ∃ α : ℝ, 0 < α ∧ ∀ w : H10, α * ‖w‖ ^ 2 ≤ a τ w w := by + sorry -- AXLE #E1 + +/-- **Issue #E2.** Boundedness of a_τ (paper, Prop. 3.2), by Cauchy–Schwarz + on each of the two integrals defining a_τ. -/ +theorem a_bounded (τ : ℝ) (hτ : 0 < τ) : + ∃ C : ℝ, 0 < C ∧ ∀ w v : H10, |a τ w v| ≤ C * ‖w‖ * ‖v‖ := by + sorry -- AXLE #E2 + +/-- **Issue #E3.** Well-posedness of one backward-Euler step (paper, + Thm. 3.3), immediate from `a_coercive`/`a_bounded` and Lax–Milgram. + The only real risk once `H10`/`a` are concrete is matching the exact + Mathlib `IsCoercive`/`LaxMilgram` API surface (paper, Remark 3.4). -/ +theorem weak_solution_exists_unique (τ : ℝ) (hτ : 0 < τ) (f : H10) : + ∃! w : H10, a τ w = fun v => ⟪f, v⟫_ℝ := by + sorry -- AXLE #E3 + +/-! ## Part II — Discretization: the discrete Laplacian, consistency, stability -/ + +/-- The discrete Laplacian A_h on a mesh of `N` interior points with + spacing `h`, as the concrete symmetric tridiagonal matrix of paper, + §6: `2/h²` on the diagonal, `-1/h²` on the two off-diagonals. -/ +def Ah (N : ℕ) (h : ℝ) : Matrix (Fin N) (Fin N) ℝ := + Matrix.of fun i j => + if i = j then 2 / h ^ 2 + else if (i : ℕ) + 1 = (j : ℕ) ∨ (j : ℕ) + 1 = (i : ℕ) then -1 / h ^ 2 + else 0 + +/-- `Ah` is symmetric by construction (the off-diagonal adjacency + condition is already symmetric in `i`, `j`). -/ +theorem Ah_isSymm (N : ℕ) (h : ℝ) : (Ah N h).IsSymm := by + unfold Matrix.IsSymm Ah + ext i j + simp only [Matrix.transpose_apply, Matrix.of_apply] + by_cases hij : i = j + · simp [hij] + · simp [hij, Ne.symm hij, or_comm] + +/-- **Issue #E4.** Truncation error of the central difference (paper, + Prop. 7.1): for `u ∈ C⁴`, the central-difference approximation to + `u''(xᵢ)` has error `h²/12 · u⁽⁴⁾(ξᵢ)` for some `ξᵢ` in the stencil. + Mechanical once the right Mathlib `taylor_mean_remainder` lemma is + located (paper, Remark 7.2). -/ +theorem truncation_error (u : ℝ → ℝ) (hu : ContDiff ℝ 4 u) (x h : ℝ) (hh : 0 < h) : + ∃ ξ ∈ Set.Icc (x - h) (x + h), + (u (x - h) - 2 * u x + u (x + h)) / h ^ 2 - deriv (deriv u) x + = h ^ 2 / 12 * (deriv^[4] u) ξ := by + sorry -- AXLE #E4 + +/-- **Issue #E5.** Energy stability of backward Euler (paper, Prop. 8.1): + `Ah` is positive semidefinite, so `I + τ·Ah` has all eigenvalues ≥ 1 + and the backward-Euler update `(I + τ·Ah)⁻¹` is non-expansive in the + Euclidean norm, uniformly in `h`. Direct from `Matrix.PosSemidef` + facts about `Ah` once its tridiagonal structure is set up in + Mathlib's matrix library (paper, Remark 8.2) — no exotic machinery + beyond the spectral theorem for symmetric real matrices. -/ +theorem energy_stability (N : ℕ) (h : ℝ) (hh : 0 < h) : (Ah N h).PosSemidef := by + sorry -- AXLE #E5 + +/-- **Issue #E6.** Lax equivalence, specialized to this one scheme and PDE + (paper, Thm. 9.1): consistency (`truncation_error`) together with + stability (`energy_stability`) implies convergence at rate `O(h²)`. + The paper is explicit that the *general* Lax equivalence theorem is a + separate, larger project and out of scope here (Remark 9.2). -/ +theorem lax_equivalence_specialized : True := by + trivial + -- AXLE #E6: full statement depends on #E4 and #E5 and the not-yet-real + -- H10/a of Part I; recorded as a placeholder obligation, not yet typed. + +/-! ## Part III — Conditioning analysis -/ + +/-- **Issue #E7.** Closed-form eigenpairs of `Ah` (paper, Prop. 12.1): + `λ_k = (4/h²) sin²(kπh/2)` with eigenvector `(v_k)ᵢ = sin(kπ·i·h)`. + A product-to-sum identity away from being mechanical (paper, proof + sketch). -/ +theorem discreteLaplacian_eigenpairs (N : ℕ) (h : ℝ) (hh : 0 < h) (k : Fin N) : + ∃ v : Fin N → ℝ, v ≠ 0 ∧ + (Ah N h).mulVec v = (4 / h ^ 2 * Real.sin (k * π * h / 2) ^ 2) • v := by + sorry -- AXLE #E7 + +/-- **Issue #E8.** The `κ(Ah) ≤ C/h²` conditioning bound (paper, + Thm. 13.1): `κ(Ah) = sin²(Nπh/2)/sin²(πh/2) = Θ(h⁻²)` as `h → 0`. + A direct consequence of `discreteLaplacian_eigenpairs`. -/ +theorem conditioning_bound : True := by + trivial + -- AXLE #E8: depends on #E7 for the closed-form spectrum; the Θ(h⁻²) + -- asymptotic statement itself is not yet typed against a concrete + -- `κ` definition. + +/-! ## Part V — The reverse direction -/ + +/-- **H-theorem, concrete check** (paper, Prop. 20.1 / Remark 20.2). On + the exact solution `u(x,t) = sin(πx) e^{-π²t}`, the energy + `H(t) = ∫₀¹ u(x,t)² dx = ½ e^{-2π²t}` decays monotonically. This is + exactly the paper's own symbolic verification (Remark 20.2), and, + unlike Parts I–III, needs no `H10` placeholder: it is a concrete + calculus fact about the closed-form energy `H`, provable outright. -/ +theorem H_heat_deriv (t : ℝ) : + HasDerivAt (fun s : ℝ => (1 / 2 : ℝ) * Real.exp (-2 * π ^ 2 * s)) + (-(π ^ 2) * Real.exp (-2 * π ^ 2 * t)) t := by + have h1 : HasDerivAt (fun s : ℝ => -2 * π ^ 2 * s) (-2 * π ^ 2) t := by + simpa using (hasDerivAt_id t).const_mul (-2 * π ^ 2) + have h2 := h1.exp + have h3 := h2.const_mul (1 / 2 : ℝ) + convert h3 using 1 + ring + +/-- Corollary: the energy is strictly decreasing whenever `π² ≠ 0`, i.e. + always — matching the paper's `dH/dt ≤ 0`, strict away from the zero + solution (paper, Prop. 20.1). -/ +theorem H_heat_strictly_decreasing (t : ℝ) : + deriv (fun s : ℝ => (1 / 2 : ℝ) * Real.exp (-2 * π ^ 2 * s)) t < 0 := by + rw [(H_heat_deriv t).deriv] + have : (0:ℝ) < Real.exp (-2 * π ^ 2 * t) := Real.exp_pos _ + nlinarith [Real.pi_pos] + +/-- **Compression non-injectivity** (paper, Remark 21.7 / the companion + helix paper's Prop. 21.3 pattern). `PiN N` is the Galerkin truncation + to the first `N` sine coefficients; `sineMode k` names `sin(kπx)` in + the (axiomatised) ambient `L²(0,1)`. The kernel element + `sin((N+1)πx)` witnesses non-injectivity directly, exactly as the + paper's Remark 21.7 describes ("close to mechanical") — proved + outright below, not left as `sorry`. -/ +axiom L2 : Type +axiom L2_addCommGroup : AddCommGroup L2 +attribute [instance] L2_addCommGroup + +/-- The Galerkin projection onto the first `N` sine coefficients, as an + additive homomorphism (linearity is exactly what the paper's + reconstruction argument, Cor. 21.4, needs). -/ +axiom PiN (N : ℕ) : L2 →+ (Fin N → ℝ) + +/-- `sineMode k` names the L² function `sin(kπx)`. -/ +axiom sineMode (k : ℕ) : L2 + +axiom sineMode_ne_zero (k : ℕ) : sineMode k ≠ 0 + +/-- The `(N+1)`-th sine mode lies in the kernel of the truncation to the + first `N` modes — orthogonality of the sine basis, paper Prop. 21.3. -/ +axiom sineMode_mem_kernel (N : ℕ) : PiN N (sineMode (N + 1)) = 0 + +theorem compression_not_injective (N : ℕ) : ¬ Function.Injective (PiN N) := by + intro hinj + have h0 : sineMode (N + 1) = 0 := by + apply hinj + rw [sineMode_mem_kernel, map_zero] + exact sineMode_ne_zero (N + 1) h0 + +/-- Corollary (paper, Cor. 21.4): the fiber of `PiN N` over any point is + not a singleton — reconstruction from discrete data is genuinely + underdetermined, not merely difficult. -/ +theorem reverse_direction_underdetermined (N : ℕ) : + ∃ w : Fin N → ℝ, ∃ u v : L2, PiN N u = w ∧ PiN N v = w ∧ u ≠ v := by + sorry -- AXLE: direct consequence of compression_not_injective + a + -- witness u in the domain; needs L2's Zero/AddGroup API to + -- name `u := 0`, `v := sineMode (N+1)`, `w := 0` concretely. + +end HeatEquationStep1 diff --git a/HelixToyModel.lean b/HelixToyModel.lean new file mode 100644 index 0000000..e13bd5b --- /dev/null +++ b/HelixToyModel.lean @@ -0,0 +1,143 @@ +/- + HelixToyModel.lean + ------------------------------------------------------------------ + Formal companion to: + "A Contact-Geometric Toy Model on the Solid Cylinder: + Transverse Stability, Closure-Dependent Escape, Degenerate Hopf + Structure, and a Cosmological No-Go." + + Model (see paper, eq. (2)): + ṙ = f(r)(1 - e^{-z}), θ̇ = 1, ż = 1, + with closure conditions f(1)=0, f'(1)=-2, f(r)(r-1)<0 for r>0, r≠1. + Transverse linearisation about Γ={r=1}, ε := r-1 : + ε̇ = 2 ε (e^{-z} - 1), z = z₀ + t. (paper eq. (5)) + + STATUS. This file is structured against Lean 4 / Mathlib4. The + arithmetic / sign lemmas (§2) are written to compile. The analytic + results (closed-form ODE check, Lyapunov limit, no-go integral) are + stated precisely and left as `sorry`, tracked below as AXLE-style + issues. It has NOT been machine-checked in the authoring environment + (no toolchain available there); a Mathlib build is required to verify. + + TRACKED ISSUES (mirror of AXLE issue tracker): + #H1 epsSol_satisfies_ode (calc via deriv_exp + chain rule) + #H2 lyapunov_exponent_eq (l'Hôpital / boundedness of correction) + #H3 nogo_attractor_to_botinf (∫ c → -2 ⇒ H → -∞) + ------------------------------------------------------------------ +-/ +import Mathlib + +noncomputable section +open Real Filter Topology + +namespace HelixToyModel + +/-! ## §1 The transverse linear solution (paper, Thm. 1) -/ + +/-- Closed-form transverse deviation, paper eq. (6): + ε(t) = ε₀ · exp(-2t + 2 e^{-z₀}(1 - e^{-t})). -/ +def epsSol (ε₀ z₀ t : ℝ) : ℝ := + ε₀ * Real.exp (-2 * t + 2 * Real.exp (-z₀) * (1 - Real.exp (-t))) + +/-- Instantaneous transverse rate ρ(z) = 2(e^{-z} - 1) (paper, Thm. 2). -/ +def transRate (z : ℝ) : ℝ := 2 * (Real.exp (-z) - 1) + +/-- **Issue #H1.** The closed form solves the linear ODE ε̇ = ρ(z₀+t)·ε. -/ +theorem epsSol_satisfies_ode (ε₀ z₀ t : ℝ) : + deriv (fun s => epsSol ε₀ z₀ s) t + = transRate (z₀ + t) * epsSol ε₀ z₀ t := by + sorry -- AXLE #H1 : structurally routine (deriv_exp, chain rule, exp_neg) + +/-- **Issue #H2.** The Lyapunov exponent equals -2 for any nonzero seed: + the e^{-z} modulation is integrable along the flow, so contributes a + bounded additive term to log|ε| and cannot change the rate. -/ +theorem lyapunov_exponent_eq (ε₀ z₀ : ℝ) (h : ε₀ ≠ 0) : + Tendsto (fun t => Real.log |epsSol ε₀ z₀ t / ε₀| / t) atTop (𝓝 (-2)) := by + sorry -- AXLE #H2 : log|ε/ε₀| = -2t + 2e^{-z₀}(1-e^{-t}); divide by t → -2 + +/-! ## §2 The neutral line z = 0 (paper, Thm. 2) — fully proved -/ + +/-- For z < 0 the transverse rate is strictly positive (repelling). -/ +theorem transRate_pos {z : ℝ} (h : z < 0) : 0 < transRate z := by + have h1 : (1 : ℝ) < Real.exp (-z) := by + have : (0 : ℝ) < -z := by linarith + calc (1 : ℝ) = Real.exp 0 := (Real.exp_zero).symm + _ < Real.exp (-z) := by exact Real.exp_lt_exp.mpr this + have : 0 < Real.exp (-z) - 1 := by linarith + unfold transRate; linarith + +/-- On the neutral line z = 0 the transverse rate vanishes. -/ +theorem transRate_zero : transRate 0 = 0 := by + unfold transRate; simp + +/-- For z > 0 the transverse rate is strictly negative (attracting). -/ +theorem transRate_neg {z : ℝ} (h : 0 < z) : transRate z < 0 := by + have h1 : Real.exp (-z) < 1 := by + have : (-z : ℝ) < 0 := by linarith + calc Real.exp (-z) < Real.exp 0 := Real.exp_lt_exp.mpr this + _ = 1 := Real.exp_zero + have : Real.exp (-z) - 1 < 0 := by linarith + unfold transRate; linarith + +/-- Sign trichotomy: the neutral line z = 0 is the unique stability reversal. -/ +theorem neutral_line_trichotomy (z : ℝ) : + (z < 0 → 0 < transRate z) ∧ (z = 0 → transRate z = 0) ∧ + (0 < z → transRate z < 0) := + ⟨transRate_pos, fun h => by subst h; exact transRate_zero, transRate_neg⟩ + +/-! ## §3 Degenerate Hopf at the axis (paper, Thm. 5) — algebraic core -/ + +/-- Linear coefficient λ(z) = 1 - e^{-z} at the axis r = 0. -/ +def lam (z : ℝ) : ℝ := 1 - Real.exp (-z) + +/-- Cubic (first Lyapunov) coefficient a(z) for the cubic closure equals λ(z); + they coincide, which is the source of the degeneracy. -/ +def aCoeff (z : ℝ) : ℝ := 1 - Real.exp (-z) + +/-- **Degeneracy identity.** For the cubic closure the pinned cycle radius is + r* = √(λ/a) = 1 for all z with λ(z) ≠ 0, since λ = a. Here we record the + coefficient identity a = λ, from which r*² = 1. -/ +theorem hopf_degenerate_pinned (z : ℝ) : aCoeff z = lam z := rfl + +/-- Consequently, wherever λ(z) ≠ 0, the squared amplitude λ/a equals 1. -/ +theorem cycle_radius_pinned {z : ℝ} (hz : lam z ≠ 0) : lam z / aCoeff z = 1 := by + rw [hopf_degenerate_pinned]; exact div_self hz + +/-! ## §4 The contact no-go (paper, Thm. 7) -/ + +/- Under θ̇ ≡ 1 and θ-independence, the contact Hamilton equations give + ż = H(z) := -g(z) and transverse rate c(z) := -g'(z). + We encode the *locking identity* c = H' and the *mutual-exclusivity* + consequence. We take H, c as the primitive data with H = -g, c = -g'. -/ + +/-- **Locking identity** (paper eq. (17)): with H = -g and c = -g', + one has c(z) = H'(z) for every z, provided g is differentiable. -/ +theorem locking_identity (g : ℝ → ℝ) (hg : Differentiable ℝ g) : + ∀ z, (fun z => -deriv g z) z = deriv (fun z => - g z) z := by + intro z + simp [deriv.neg (hg z)] + +/-- **Issue #H3 / No-go (clean direction).** If the transverse rate c tends to + -2 (a genuine attractor) and c = H', then the expansion rate H is unbounded + below; in particular H does not converge to any positive constant, so a + de Sitter (finite positive-limit) rate is impossible. -/ +theorem nogo_attractor_not_deSitter + (H c : ℝ → ℝ) (hlock : ∀ z, c z = deriv H z) + (hattr : Tendsto c atTop (𝓝 (-2))) : + Tendsto H atTop atBot := by + sorry -- AXLE #H3 : H(z) = H(z₀) + ∫_{z₀}^z c , integrand → -2 ⇒ H → -∞ + +/-- Corollary (mutual exclusivity, contrapositive form): a transverse attractor + excludes a positive finite-limit expansion rate on (M, α). -/ +theorem attractor_excludes_deSitter + (H c : ℝ → ℝ) (hlock : ∀ z, c z = deriv H z) + (hattr : Tendsto c atTop (𝓝 (-2))) + (L : ℝ) (hL : 0 < L) : ¬ Tendsto H atTop (𝓝 L) := by + intro hHL + have hbot : Tendsto H atTop atBot := nogo_attractor_not_deSitter H c hlock hattr + -- a function cannot tend to a finite limit and to -∞ simultaneously + exact absurd (hHL.mono_right atBot_le_nhds ▸ hHL) (by + -- disjointness of 𝓝 L and atBot at atTop + sorry) -- AXLE #H3b : atBot and 𝓝 L are disjoint filters (nontrivial base) + +end HelixToyModel diff --git a/differential-equations/ch-box-domain-lift.html b/differential-equations/ch-box-domain-lift.html new file mode 100644 index 0000000..23a002d --- /dev/null +++ b/differential-equations/ch-box-domain-lift.html @@ -0,0 +1,160 @@ + + + + + +Lifting to a Box Domain (2D/3D) — Principia Orthogona, Book 6 + + + +
+ +
Principia Orthogona  ·  Book 6  ·  Differential Equations
+ +
+ Elliptic / Poisson Foundations + → + Heat Equation + → + Lifting to a Box Domain + → + Helix Toy Model + → + The Cosmic No-Go + → + A Nonlinear Reaction-Diffusion Fold +
+ +
+
Ah(2D) = Ah ⊗ I + I ⊗ Ah
+
the discrete lift, exactly
+
+ +

Lifting to a Box Domain (2D/3D)

+
the continuous side is a real, checkable question; the discrete side is already mechanical
+ +
+ +

+ Book 6's first three chapters all fixed d=1 deliberately. + The question this chapter takes on is whether that was a genuine + simplification or just a starting point — and the honest answer + splits in two, one half settled here, one half still open pending an + actual compile. +

+ +

The discrete side: mechanical, verified this session

+

+ The heat equation chapter's discrete Laplacian Ah + (Part II) is the standard 1D tridiagonal matrix. Its two-dimensional + analogue on an N×N grid — the 5-point stencil + finite-difference Laplacian on the box (0,1)² — is + not a new object requiring new machinery. It is exactly the + Kronecker sum of the same 1D matrix with itself: +

+
Ah(2D) = Ah ⊗ IN + IN ⊗ Ah,
+

+ and because Kronecker sums of symmetric matrices diagonalize in the + tensor-product eigenbasis, the eigenvalues lift by simple addition: + every 2D eigenvalue is a sum of two 1D eigenvalues from the heat + equation chapter's own Prop. 12.1, +

+
λk,l = λk + λl = (4/h²)[sin²(kπh/2) + sin²(lπh/2)].
+ +
Verified this session (numpy, N=6 grid, exact eigendecomposition, + not assumed from the algebra alone): + + max |eigenvalues(A_h^2D) - {lambda_k + lambda_l : all pairs}| = 2.8e-13 + + -- i.e. exact agreement to machine precision. + + Conditioning scaling, N = 4, 8, 16, 32, 48, 64: + h: 0.2000 0.1111 0.0588 0.0303 0.0204 0.0154 + kappa: 9.47 32.16 116.46 440.69 972.42 1711.66 + + Fitted log-log slope: -2.0224 + (heat equation chapter's own 1D result, Thm 13.1: -2.016)
+ +

+ The conditioning bound is the genuinely interesting fact here: despite + moving from 1 to 2 dimensions, κ(Ah(2D)) + = Θ(h−2) — the same exponent as the 1D + case, not h−4 or some dimension-dependent + rate. Iterative solver cost still scales as O(h−1) + CG iterations regardless of dimension, for this discretization. This + is not obvious in advance; it falls directly out of the Kronecker + structure once the eigenvalues are additive. +

+ +

The continuous side: a real, still-open question

+

+ The harder half is whether the heat equation's Part I — the + H²₀(0,1) construction currently sitting behind an + axiom — lifts as cleanly. The reconnaissance into Scott Armstrong + and Julia Kempe's DeGiorgi Sobolev-space library found + real reason for optimism: their core definitions + (MemW1p, MemW1pWitness, MemW01p, + MemH01) are stated for Ω : Set E with + E := EuclideanSpace ℝ (Fin d) and d a fully + generic variable — no ball, no d ≥ 3 restriction + anywhere in that layer. A scratch test + (degiorgi-sobolev-scratch/DeGiorgiSobolevScratch/BoxDomainTest.lean) + applies their own memW01p_of_contDiff_hasCompactSupport_subset + lemma directly to a 2D box domain and to the exact 1D interval this + corpus already uses, producing two theorems + (boxBump2D_memH01, intervalBump1D_memH01) + that are not sorry — they are real applications of + the real, fetched lemma signature. +

+

+ That test has not been compiled. It is a strong, source-grounded + reason to expect the lift works, not a proof that it does — + the scratch project needs an actual lake build, on a + separate Lean/Mathlib pin (v4.29.0-rc6) from this repo's own + (v4.14.0), which has not yet been run. Until it is, this chapter's + continuous half stays exactly where the reconnaissance left it: + plausible and specific, not confirmed. +

+ + + + + + + +
StatementStatusNotes
2D discrete Laplacian as Kronecker sumverified numericallyExact to machine precision against the 1D eigenvalue formula; not yet a Lean theorem
κ(Ah(2D)) = Θ(h−2)verified numericallyFitted slope −2.022 across six mesh sizes, matching the 1D result
MemH01 domain-genericity (box, 2D and 1D)written, not compiledReal applications of DeGiorgi's own lemma; pending lake build
Full Parts I–III lift to 2D/3Dnot startedDepends on the compile above; the discrete half (this chapter) is ready to receive it
+ +
+ ← Elliptic / Poisson Foundations + The Wave Equation → +
+ +
+ + diff --git a/differential-equations/ch-cosmic-no-go.html b/differential-equations/ch-cosmic-no-go.html new file mode 100644 index 0000000..21cb150 --- /dev/null +++ b/differential-equations/ch-cosmic-no-go.html @@ -0,0 +1,255 @@ + + + + + +The Cosmic No-Go — Principia Orthogona, Book 6 + + + +
+
+
+ +
Principia Orthogona  ·  Book 6  ·  Differential Equations
+ +
+ Helix Toy Model + → + Neutral Line + → + Escape Basin + → + Degenerate Hopf + → + The Cosmic No-Go +
+ +
+
c(z) = H′(z)
+
the locking identity
+
+ +

The Cosmic No-Go

+
a transverse attractor and a de Sitter expansion rate cannot coexist
+ +
+ +

+ Under any contact-Hamiltonian flow with constant rotation, the transverse + contraction rate is rigidly locked to the derivative of the cosmic + expansion rate. Push the transverse rate toward a genuine attractor + (μ → −2) and the expansion rate is forced unbounded + below — a structural obstruction, not a gap waiting to be closed. + The coupling that makes this model a faithful relaxation system + is exactly what makes it a poor expansion model. The kinematic + correspondence to de Sitter cosmology (ż = H, e−z + ∝ a−1) is genuine but strictly kinematic: it has no + matter or radiation era, and the correction it carries corresponds to an + equation of state matching neither. +

+ +

Where this sits in a wider effort

+ +

+ This chapter's formalization work is one small corner of a much larger, + live effort to bring hard analysis into Lean 4. Worth knowing about + independent of anything here: Scott Armstrong and Julia Kempe's 2026 + formalization of De Giorgi–Nash–Moser elliptic regularity + theory — the first proof-assistant Sobolev-space library built from + weak derivatives at this scale, sorry-free and axiom-free beyond Lean and + Mathlib itself. See + arXiv:2604.05984 + and github.com/scottnarmstrong/DeGiorgi. + Where our differential-equations line and theirs overlap — weak + derivatives, Sobolev witnesses, well-posedness on a domain — is a + real seam worth watching, not a claim of collaboration. +

+ +

In this chapter's corpus

+ + +
+ ← Degenerate Hopf + A Nonlinear Reaction-Diffusion Fold → +
+ +
+ + diff --git a/differential-equations/ch-elliptic-poisson-foundations.html b/differential-equations/ch-elliptic-poisson-foundations.html new file mode 100644 index 0000000..d56321f --- /dev/null +++ b/differential-equations/ch-elliptic-poisson-foundations.html @@ -0,0 +1,175 @@ + + + + + +Elliptic / Poisson Foundations — Principia Orthogona, Book 6 + + + +
+ +
Principia Orthogona  ·  Book 6  ·  Differential Equations
+ +
+ Elliptic / Poisson Foundations + → + Heat Equation + → + Helix Toy Model + → + The Cosmic No-Go + → + A Nonlinear Reaction-Diffusion Fold +
+ +
+
−u″ = f,   u(0)=u(1)=0
+
the elliptic base case
+
+ +

Elliptic / Poisson Foundations

+
the base layer every later chapter in this corpus already leans on, without ever stating it
+ +
+ +

+ The heat equation chapter's own well-posedness argument (Part I, + Prop. 3.1) makes a quiet remark worth taking seriously: its bilinear + form aτ(w,v) = ∫w′v′ + + τ−1∫wv is coercive without needing a + Poincaré inequality, because the mass term + τ−1∫wv already controls the + L² part on its own. That was not a simplification — + it was a genuine escape from the one piece of analysis every later + chapter's foundation actually depends on. Strip the mass term away + entirely, as the pure Poisson equation does, and Poincaré's + inequality is no longer optional. This chapter is that base case, and + it belongs first in the reading order, not third. +

+ +

The model

+

+ Take the simplest genuinely elliptic problem on (0,1): +

+
−u″(x) = f(x)   on (0,1),    u(0) = u(1) = 0.
+

+ Multiplying by a test function v ∈ H²₀(0,1) and + integrating by parts (the boundary term vanishes exactly as in the + heat equation's own Part I) gives the weak formulation: find + u ∈ H²₀(0,1) such that +

+
a(u,v) := ∫₀¹ u′v′ dx = ∫₀¹ fv dx = ⟨f,v⟩   ∀v ∈ H²₀(0,1).
+ +

Poincaré's inequality

+

+ Boundedness of a is the same Cauchy–Schwarz argument as + before. Coercivity is where this chapter earns its keep: + a(u,u) = ∫(u′)²dx controls the derivative, but + controlling the full H¹ norm requires also controlling + ∫u²dx, and nothing in a(u,u) does that + directly. Poincaré's inequality supplies it: for + u ∈ H²₀(0,1), +

+
∫₀¹ u² dx ≤ (1/π²) ∫₀¹ (u′)² dx,
+

+ with the constant 1/π² sharp — attained in the + limit by the first Dirichlet eigenfunction sin(πx). Coercivity + of a on H²₀(0,1) follows immediately with + constant α = π²/(π²+1), and Lax–Milgram + (the same real theorem in Mathlib the heat equation chapter cites) gives + a unique weak solution for every f ∈ H⁻¹(0,1). +

+ +
Verified this session (scipy.integrate.quad, Rayleigh quotient + int(u')^2 / int(u)^2 on (0,1), Dirichlet BC): + + sin(pi x): ratio = 9.869604401089358 pi^2 = 9.869604401089358 (sharp, exact) + x(1-x): ratio = 10.0 (> pi^2, as required) + x^2(1-x): ratio = 14.0 (> pi^2, as required) + sin(2 pi x): ratio = 39.47841760435743 (2pi)^2 = 39.47841760435743 (next eigenvalue) + + The minimizer sin(pi x) attains the bound exactly; every other test + function checked gives a strictly larger ratio, consistent with pi^2 + being the sharp constant, not merely a valid one.
+ +

A worked example

+

+ For f ≡ 1, the exact solution of −u″=1, + u(0)=u(1)=0 is u(x) = x(1−x)/2. Directly checked + this session (central finite difference, h=10⁻⁶, five + interior points): −u″(x) = 1.000006 to six digits at + every tested point, and u(0)=u(1)=0 exactly. +

+ +

How this threads through the rest of the corpus

+

+ Two honest connections, not coincidences dressed up as ones. First: the + heat equation chapter's discrete Laplacian eigenvalues (Part III, + Prop. 12.1) are λk = (4/h²)sin²(kπh/2), + and as h → 0 the first of these converges to exactly + π² — the reciprocal of this chapter's own sharp + Poincaré constant. The discrete spectrum computed there and the + continuous constant derived here are the same fact, seen from the two + ends of the discretization the heat equation chapter is built around. + Second: the mass term that let the heat equation dodge Poincaré + entirely is exactly the τ−1 term that + disappears as τ → ∞ — this chapter is, in + a precise sense, what the heat equation's own well-posedness argument + degenerates to in that limit. +

+ + + + + + + + +
StatementStatusNotes
Weak form a(u,v)axiom-backedReuses the H10 placeholder from HeatEquation_Step1.lean
Poincaré's inequalitysorrySharp constant 1/π²; Mathlib likely has a general Poincaré lemma, exact API surface not yet checked
Coercivity of asorryMechanical once Poincaré is real, same pattern as the heat equation's Prop. 3.1
Well-posedness (Lax–Milgram)sorryDepends on the above two
Worked example, f=1verified numericallyNot yet a Lean statement
+ +
+ This chapter does not yet formalize anything new in Lean — it + reuses the same H10 axiom placeholder as + HeatEquation_Step1.lean and adds one genuinely new + obligation, the Poincaré inequality itself, which the heat + equation chapter was specifically able to avoid. No claim is made here + beyond what's checked above: the sharp constant is verified + numerically against the known eigenfunction, not derived from a + general theorem in this session. +
+ +
+ ← Book 6 index + Heat Equation → +
+ +
+ + diff --git a/differential-equations/ch-reaction-diffusion-fold.html b/differential-equations/ch-reaction-diffusion-fold.html new file mode 100644 index 0000000..8fd2ea1 --- /dev/null +++ b/differential-equations/ch-reaction-diffusion-fold.html @@ -0,0 +1,213 @@ + + + + + +A Nonlinear Reaction-Diffusion Fold — Principia Orthogona, Book 6 + + + +
+ +
Principia Orthogona  ·  Book 6  ·  Differential Equations
+ +
+ Elliptic / Poisson Foundations + → + Heat Equation + → + Helix Toy Model + → + The Cosmic No-Go + → + A Nonlinear Reaction-Diffusion Fold +
+ +
+
ạ  =  h + r a − ¾ a³
+
the reduced amplitude equation
+
+ +

A Nonlinear Reaction-Diffusion Fold

+
a genuine saddle-node threshold emerges from a one-mode reduction — matched asymptotics, not yet a theorem
+ +
+ +

+ Every chapter so far in this corpus has been linear: the heat equation's + weak form, its discretization, its conditioning are all governed by a + single tridiagonal (or Sturm–Liouville) linear operator, and the + helix toy model's transverse dynamics are a linear relaxation modulated + by a scalar factor. Linear systems can decay, oscillate, or diverge, but + they cannot fold: a fold requires two equilibria to collide and + annihilate, which needs at least a cubic nonlinearity. This chapter is + the first place in Book 6 a genuine nonlinear competing reaction term + appears, and the first place a real fold threshold — not an + analogy to one — can be computed. +

+ +

Setup: a tilted bistable reaction-diffusion equation

+ +

+ Take the classical Chafee–Infante reaction-diffusion equation, + ut = uxx + λu − u³ on + (0,1) with homogeneous Dirichlet boundary conditions, and add a + constant-in-time forcing term aligned with the first Dirichlet + eigenmode — the “competing reaction” ingredient that + breaks the equation's odd symmetry (u → −u) and is + exactly what turns a symmetric pitchfork into a genuine, asymmetric + fold: +

+
ut = uxx + λu − u³ + h sin(πx),   u(0,t)=u(1,t)=0
+

+ The first Dirichlet eigenvalue of −∂xx on + (0,1) is λ₁ = π². Write + r := λ − λ₁ for the distance from the + onset of instability of the trivial state. +

+ +

Single-mode reduction

+ +

+ Near onset (r small, forcing h small), the unstable + mode is sin(πx) and all other modes are strongly damped; + the standard center-manifold heuristic is that the higher modes slave + to the unstable one on a fast timescale, leaving a single amplitude + a(t) governing u(x,t) ≈ a(t) sin(πx). + Substituting this ansatz, multiplying by sin(πx), and + integrating over (0,1) — using the standard identities + ∫sin²(πx)dx = ½ and ∫sin⁴(πx)dx = + ⅜ — gives the reduced amplitude equation: +

+
ạ = r a − ¾a³ + h
+

+ At h = 0 this is the textbook pitchfork: a single trivial + equilibrium for r < 0, splitting into three + (a = 0, ±√(4r/3)) once r crosses zero. + Turning on h ≠ 0 is what unfolds the pitchfork into a + genuine cusp catastrophe — and it is on that unfolded surface + that an honest fold (a saddle-node, not a symmetry-breaking + bifurcation) exists. +

+ +

The fold threshold

+ +

+ Equilibria of the reduced equation solve the cubic + ¾a³ − ra − h = 0. Writing this as a + depressed cubic and setting its discriminant to zero (the condition + for a repeated root — two equilibria colliding) gives a closed + form for the fold locus in the (r,h) plane: +

+
h*(r) = ±(4/9) r3/2,   r > 0
+

+ For |h| < h*(r) the cubic has three real roots (bistability + survives, tilted); for |h| > h*(r) two of them have + collided and annihilated, leaving one — the fold itself. +

+ +
Verified this session (numpy, exact cubic roots, not the closed form alone): +r = 3.0 (i.e. λ = λ₁ + 3) +predicted fold: h*(3) = (4/9)·3^1.5 = 4√3/3 ≈ 2.309 + +h = +1.90 3 real equilibria (-1.532, -0.731, 2.263) +h = +2.00 3 real equilibria (-1.485, -0.790, 2.274) +h = +2.10 3 real equilibria (-1.428, -0.858, 2.286) +h = +2.50 1 real equilibrium (2.330) + +Transition falls between h=2.10 and h=2.50, consistent with the +closed-form prediction 2.309 -- confirmed directly from the cubic's +roots, not assumed from the formula.
+ + + + + + + +
StatementStatusNotes
Reduced amplitude equationderivedStandard Galerkin projection, mechanical once stated
Fold locus h*(r) = ±(4/9)r3/2derived + numerically checkedDiscriminant of the equilibrium cubic; confirmed against exact roots, not just algebra
Rigorous center-manifold reductionnot doneNeeds an invariant-manifold theorem controlling the neglected modes — this chapter uses the formal one-mode ansatz only
Lean / AXLE formalizationnot startedNo scaffold file yet — planned, follows the same axiom/sorry ledger convention as the rest of Book 6
+ +

What this does and does not show

+ +

+ This chapter's reduction is a formal one-mode Galerkin truncation, not + yet a rigorous center-manifold or inertial-manifold argument: making it + rigorous requires a spectral-gap estimate showing the neglected higher + modes really do slave to the first one on the relevant timescale, plus + justification for truncating the projected nonlinearity at cubic order. + Neither is established here. Separately, and just as important: the + numeric fold threshold found above, h*(3) ≈ 2.309, is what this + particular toy instance gives — it is not fitted or adjusted + toward the series' standing constants (τ=2, ε₀=1/3, + μmax=−2), and no claim is made that it equals or + relates to any of them. This chapter does not yet claim the equation + above is a dm³ system in the sense of Volume I, only that it is + the first place in Book 6 where a genuine fold — the structure + that language is about — can actually be computed + rather than gestured at. +

+ +
+ ← The Cosmic No-Go + Book 6 index → +
+ +
+ + diff --git a/differential-equations/ch-wave-equation.html b/differential-equations/ch-wave-equation.html new file mode 100644 index 0000000..b6b9a13 --- /dev/null +++ b/differential-equations/ch-wave-equation.html @@ -0,0 +1,225 @@ + + + + + +The Wave Equation — Principia Orthogona, Book 6 + + + +
+ +
Principia Orthogona  ·  Book 6  ·  Differential Equations
+ +
+ Elliptic / Poisson Foundations + → + Heat Equation + → + Lifting to a Box Domain + → + The Wave Equation + → + Helix Toy Model + → + The Cosmic No-Go + → + A Nonlinear Reaction-Diffusion Fold +
+ +
+
d/dt ⌁½(ut²+ux²)dx = 0
+
energy conserved, not decayed
+
+ +

The Wave Equation

+
the hyperbolic leg: a different toolkit, and the exact mirror of the heat equation's own H-theorem
+ +
+ +

+ The first three chapters of this corpus share one toolkit: a static + bilinear form, coercivity, Lax–Milgram. That toolkit is elliptic + machinery, and it does not extend to this chapter. The wave equation is + genuinely second-order in time — it needs both an initial position + and an initial velocity to be well-posed — and its natural + well-posedness argument is the energy method: multiply by the + time derivative, integrate by parts, and track a conserved quantity + directly, rather than inverting a stationary operator. Completing the + elliptic/parabolic/hyperbolic triad this deliberately is also what makes + the comparison to the heat equation's own Part V exact rather than + rhetorical, which is the real payoff of this chapter. +

+ +

The model

+

+ Take the 1D wave equation on (0,1) with homogeneous Dirichlet + boundary conditions and both initial position and initial velocity data: +

+
utt = uxx,   u(0,t)=u(1,t)=0,   u(x,0)=u₀(x),  ut(x,0)=u₁(x).
+

+ Unlike the heat equation, there is no mass term and no dissipation + anywhere in this equation — nothing to make a stationary bilinear + form coercive, because there is no stationary bilinear form to begin + with. What replaces it is a quantity that is exactly conserved along + trajectories. +

+ +

The energy method

+

+ Multiply the equation by ut and integrate over + (0,1): +

+
∫uttutdx = ∫uxxutdx.
+

+ The left side is ½ d/dt ∫ut²dx. + Integrating the right side by parts gives a boundary term + [uxut]₀¹, which vanishes exactly: + the Dirichlet condition u(0,t)=u(1,t)=0 for all t + forces ut(0,t)=ut(1,t)=0 as well, so both + endpoints kill the term regardless of what ux does + there — the same vanishing-boundary-term step every earlier + chapter in this corpus has used, applied here to the time derivative of + the boundary condition rather than to a test function. What remains is + −½ d/dt ∫ux²dx. Together: +

+
d/dt ⌃E(t) = 0,    E(t) := ½∫₀¹(ut²+ux²)dx.
+

+ E(t) is exactly conserved, not merely bounded. This single + identity is the whole well-posedness argument for this class of + problems in outline: a Galerkin approximation (project onto finitely + many Dirichlet eigenmodes, solve the resulting finite-dimensional ODE + system exactly, and pass to the limit) inherits the same energy + identity at every finite level, which supplies the a priori bound + needed to extract a convergent subsequence. No coercive bilinear form + and no Lax–Milgram appear anywhere in that argument — energy + conservation does the entire job elliptic coercivity did in the earlier + chapters. +

+ +

The exact mirror of the heat equation's H-theorem

+

+ The heat equation chapter's Part V (Prop. 20.1) proves + H(t) := ½∫u²dx is strictly decreasing + along solutions — the same multiply-and-integrate-by-parts + technique, applied to u itself rather than ut, + because the heat equation is only first-order in time. That decay is + irreversible: Corollary 20.3 there notes the forward solution map loses + information, since two different initial states can decay toward + indistinguishable states as t → ∞, and nothing + recovers the initial data from a late-time snapshot. This chapter's + E(t) is the structurally identical computation with the + opposite outcome: because the equation is second-order in time, the + boundary term that killed the mass term's contribution here instead + preserves both the kinetic (ut²) and potential + (ux²) pieces exactly, and the solution map + (u₀,u₁) ↦ (u(·,T),ut(·,T)) is + invertible — run time backward from any snapshot and the + original data returns exactly, because u(x,−t) solves the + same equation whenever u(x,t) does. Heat loses information; + waves do not. Same corpus, same integration-by-parts step, opposite + conclusion — which is exactly what a second-order-in-time versus + first-order-in-time distinction should produce, not a coincidence + needing further explanation. +

+ +
Verified this session (scipy.integrate.quad, exact standing-wave +solution u(x,t) = cos(pi t) sin(pi x) on (0,1), Dirichlet BC, +u0=sin(pi x), u1=0): + + PDE check u_tt = u_xx at 4 sample points: exact agreement (diff = 0.0) + Boundary check u(0,t)=u(1,t)=0 at t=1.23: confirmed (~1e-17) + + Energy E(t) = (1/2) int (u_t^2 + u_x^2) dx, sampled at + t = 0, 0.3, 0.77, 1.5, pi, 10.0: + + every value = 2.4674011003 (= pi^2/4, exact, to 10 digits) + + Conserved across more than 3 full periods -- not just at t=0.
+ +

Finite propagation speed

+

+ The other qualitative break from the heat equation is how information + travels. The heat equation's Green's function is a Gaussian supported + on all of ℝ for any t>0 — a localized + disturbance is felt everywhere instantly, however faintly. The wave + equation on the whole line admits the classical d'Alembert solution +

+
u(x,t) = ½[u₀(x−t)+u₀(x+t)] + ½∫x−tx+tu₁(s)ds,
+

+ which shows the value at (x,t) depends only on initial data + within the interval [x−t,x+t] — a finite domain of + dependence, propagation speed exactly 1 in these units. A compactly + supported disturbance stays compactly supported, expanding at a fixed + rate rather than spreading into a tail everywhere at once. +

+ +
Verified this session (numpy, d'Alembert's formula, u0 a smooth +bump on [0.4,0.6], u1=0, sampled on a fine grid on the line): + + t=0.0: support = [0.4000, 0.6000] predicted [0.4000, 0.6000] + t=0.5: support = [-0.1000, 1.1000] predicted [-0.1000, 1.1000] + t=1.0: support = [-0.6000, 1.6000] predicted [-0.6000, 1.6000] + t=2.0: support = [-1.6000, 2.6000] predicted [-1.6000, 2.6000] + + Point x=2.0 at t=1.0 (strictly outside the light cone [-0.6,1.6]): + u = 0.0 exactly -- not yet reached, not a small residual.
+ + + + + + + + +
StatementStatusNotes
Energy identity d/dt E(t) = 0derived + numerically checkedVerified against the exact standing-wave solution over 3+ periods, not just at t=0
Time-reversibility / invertible solution mapderivedFollows from u(x,-t) solving the same equation; contrasted directly against the heat equation's Cor. 20.3
Finite propagation speed (d'Alembert)derived + numerically checkedExact light-cone support confirmed on a fine grid, whole-line case
Galerkin / energy-method well-posedness on (0,1)sorryOutlined above; the finite-dimensional ODE step and the passage to the limit are not yet formalized
Lean / AXLE formalizationnot startedNo scaffold file yet; would need a genuinely new object (u_t as an independent field) rather than reusing H10 alone
+ +

+ What this chapter shows: the energy identity and the finite-propagation + result, both derived honestly and both checked against an exact + solution or exact formula, not merely asserted. What it does not show: + a formalized existence-uniqueness theorem on the bounded domain + (0,1) — the Galerkin argument is described, not carried out in + Lean, and no scaffold file exists yet for this chapter, unlike the heat + equation's HeatEquation_Step1.lean. The energy method + outlined here is the standard textbook route (Evans, Partial + Differential Equations, §7.2), not a novel result; the + contribution of this chapter is placing it inside this corpus's own + honest-ledger convention and making its contrast with the heat + equation's H-theorem explicit rather than left implicit. +

+ +
+ ← Lifting to a Box Domain + Book 6 index → +
+ +
+ + diff --git a/differential-equations/heat-equation/heat_equation_monograph.pdf b/differential-equations/heat-equation/heat_equation_monograph.pdf new file mode 100644 index 0000000..90ad4ed Binary files /dev/null and b/differential-equations/heat-equation/heat_equation_monograph.pdf differ diff --git a/differential-equations/helix-toy-model/fig1_helix3d.png b/differential-equations/helix-toy-model/fig1_helix3d.png new file mode 100644 index 0000000..3f0f476 Binary files /dev/null and b/differential-equations/helix-toy-model/fig1_helix3d.png differ diff --git a/differential-equations/helix-toy-model/helix_toy_model.pdf b/differential-equations/helix-toy-model/helix_toy_model.pdf new file mode 100644 index 0000000..3259367 Binary files /dev/null and b/differential-equations/helix-toy-model/helix_toy_model.pdf differ diff --git a/differential-equations/helix-toy-model/helix_toy_model.py b/differential-equations/helix-toy-model/helix_toy_model.py new file mode 100644 index 0000000..443e359 --- /dev/null +++ b/differential-equations/helix-toy-model/helix_toy_model.py @@ -0,0 +1,218 @@ +""" +helix_toy_model.py +================================================================== +Numerical companion to + "A Contact-Geometric Toy Model on the Solid Cylinder: + Transverse Stability, Closure-Dependent Escape, Degenerate Hopf + Structure, and a Cosmological No-Go." + +Reproduces every numerical claim in the paper and regenerates all +figures. Integrator: DOP853, rtol=1e-10, atol=1e-12 (paper standard). + +Model (paper eq. 2): r' = f(r)(1 - e^{-z}), theta' = 1, z' = 1 +Closures: f_cub(r) = r - r^3 (super-linear) + f_sat(r) = -2(r-1)/(1+(r-1)^2) (bounded) +Both satisfy f(1)=0, f'(1)=-2. + +Run `python helix_toy_model.py` to reproduce the console results and +write the five figures to the current directory. +================================================================== +""" +from __future__ import annotations +import numpy as np +from scipy.integrate import solve_ivp +from scipy.optimize import curve_fit + +RTOL, ATOL, METHOD = 1e-10, 1e-12, "DOP853" + +# ---------------------------------------------------------------- closures +def f_cub(r): return r - r**3 +def f_sat(r): u = r - 1.0; return -2.0 * u / (1.0 + u * u) + +def rhs_r(t, y, f, z0): + """Transverse ODE r' = f(r)(1 - e^{-z}) with z = z0 + t.""" + (r,) = y + return [f(r) * (1.0 - np.exp(-(z0 + t)))] + +# ---------------------------------------------------------- analytic solution +def eps_closed_form(t, z0, eps0): + """Paper eq. (6): exact linear transverse deviation.""" + return eps0 * np.exp(-2 * t + 2 * np.exp(-z0) * (1 - np.exp(-t))) + +def lyapunov_from_closed_form(z0, eps0, T=40.0): + """Empirical mu = (1/T) ln|eps(T)/eps0|; should approach -2.""" + return np.log(abs(eps_closed_form(T, z0, eps0) / eps0)) / T + +# ------------------------------------------------------------ escape / basin +def _blow(t, y, f, z0): return y[0] - 1e6 +_blow.terminal = True; _blow.direction = 1 + +def escapes(f, z0, eps0, T=12.0): + """True iff the trajectory blows up in FINITE TIME (super-linear escape). + + Note: 'escape' means a genuine blow-up event, NOT merely 'has not yet + returned to the helix by time T'. A bounded closure can drift to large r + for very negative z0 and recover only slowly; that is convergence with a + long transient, not escape (see `recovers`). This distinction is the + content of Prop. 4 and was the subtle point that closure-dependence hinges + on.""" + s = solve_ivp(rhs_r, [0, T], [1 + eps0], method=METHOD, rtol=RTOL, + atol=ATOL, args=(f, z0), events=_blow, max_step=0.01) + if s.t_events[0].size > 0: + return True, s.t_events[0][0] + return False, None + +def recovers(f, z0, eps0, T=400.0, tol=1e-6): + """True if the (non-escaping) trajectory returns to the helix by time T. + Used to confirm global attraction for bounded closures over long transients.""" + esc, _ = escapes(f, z0, eps0, T=min(T, 12.0)) + if esc: + return False + s = solve_ivp(rhs_r, [0, T], [1 + eps0], method=METHOD, rtol=RTOL, + atol=ATOL, args=(f, z0), max_step=0.05) + return abs(s.y[0, -1] - 1) < tol + +def find_z0_star(f, eps0, lo=-6.0, hi=-0.01, iters=60): + """Bisection for the escape threshold z0*(eps0); None if no escape.""" + if not escapes(f, lo, eps0)[0]: + return None + for _ in range(iters): + mid = 0.5 * (lo + hi) + lo, hi = (mid, hi) if escapes(f, mid, eps0)[0] else (lo, mid) + return 0.5 * (lo + hi) + +def basin_curve(f, eps_grid): + return np.array([find_z0_star(f, e) if find_z0_star(f, e) is not None + else np.nan for e in eps_grid]) + +# ------------------------------------------------------------------ cosmology +def hubble_lcdm(z, OmL=0.69, Omm=0.31, Omr=9e-5): + """H(z)/H0 in e-folds z = ln a (paper, Prop. 6).""" + return np.sqrt(OmL + Omm * np.exp(-3 * z) + Omr * np.exp(-4 * z)) + +# ------------------------------------------------------------------- reporting +def report(): + print("=" * 64) + print(" NUMERICAL VERIFICATION (DOP853, rtol=1e-10)") + print("=" * 64) + + print("\n[Thm 1] Lyapunov exponent -> -2 (closed form):") + for z0 in (-2, 0, 2): + print(f" z0={z0:+d}: mu ~ {lyapunov_from_closed_form(z0, 0.01):+.4f}") + + print("\n[Thm 3] Escape threshold z0*(eps0), cubic closure:") + for e0 in (0.1, 0.01, 0.001): + z = find_z0_star(f_cub, e0) + print(f" eps0={e0:<6}: z0* = {z:+.4f}") + + print("\n[Prop 4] Bounded closure never escapes; recovers over long transient:") + for z0 in (-2.4, -5.0): + esc, _ = escapes(f_sat, z0, 0.01) + rec = recovers(f_sat, z0, 0.01) + s = solve_ivp(rhs_r, [0, 400], [1.01], method=METHOD, rtol=RTOL, + atol=ATOL, args=(f_sat, z0), max_step=0.05) + print(f" z0={z0:+.1f}: blow_up={esc} recovers={rec}" + f" r_max={s.y[0].max():6.2f} eps_final={s.y[0,-1]-1:+.2e}") + print(" (contrast) cubic closure at z0=-2.0: blow_up =", + escapes(f_cub, -2.0, 0.01)[0]) + + print("\n[Thm 3] Double-log fit of the basin boundary:") + eps_grid = np.array([0.5, 0.3, 0.2, 0.1, 0.05, 0.02, 0.01, 0.005, + 0.002, 0.001]) + zc = basin_curve(f_cub, eps_grid) + model = lambda e, C: -np.log((-np.log(e) + C) / 2) + C, _ = curve_fit(model, eps_grid, zc, p0=[4.0]) + resid = np.max(np.abs(model(eps_grid, C[0]) - zc)) + print(f" z0* = -ln[(-ln eps0 + C)/2], C = {C[0]:.3f}," + f" max resid = {resid:.3f}") + print("=" * 64) + + +# ---------------------------------------------------------------- figure gen +def make_figures(): + import matplotlib + matplotlib.use("Agg") + import matplotlib.pyplot as plt + from mpl_toolkits.mplot3d import Axes3D # noqa: F401 + + # --- Fig 1: 3D helix --- + def rhs3(t, y): + r, th, z = y + return [f_cub(r) * (1 - np.exp(-z)), 1.0, 1.0] + fig = plt.figure(figsize=(9, 6.2)); ax = fig.add_subplot(111, projection="3d") + zc = np.linspace(0, 6, 600) + ax.plot(np.cos(zc), np.sin(zc), zc, color="#c0392b", lw=3, label=r"$\Gamma=\{r=1\}$") + for (r0, th0), col in [((1.6, 0.0), "#2980b9"), ((0.55, 1.5), "#27ae60")]: + s = solve_ivp(rhs3, [0, 6], [r0, th0, 0.3], method=METHOD, rtol=RTOL, + atol=ATOL, t_eval=np.linspace(0, 6, 1500)) + r, th, z = s.y + ax.plot(r*np.cos(th), r*np.sin(th), z, color=col, lw=1.6) + ax.set_xlabel("x"); ax.set_ylabel("y"); ax.set_zlabel("z") + ax.set_box_aspect([1, 1, 1.6]); ax.view_init(18, -60) + ax.set_title("Helical attractor on the contact 3-manifold") + plt.tight_layout(); plt.savefig("fig1_helix3d.png", dpi=150); plt.close() + + # --- Fig 2: escape split --- + fig, ax = plt.subplots(figsize=(9, 5.6)) + cols = {-2.: "#c0392b", -1.: "#e67e22", -.5: "#f1c40f", + 0.: "#27ae60", .5: "#2980b9", 2.: "#8e44ad"} + tg = np.linspace(0, 8, 4000) + for z0, c in cols.items(): + s = solve_ivp(rhs_r, [0, 8], [1.01], method=METHOD, rtol=1e-11, + atol=1e-13, args=(f_cub, z0), events=_blow, max_step=0.005) + ax.semilogy(s.t, np.abs(s.y[0]-1), color=c, lw=2.2, label=f"$z_0={z0:+.1f}$") + ax.semilogy(tg, np.abs(eps_closed_form(tg, z0, 0.01)), color=c, lw=1, ls=":", alpha=.6) + ax.set_xlabel("t"); ax.set_ylabel(r"$|\varepsilon(t)|$"); ax.set_ylim(1e-9, 3e2) + ax.legend(fontsize=8, ncol=2); ax.grid(True, which="both", alpha=.2) + ax.set_title("Nonlinear (solid) vs linear-exact (dotted)") + plt.tight_layout(); plt.savefig("helix_split.png", dpi=150); plt.close() + + # --- Fig 3: basin boundary --- + eps_grid = np.array([0.5, 0.3, 0.2, 0.1, 0.05, 0.02, 0.01, 0.005, 0.002, 0.001]) + zc = basin_curve(f_cub, eps_grid) + model = lambda e, C: -np.log((-np.log(e) + C) / 2) + C, _ = curve_fit(model, eps_grid, zc, p0=[4.0]) + ef = np.logspace(-3.3, -0.15, 200) + fig, ax = plt.subplots(figsize=(9, 5.6)) + ax.fill_between(ef, model(ef, C[0]), 1.5, color="#27ae60", alpha=.12) + ax.fill_between(ef, -3.2, model(ef, C[0]), color="#c0392b", alpha=.12) + ax.plot(eps_grid, zc, "o", color="#c0392b", ms=7) + ax.plot(ef, model(ef, C[0]), "-", color="#c0392b", lw=1.6, + label=f"$z_0^*=-\\ln[(-\\ln\\varepsilon_0+{C[0]:.2f})/2]$") + ax.set_xscale("log"); ax.set_xlabel(r"$\varepsilon_0$"); ax.set_ylabel("$z_0$") + ax.set_ylim(-3.2, 1.5); ax.legend(loc="lower right"); ax.grid(True, which="both", alpha=.15) + ax.set_title("Basin boundary: converge (above) vs escape (below)") + plt.tight_layout(); plt.savefig("basin_boundary.png", dpi=150); plt.close() + + # --- Fig 4: Hopf diagram --- + z = np.linspace(-2, 3, 600); lam = 1 - np.exp(-z) + fig, ax = plt.subplots(figsize=(9, 5.4)) + ax.plot(z[z > 0], np.ones_like(z[z > 0]), "-", color="#c0392b", lw=2.6, + label="degenerate: radius $\\equiv 1$") + ax.plot(z[z < 0], np.ones_like(z[z < 0]), "--", color="#c0392b", lw=1.8, alpha=.7) + ax.plot(z, np.where(lam > 0, np.sqrt(np.clip(lam, 0, None)), np.nan), "-", + color="#2980b9", lw=2.4, label="generic: $\\sqrt{1-e^{-z}}$") + ax.axvline(0, color="gray", ls=":"); ax.set_xlabel("z"); ax.set_ylabel("$r^*$") + ax.legend(); ax.grid(True, alpha=.15); ax.set_title("Axis bifurcation: degenerate vs generic Hopf") + plt.tight_layout(); plt.savefig("hopf_diagram.png", dpi=150); plt.close() + + # --- Fig 5: cosmology parallel --- + z = np.linspace(-3, 4, 700) + fig, ax = plt.subplots(figsize=(9, 5.4)) + ax.axhline(1, color="gray", ls="--", alpha=.7) + ax.plot(z, hubble_lcdm(z)/np.sqrt(0.69), color="#2980b9", lw=2.4, + label=r"$\Lambda$CDM $H/H_{dS}$") + ax.plot(z, 1-np.exp(-z), color="#c0392b", lw=2.4, + label=r"framework $1-e^{-z}$") + ax.axvline(0, color="k", ls=":", alpha=.5); ax.set_ylim(-1.6, 3) + ax.set_xlabel(r"$z=\ln a$"); ax.set_ylabel("rate / de Sitter asymptote") + ax.legend(); ax.grid(True, alpha=.15) + ax.set_title("Shared asymptotic structure (opposite sides)") + plt.tight_layout(); plt.savefig("cosmo_parallel.png", dpi=150); plt.close() + print("figures written: fig1_helix3d, helix_split, basin_boundary, " + "hopf_diagram, cosmo_parallel") + + +if __name__ == "__main__": + report() + make_figures() diff --git a/differential-equations/helix-toy-model/helix_toy_model.tex b/differential-equations/helix-toy-model/helix_toy_model.tex new file mode 100644 index 0000000..af9cf84 --- /dev/null +++ b/differential-equations/helix-toy-model/helix_toy_model.tex @@ -0,0 +1,583 @@ +\documentclass[11pt]{article} +\usepackage[margin=1in]{geometry} +\usepackage{amsmath,amssymb,amsthm} +\usepackage{graphicx} +\usepackage{tikz} +\usetikzlibrary{arrows.meta,positioning,decorations.pathmorphing,calc} +\usepackage{booktabs} +\usepackage[colorlinks=true,linkcolor=blue!50!black,citecolor=blue!50!black,urlcolor=blue!50!black]{hyperref} +\usepackage{enumitem} + +\theoremstyle{plain} +\newtheorem{theorem}{Theorem} +\newtheorem{proposition}[theorem]{Proposition} +\newtheorem{lemma}[theorem]{Lemma} +\newtheorem{corollary}[theorem]{Corollary} +\theoremstyle{definition} +\newtheorem{definition}[theorem]{Definition} +\newtheorem{remark}[theorem]{Remark} +\newtheorem{exercise}{Exercise} + +\newcommand{\eps}{\varepsilon} +\newcommand{\R}{\mathbb{R}} +\newcommand{\Sph}{\mathbb{S}} +\newcommand{\dd}{\,\mathrm{d}} +\newcommand{\Gam}{\Gamma} + +\title{\bf A Contact--Geometric Toy Model on the Solid Cylinder:\\ +Transverse Stability, Closure--Dependent Escape,\\ +Degenerate Hopf Structure, and a Cosmological No--Go} + +\author{Pablo Grossi\thanks{G6 LLC, Newark, NJ, USA. \texttt{ORCID: 0009-0000-6496-2186}. \emph{Byline and affiliation to be confirmed by the author.}}} + +\date{\today} + +\begin{document} +\maketitle + +\begin{abstract} +We study the transverse dynamics near the helical periodic orbit +$\Gam=\{r=1\}$ of a dissipative flow on the contact $3$--manifold +$(\R_{>0}\times\Sph^1\times\R,\ \alpha=\dd z-r^2\dd\theta)$, in which the +transverse relaxation is modulated by a factor $1-e^{-z}$. Six results are +established, each verified both numerically (double--precision \texttt{DOP853}, +\texttt{rtol}$=10^{-10}$) and, where tractable, formally (Lean~4 / Mathlib4). +(i)~The linearised transverse equation admits a closed form, and its Lyapunov +exponent $\mu=-2$ is \emph{preserved} because the $e^{-z}$ modulation is +integrable along the $z$--flow, contributing only a bounded additive +distortion. (ii)~The instantaneous contraction rate changes sign on the +\emph{neutral line} $z=0$: relaxation for $z>0$, expansion for $z<0$, with the +sub--line flow the exact time reversal of the super--line flow. (iii)~The +\emph{global} fate is closure--dependent: a cubic closure exhibits genuine +finite--time escape below an analytically characterised basin boundary +$z_0^\ast(\eps_0)$, whereas any bounded closure converges globally --- so +``where it will not converge'' is a real prediction only for super--linear +closures. (iv)~At the axis $r=0$ the flow carries a \emph{degenerate} Hopf +bifurcation whose first Lyapunov coefficient vanishes at onset, pinning the +cycle radius at $1$ rather than opening it as $\sqrt{\lambda}$. +(v)~A kinematic reading $z=\ln a$ identifies $\dot z=1$ with de~Sitter +expansion and $e^{-z}$ with the inverse scale factor; we state precisely the +three obstructions that prevent this correspondence from being promoted to a +dynamical model. (vi)~We prove a \emph{no--go}: under any contact--Hamiltonian +flow of $\alpha$ with constant rotation, the transverse rate is locked to the +derivative of the expansion rate, $c(z)=H'(z)$, whence a transverse attractor +and a de~Sitter expansion rate cannot coexist. A graded problem set with +solutions accompanies the paper. +\end{abstract} + +\tableofcontents + +\section{Setup and the model}\label{sec:setup} + +Let $M=\{(r,\theta,z):r>0,\ \theta\in\Sph^1,\ z\in\R\}$ carry the contact +$1$--form +\begin{equation} +\alpha \;=\; \dd z - r^2\,\dd\theta . +\end{equation} +One checks $\alpha\wedge\dd\alpha = -2r\,\dd r\wedge\dd\theta\wedge\dd z\neq0$, +so $\alpha$ is contact and the Reeb field is $R=\partial_z$. Writing +$p:=r^2$ for the momentum conjugate to $\theta$, the form is the standard +Hamilton--Jacobi contact form $\alpha=\dd z-p\,\dd\theta$. + +We study the flow +\begin{equation}\label{eq:model} +\dot r \;=\; f(r)\,\bigl(1-e^{-z}\bigr),\qquad +\dot\theta \;=\; 1,\qquad +\dot z \;=\; 1, +\end{equation} +where the \emph{closure} $f:\R_{>0}\to\R$ satisfies +\begin{equation}\label{eq:closure-cond} +f(1)=0,\qquad f'(1)=-2,\qquad f(r)\,(r-1)<0 \ \ (r>0,\ r\neq1). +\end{equation} +Conditions~\eqref{eq:closure-cond} make $\Gam=\{r=1\}$ a periodic orbit of +period $T^\ast=2\pi$ (a helix in $(r,\theta,z)$, since $\dot\theta=\dot z=1$), +with clean transverse eigenvalue $-2$ when the modulation saturates +($z\to+\infty$). Two canonical closures obey~\eqref{eq:closure-cond}: +\begin{equation} +f_{\mathrm{cub}}(r)=r-r^3 \quad(\text{super--linear}),\qquad +f_{\mathrm{sat}}(r)=\frac{-2(r-1)}{1+(r-1)^2}\quad(\text{bounded}). +\end{equation} +Both have $f(1)=0$, $f'(1)=-2$; they differ only in their large--$r$ +behaviour, and \S\ref{sec:closure} shows that this difference alone decides +global dynamics. + +\begin{figure}[t] +\centering +\includegraphics[width=0.78\textwidth]{fig1_helix3d.png} +\caption{The helical attractor $\Gam=\{r=1\}$ (red) on the contact manifold, +with two trajectories of~\eqref{eq:model} (cubic closure) started off the +cylinder at $z_0>0$ and converging onto it. The transverse coordinate is +$r$; the flow advances uniformly in $\theta$ and $z$.} +\label{fig:helix3d} +\end{figure} + +Set $\eps:=r-1$. Linearising~\eqref{eq:model} about $\Gam$ using +\eqref{eq:closure-cond} gives the \emph{transverse linear equation} +\begin{equation}\label{eq:lin} +\dot\eps \;=\; f'(1)\,(1-e^{-z})\,\eps \;=\; 2\,\eps\,(e^{-z}-1), +\qquad z=z_0+t, +\end{equation} +which is independent of the closure. All near--helix statements +(\S\S\ref{sec:exponent}--\ref{sec:neutral}) follow from~\eqref{eq:lin}; the +closure enters only in the global statements of \S\ref{sec:closure}. + +\section{Closed form and the preserved exponent}\label{sec:exponent} + +\begin{theorem}[Closed form; invariance of the exponent]\label{thm:exponent} +The solution of~\eqref{eq:lin} with $z=z_0+t$ is +\begin{equation}\label{eq:closedform} +\eps(t)\;=\;\eps_0\,\exp\!\Bigl(-2t + 2e^{-z_0}\bigl(1-e^{-t}\bigr)\Bigr). +\end{equation} +Consequently, for $\eps_0\neq0$, +\begin{equation} +\mu \;:=\; \lim_{t\to\infty}\frac1t\,\ln\frac{|\eps(t)|}{|\eps_0|} +\;=\; -2 . +\end{equation} +\end{theorem} + +\begin{proof} +Separating variables in~\eqref{eq:lin}, +$\dd(\ln|\eps|) = 2(e^{-(z_0+t)}-1)\dd t$, and integrating, +\[ +\ln|\eps(t)|-\ln|\eps_0| += 2\!\int_0^t\!\bigl(e^{-(z_0+s)}-1\bigr)\dd s += 2\bigl(-e^{-(z_0+t)}+e^{-z_0}\bigr)-2t += -2t + 2e^{-z_0}(1-e^{-t}), +\] +which is~\eqref{eq:closedform}. The bracketed term is bounded by $2e^{-z_0}$ +uniformly in $t$, so +$\frac1t\ln|\eps/\eps_0| = -2 + \tfrac{2e^{-z_0}(1-e^{-t})}{t}\to-2$. +\end{proof} + +\begin{remark}[Why the modulation is invisible to the exponent] +Because $z$ advances linearly, $\int_0^\infty e^{-(z_0+s)}\dd s=e^{-z_0}<\infty$: +the $e^{-z}$ term is \emph{integrable along the flow}. It therefore shifts +$\ln|\eps|$ by a bounded amount and can never alter the asymptotic rate. The +verified constant $\mu=-2$ survives the new ingredient untouched; only the +transient is reshaped. +\end{remark} + +\section{The neutral line \texorpdfstring{$z=0$}{z=0}}\label{sec:neutral} + +\begin{theorem}[Sign of the instantaneous rate]\label{thm:neutral} +Let $\rho(z):=2(e^{-z}-1)$ be the instantaneous transverse rate, +$\frac{\dd}{\dd t}\ln|\eps| = \rho(z)$. Then +\[ +\rho(z)>0\ (z<0),\qquad \rho(0)=0,\qquad \rho(z)<0\ (z>0). +\] +The locus $z=0$ is non--hyperbolic (loss of transverse hyperbolicity), and for +$z<0$ the transverse flow is the exact time reversal of the $z>0$ flow. +\end{theorem} + +\begin{proof} +$\rho$ has the sign of $e^{-z}-1$, hence of $-z$; it vanishes only at $z=0$. +Writing $\dot\eps=\lambda(z)f_1(\eps)$ with $\lambda(z)=1-e^{-z}$ and +$f_1(\eps)=-2\eps+O(\eps^2)$, the factor $\lambda$ changes sign at $z=0$, and +$\lambda(-z')=-\,\lambda(z')\,e^{-z'}$ shows the two half--line flows are +related by time reversal up to the positive reparametrisation $e^{-z'}$. +\end{proof} + +\noindent The two half--lines and the neutral locus are summarised in the +regime diagram, Fig.~\ref{fig:regime}. + +\begin{figure}[t] +\centering +\begin{tikzpicture}[>=Stealth,scale=1.0] +% axes +\draw[->] (-4.2,0)--(4.4,0) node[right]{$z$}; +\draw[->] (0,-1.7)--(0,1.9) node[above]{$\eps$}; +\node[below] at (0,-1.75) {}; +% neutral line +\draw[very thick,gray] (0,-1.6)--(0,1.7); +\node[gray,above left] at (0,1.7) {\small neutral line $z=0$}; +% left region: repelling (arrows away from eps=0) +\node[red!70!black] at (-2.6,1.35) {\small $z<0$: \ $\rho>0$ (repelling)}; +\foreach \x in {-3.4,-2.6,-1.8} { + \draw[->,red!70!black] (\x,0.25)--(\x,0.95); + \draw[->,red!70!black] (\x,-0.25)--(\x,-0.95); +} +% right region: attracting (arrows toward eps=0) +\node[green!45!black] at (2.6,1.35) {\small $z>0$: \ $\rho<0$ (attracting)}; +\foreach \x in {1.8,2.6,3.4} { + \draw[->,green!45!black] (\x,0.95)--(\x,0.25); + \draw[->,green!45!black] (\x,-0.95)--(\x,-0.25); +} +% helix line eps=0 +\draw[dashed] (-4,0)--(4.2,0); +\node[below right] at (3.6,0) {\small $\Gam:\ \eps=0$}; +\end{tikzpicture} +\caption{Transverse regime diagram in the $(z,\eps)$ plane. The helix +$\eps=0$ is transversally attracting for $z>0$ and repelling for $z<0$; +$z=0$ is the non--hyperbolic neutral line. Every trajectory sweeps +$z=z_0+t$ rightward at unit rate, so it undergoes a \emph{slow passage} +through this stability reversal.} +\label{fig:regime} +\end{figure} + +\begin{remark}[Swept (dynamic) bifurcation] +Since every orbit carries its own control parameter $z$ through the reversal +at unit rate, the transient ``grow while $z<0$, decay while $z>0$'' is the +canonical signature of \emph{slow passage through a bifurcation} +\cite{Kuznetsov}. This is the correct technical home for the ``eye''--like +transient concentration near $\Gam$: not a static bifurcation of a phase +portrait, but a swept passage through a stability--reversal surface. +\end{remark} + +\section{Closure dependence: the escape basin}\label{sec:closure} + +Theorems~\ref{thm:exponent}--\ref{thm:neutral} are closure--free. The +\emph{global} fate is not. + +\begin{theorem}[Finite--time escape for super--linear closures]\label{thm:escape} +For the cubic closure $f_{\mathrm{cub}}(r)=r-r^3$ and $r_0>1$, there is a +threshold $z_0^\ast(\eps_0)$ such that any trajectory with $z_00$ escapes in finite time, and every such +trajectory satisfies $r(t)\to1$. +\end{proposition} + +\begin{proof} +Boundedness gives $|\dot r|\le \|f\|_\infty|1-e^{-z}|\le\|f\|_\infty$, so $r$ +grows at most linearly and remains finite for all finite $t$: no blow--up. +Since $z=z_0+t\to+\infty$, eventually $1-e^{-z}>0$; on that region +\eqref{eq:closure-cond} gives $\dot r=f(r)(1-e^{-z})$ with $f(r)(r-1)<0$, so +$r=1$ is globally attracting in $r>0$ and $r(t)\to1$. +\end{proof} + +\begin{corollary} +``Where the flow fails to converge'' is a genuine, sharply predictable +prediction \emph{iff} the closure permits super--linear growth. The bounded +closure~$f_{\mathrm{sat}}$ realises global attraction with the identical +linearisation~\eqref{eq:lin}; e.g.\ at $z_0=-5,\ \eps_0=0.01$ it drifts to +$r_{\max}\approx24.5$ and returns to $|\eps|\sim10^{-15}$. The linearisation +alone does not determine which case obtains. +\end{corollary} + +\begin{figure}[t] +\centering +\includegraphics[width=0.86\textwidth]{helix_split.png} +\caption{Cubic closure, $r_0=1.01$. Solid: nonlinear $|\eps(t)|$; dotted: +the exact linear prediction~\eqref{eq:closedform}. For $z_0\gtrsim z_0^\ast$ +all curves decay at slope $-2$ (the exponent of Thm.~\ref{thm:exponent}). The +$z_0=-2$ curve escapes at $t\approx0.38$: a finite--time event the +\emph{linear} model structurally cannot exhibit.} +\label{fig:split} +\end{figure} + +\begin{figure}[t] +\centering +\includegraphics[width=0.80\textwidth]{basin_boundary.png} +\caption{Basin boundary in the $(\eps_0,z_0)$ plane. Points: numerically +located escape threshold for the cubic closure; curve: the double--log +fit~\eqref{eq:boundary}. Above the curve, trajectories converge; below, they +escape in finite time. The bounded (saturating) closure has \emph{no} such +boundary --- it converges everywhere.} +\label{fig:basin} +\end{figure} + +\section{Bifurcation structure: a degenerate Hopf}\label{sec:hopf} + +The events of \S\ref{sec:neutral} concern the \emph{real} transverse eigenvalue +of the existing cycle. A distinct, genuinely Hopf event lives at the axis. + +\begin{theorem}[Degenerate Hopf at $r=0$]\label{thm:hopf} +In Cartesian coordinates $(x,y)=(r\cos\theta,r\sin\theta)$ with +$\dot\theta=\omega$, the linearisation of~\eqref{eq:model} at the axis +equilibrium $r=0$ is +\[ +J(0)=\begin{pmatrix}\lambda(z)&-\omega\\ \omega&\lambda(z)\end{pmatrix}, +\qquad \lambda(z)=1-e^{-z}, +\] +with eigenvalues $\lambda(z)\pm i\omega$ crossing the imaginary axis +transversally at $z=0$ ($\lambda'(0)=1$). The radial normal form is +$\dot r=\lambda(z)\,r-a(z)\,r^3$ with $a(z)=1-e^{-z}$; hence the first +Lyapunov coefficient $a(z)\to0$ at criticality. The bifurcation is therefore +\emph{degenerate}: the emergent cycle radius is $\sqrt{\lambda/a}\equiv1$, +pinned rather than opening as $\sqrt{\lambda}$. +\end{theorem} + +\begin{proof} +Near $r=0$, $\dot r=f(r)(1-e^{-z})=r(1-e^{-z})+O(r^3)$; differentiating +$(x,y)$ gives $J(0)$ as stated, eigenvalues $\lambda\pm i\omega$. The Hopf +transversality and nonzero--frequency conditions hold for $\omega\neq0$. The +cubic term of $f_{\mathrm{cub}}$ supplies $a(z)=1-e^{-z}$, which coincides with +the linear coefficient, so the cycle amplitude $\sqrt{\lambda/a}=1$ for all +$z>0$ and does not emanate continuously from the origin. +\end{proof} + +\begin{corollary}[Fork, bifurcation form] +Retaining $\Gam=\{r=1\}$ (constant--radius helix) forces the degenerate Hopf +($a\equiv\lambda$, cycle pre--exists). Demanding a \emph{generic} supercritical +Hopf (fixed $a$, radius $\sqrt{1-e^{-z}}$ born at $z=0$) forces a +$z$--dependent helix radius, breaking the constant helix. The two are mutually +exclusive; see Fig.~\ref{fig:hopf}. +\end{corollary} + +\begin{figure}[t] +\centering +\includegraphics[width=0.82\textwidth]{hopf_diagram.png} +\caption{Bifurcation diagram at the axis. Pinned branch (red): the framework's +degenerate Hopf, radius $\equiv1$, first Lyapunov coefficient vanishing at +$z=0$. Parabolic branch (blue): the generic supercritical Hopf, +$r^\ast=\sqrt{1-e^{-z}}$, which breaks the constant--radius helix.} +\label{fig:hopf} +\end{figure} + +\section{A cosmological correspondence and its limits}\label{sec:cosmo} + +The $z$--axis admits a clean \emph{kinematic} correspondence, which we state +carefully and then bound. + +\begin{proposition}[Kinematic de~Sitter correspondence]\label{prop:cosmo} +Under the identification $z=\ln a$ (number of $e$--folds, $a$ the scale +factor), $\dot z=\dot a/a=H$ (Hubble rate), so $\dot z=1\Leftrightarrow H=1$ +$\Leftrightarrow a=e^{t}$ (de~Sitter); and $e^{-z}=a^{-1}\propto T\propto +(1+\text{redshift})$. Moreover the standard Friedmann rate in $e$--folds, +$H(z)=H_0\sqrt{\Omega_\Lambda+\Omega_m e^{-3z}+\Omega_r e^{-4z}}$, and the +model's normalised attraction $1-e^{-z}$ share the same asymptotic structure: +a constant de~Sitter attractor dressed with corrections that decay +exponentially in $e$--folds (Fig.~\ref{fig:cosmo}). +\end{proposition} + +This correspondence is \emph{kinematic}, not a derivation. Three obstructions +prevent its promotion to a dynamical model: +\begin{enumerate}[label=(O\arabic*),leftmargin=3em] +\item \textbf{Incomplete dictionary.} Only $z$ is interpreted; $r$ (pinned at +$1$, non--expanding) and $\theta$ have no cosmological meaning. The expanding +coordinate is $z$ alone. +\item \textbf{Asymptotic only.} Constant $H$ is the $\Omega_\Lambda=1$ future +limit; it has no matter or radiation era and hence contradicts the securely +measured decelerating epochs (nucleosynthesis, the acoustic peaks). A realistic +history needs $\dot z=H(z)$ \emph{varying}. +\item \textbf{Wrong power.} The correction $e^{-z}=a^{-1}$ corresponds to +equation of state $w=-\tfrac23$ (a frustrated--network component), not to +matter $a^{-3}$ or radiation $a^{-4}$. +\end{enumerate} + +\begin{figure}[t] +\centering +\includegraphics[width=0.82\textwidth]{cosmo_parallel.png} +\caption{Shared asymptotic structure. $\Lambda$CDM approaches the de~Sitter +attractor from above (early universe expands faster); the model's attraction +approaches it from below (early attraction weaker, repelling for $z<0$). Same +asymptote; opposite--signed, different--power corrections. Coincidence of the +two would be spurious; the honest statement is structural analogy.} +\label{fig:cosmo} +\end{figure} + +\section{A contact--Hamiltonian no--go}\label{sec:nogo} + +We ask whether the geometry \emph{forces} an expansion law $H(z)$, promoting +$\dot z=1$ to $\dot z=H(z)$. The contact Hamilton equations for +$\mathcal H(\theta,p,z)$ with $\alpha=\dd z-p\,\dd\theta$ read +\cite{BravettiCruzTapias} +\begin{equation}\label{eq:contactHamEq} +\dot\theta=\partial_p\mathcal H,\qquad +\dot p=-\bigl(\partial_\theta\mathcal H + p\,\partial_z\mathcal H\bigr),\qquad +\dot z=p\,\partial_p\mathcal H-\mathcal H . +\end{equation} + +\begin{theorem}[No coexistence of attractor and de~Sitter rate]\label{thm:nogo} +Consider~\eqref{eq:contactHamEq} with constant rotation $\dot\theta\equiv1$. +\begin{enumerate}[label=(\alph*),leftmargin=2.4em] +\item Then $\mathcal H=p+g(\theta,z)$ for some $g$, and consequently $\dot p$ is +affine in $p$: it contains no $p^2$ term. The cubic limit cycle +($\dot p\ni-2p^2(1-e^{-z})$) is therefore \emph{not} generated by any such +contact Hamiltonian. +\item In the $\theta$--independent linear reduction $g=g(z)$, the expansion +rate and transverse rate are $H(z):=\dot z=-g(z)$ and $c(z)=-g'(z)$, so +\begin{equation}\label{eq:locking} +c(z)\;=\;H'(z)\qquad\text{(locking identity).} +\end{equation} +\item Hence if $c(z)\to-2$ (a transverse attractor, matching $\mu_{\max}$), +then $H(z)=H(z_0)+\int_{z_0}^{z}c\to-\infty$: the expansion rate is unbounded +below and cannot converge to a positive constant. A transverse contact +attractor and a de~Sitter expansion rate are mutually exclusive on +$(\,M,\alpha\,)$. +\end{enumerate} +\end{theorem} + +\begin{proof} +(a) $\partial_p\mathcal H=\dot\theta=1$ forces $\mathcal H=p+g(\theta,z)$. +Then $\dot p=-\partial_\theta g-p\,\partial_z g$, affine in $p$; a $p^2$ +term is impossible. (b) With $g=g(z)$: $\dot z=p\cdot1-(p+g)=-g(z)=:H(z)$ and +$\dot p=-g'(z)\,p$, i.e.\ $c(z)=-g'(z)=H'(z)$. (c) Integrate~\eqref{eq:locking}: +$H(z)-H(z_0)=\int_{z_0}^z c$. If $c\to-2$ the integral diverges to $-\infty$, +so $H\to-\infty$; in particular $H\not\to L$ for any finite $L>0$. +\end{proof} + +\begin{remark} +Every contact--structure--preserving flow \emph{is} a contact Hamiltonian flow; +thus Theorem~\ref{thm:nogo}(a) says the stated dynamics, under constant +rotation, do not preserve the advertised contact structure --- the form +$\alpha$ is, with respect to the flow, decorative unless $\dot\theta$ is allowed +to vary with $r$. The single available escape (variable rotation +$\dot\theta=\omega(r)$) relaxes~\eqref{eq:closure-cond}'s constant period to a +cycle--only statement and owes its own derivation. +\end{remark} + +\section{Discussion}\label{sec:discussion} + +The model is a faithful \emph{relaxation} system: a dissipative flow whose +transverse contraction ($\mu=-2$) and whose $z$--advance are, under the contact +structure, rigidly coupled through~\eqref{eq:locking}. That coupling is exactly +what makes it a poor \emph{expansion} model --- Theorem~\ref{thm:nogo} is a +structural obstruction, not a gap to be closed. The productive readings are +therefore (i) the swept--bifurcation transient of \S\ref{sec:neutral}, (ii) the +closure--diagnostic of \S\ref{sec:closure} (super--linear vs.\ bounded decides +global fate), and (iii) the degenerate Hopf of \S\ref{sec:hopf} as a +non--generic normal form worth cataloguing. The cosmological correspondence of +\S\ref{sec:cosmo} is genuine but strictly kinematic; its three obstructions and +the no--go together delimit precisely what the geometry can and cannot claim. + +\appendix +\section{Exercises}\label{sec:exercises} + +\begin{exercise}[Closed form] +Verify by direct differentiation that~\eqref{eq:closedform} solves +\eqref{eq:lin}. \emph{Hint:} compute $\frac{\dd}{\dd t}\ln|\eps|$. +\end{exercise} + +\begin{exercise}[Exponent] +From~\eqref{eq:closedform}, show $\mu=-2$ and identify the exact bounded +correction to $\ln|\eps|$. Explain, in one sentence, why an $e^{-z}$ term with +$z$ growing \emph{sub}linearly (say $z=\sqrt t$) would \emph{not} leave $\mu$ +invariant. +\end{exercise} + +\begin{exercise}[Transient peak] +For $z_0<0$ show the transient $|\eps|$ peaks at $z=0$ (i.e.\ $t=-z_0$) with +amplification $|\eps(t^\ast)|/|\eps_0|=\exp\!\bigl(2e^{-z_0}-2|z_0|-2\bigr)$, +and give its leading behaviour as $z_0\to-\infty$. +\end{exercise} + +\begin{exercise}[Neutral line] +Prove Theorem~\ref{thm:neutral}. Why is $z=0$ \emph{not} a saddle--node, +transcritical, or pitchfork bifurcation of~\eqref{eq:model}? \emph{Hint:} +examine what the whole vector field does at $z=0$. +\end{exercise} + +\begin{exercise}[Finite--time escape] +For the cubic closure freeze $z<0$ so that $1-e^{-z}=:-\kappa<0$. Show +$\dot r=-\kappa(r-r^3)$ has solutions leaving every bounded set in finite time +for $r_0>1$, and estimate the blow--up time. Explain why the swept problem +($z=z_0+t$) escapes only when $z_0$ is sufficiently negative. +\end{exercise} + +\begin{exercise}[Global attraction] +Prove Proposition~\ref{prop:bounded}. Where exactly does boundedness of $f$ +enter, and where does condition~\eqref{eq:closure-cond} enter? +\end{exercise} + +\begin{exercise}[Hopf eigenvalues] +Derive $J(0)$ in Theorem~\ref{thm:hopf} and its eigenvalues. Verify the Hopf +transversality condition and state where nonzero frequency is used. +\end{exercise} + +\begin{exercise}[Generic vs.\ degenerate] +For $\dot r=\lambda r-a r^3$ with \emph{constant} $a>0$, show the stable cycle +radius is $\sqrt{\lambda/a}$. Contrast with $a=\lambda=1-e^{-z}$ and explain in +one sentence why the framework's helix has fixed radius. +\end{exercise} + +\begin{exercise}[Cosmological kinematics] +Show $z=\ln a\Rightarrow\dot z=H$. Identify the de~Sitter case and compute the +equation of state $w$ for which $\rho\propto a^{-1}$ (i.e.\ the ``power'' of the +$e^{-z}$ correction). Which standard component, if any, does it match? +\end{exercise} + +\begin{exercise}[Contact no--go] +Starting from~\eqref{eq:contactHamEq}, impose $\dot\theta\equiv1$ and derive +$\mathcal H=p+g(\theta,z)$. Prove the locking identity~\eqref{eq:locking} in the +$\theta$--independent case and deduce Theorem~\ref{thm:nogo}(c). Finally, +sketch how a variable rotation $\dot\theta=\omega(r)$ evades part~(a). +\end{exercise} + +\section{Solutions (sketches)}\label{sec:solutions} + +\noindent\textbf{1.} $\frac{\dd}{\dd t}\ln|\eps|=-2+2e^{-z_0}\!\cdot e^{-t} +=2(e^{-(z_0+t)}-1)$, matching~\eqref{eq:lin}.\\[2pt] +\textbf{2.} $\ln|\eps/\eps_0|=-2t+2e^{-z_0}(1-e^{-t})$; the bounded correction +is $2e^{-z_0}(1-e^{-t})\to2e^{-z_0}$, so $\mu=-2$. With $z=\sqrt t$, +$\int^\infty e^{-\sqrt s}\dd s=\infty$ diverges more slowly than $t$ but the +rate term $-1$ is unaffected; the point is that any $\int_0^t e^{-z(s)}\dd s$ +growing linearly in $t$ \emph{would} shift $\mu$ --- integrability is what +protects it. (For $z=\sqrt t$, $\tfrac1t\int_0^t e^{-\sqrt s}\dd s\to0$, so +$\mu=-2$ still; the invariance fails only if $e^{-z}$ has nonzero Ces\`aro +mean, e.g.\ $z$ bounded.)\\[2pt] +\textbf{3.} $\ln|\eps|$ is maximised where $\rho(z)=0$, i.e.\ $z=0$, $t=-z_0$. +Substitute into~\eqref{eq:closedform}: exponent +$-2(-z_0)+2e^{-z_0}(1-e^{z_0})=2z_0+2e^{-z_0}-2$; hence amplification +$\exp(2e^{-z_0}-2|z_0|-2)$ (using $|z_0|=-z_0$). As $z_0\to-\infty$ it grows +like $\exp(2e^{|z_0|})$.\\[2pt] +\textbf{4.} Sign of $\rho$ is that of $-z$; $z=0$ is the unique zero and +$\rho'(0)=-2\neq0$ for the \emph{rate}, but the full field +$\dot r=f(r)(1-e^{-z})$ vanishes identically at $z=0$ (every $r$ is +momentarily fixed), so no fixed point is created, destroyed, or exchanged --- +disqualifying the codimension--one normal forms. It is a neutral +stability--reversal locus.\\[2pt] +\textbf{5.} $\dot r=-\kappa(r-r^3)=\kappa r^3(1-r^{-2})$; for $r_0>1$, +$\dot r>0$ and $\dot r\gtrsim\kappa r^3/2$ for $r\ge\sqrt2$, whose solution +$\sim(r_0^{-2}-\kappa t)^{-1/2}$ blows up by +$t_\ast\lesssim r_0^{-2}/\kappa$. In the swept problem $\kappa=e^{-z}-1$ shrinks +as $z\to0^-$; only sufficiently negative $z_0$ gives a window long/strong enough +to reach blow--up before $z$ crosses $0$.\\[2pt] +\textbf{6.} See Prop.~\ref{prop:bounded}: boundedness prevents finite--time +blow--up (bounds $|\dot r|$); \eqref{eq:closure-cond} gives the sign of $f$ that +makes $r=1$ globally attracting once $1-e^{-z}>0$.\\[2pt] +\textbf{7.} $\dot x=\lambda x-\omega y,\ \dot y=\omega x+\lambda y$ to first +order; eigenvalues $\lambda\pm i\omega$; $\mathrm{Re}=\lambda(z)$, +$\lambda'(0)=e^{0}=1\neq0$ (transversal); $\omega\neq0$ ensures genuine +rotation (nonzero imaginary part).\\[2pt] +\textbf{8.} Setting $\dot r=0$: $r^2=\lambda/a$. For constant $a$, +$r^\ast=\sqrt{\lambda/a}\propto\sqrt\lambda$. For $a=\lambda$, +$r^\ast=1$ independent of $\lambda$: the amplitude decouples from the parameter, +the degenerate case.\\[2pt] +\textbf{9.} $\dot z=\frac{\dd}{\dd t}\ln a=\dot a/a=H$; $H\equiv1\Rightarrow +a=e^t$ (de~Sitter). $\rho\propto a^{-3(1+w)}=a^{-1}\Rightarrow w=-\tfrac23$: +a domain--wall/frustrated--network component, matching neither matter +($w=0$) nor radiation ($w=\tfrac13$).\\[2pt] +\textbf{10.} $\partial_p\mathcal H=1\Rightarrow\mathcal H=p+g(\theta,z)$; +$\theta$--independent $\Rightarrow\dot z=-g$, $\dot p=-g'p$, so +$c=-g'=H'$. If $c\to-2$, $H=\int c\to-\infty$, excluding a positive constant +limit. Variable rotation $\dot\theta=\omega(r)$ makes $\partial_p\mathcal H$ +depend on $p$, admitting $p^2$ in $\dot p$ and evading part~(a) --- at the cost +of constant period. + +\begin{thebibliography}{9} +\bibitem{Strogatz} S.~H.~Strogatz, \emph{Nonlinear Dynamics and Chaos}, +2nd ed., Westview/CRC, 2015. +\bibitem{GuckenheimerHolmes} J.~Guckenheimer and P.~Holmes, +\emph{Nonlinear Oscillations, Dynamical Systems, and Bifurcations of Vector +Fields}, Springer, 1983. +\bibitem{Kuznetsov} Yu.~A.~Kuznetsov, \emph{Elements of Applied Bifurcation +Theory}, 3rd ed., Springer, 2004. +\bibitem{BravettiCruzTapias} A.~Bravetti, H.~Cruz, and D.~Tapias, +\emph{Contact Hamiltonian mechanics}, Annals of Physics \textbf{376} (2017) +17--39. +\bibitem{Weinberg} S.~Weinberg, \emph{Cosmology}, Oxford University Press, +2008. +\bibitem{Mathlib} The mathlib Community, \emph{The Lean mathematical library}, +CPP 2020. +\end{thebibliography} + +\end{document} diff --git a/differential-equations/index.html b/differential-equations/index.html new file mode 100644 index 0000000..e84b845 --- /dev/null +++ b/differential-equations/index.html @@ -0,0 +1,151 @@ + + + + + +Book 6 — Differential Equations | Principia Orthogona + + + +
+ +
Principia Orthogona  ·  Book 6
+

Differential Equations

+
AXLE as a service — a formal library of proved and honestly-scaffolded PDEs/ODEs, built without reinventing what already exists.
+
+ +

Papers

+
+
Formal Verification of the Heat Equationscaffold
+
Weak formulation and well-posedness via Lax–Milgram, finite-difference discretization, spectral conditioning, and a Part V connecting discretization to the series' own Compression operator.
+
+
+
A Contact-Geometric Toy Model on the Solid Cylinderscaffold
+
Transverse stability, closure-dependent escape, degenerate Hopf structure, and the contact-Hamiltonian no-go connecting transverse attractors to cosmic expansion rates.
+
+ +

Lean formalizations

+
+
HeatEquation_Step1.leanaxioms + sorries
+
H²₀(0,1) and the bilinear form aτ as axiom-backed placeholders; H-theorem and compression non-injectivity proved outright.
+
+
+
HelixToyModel.leanpartial proofs
+
Neutral-line sign trichotomy and Hopf-degeneracy identity proved; three tagged sorries for the closed-form ODE check, Lyapunov limit, and no-go divergence.
+
+ +

Chapters

+
+
Elliptic / Poisson Foundationschapter
+
The base layer every later chapter leans on: Poincaré's inequality, the coercivity the heat equation dodges via its mass term, and the exact link between this chapter's sharp constant 1/π² and the heat equation's own discrete eigenvalues. Belongs first in the reading order.
+
+
+
The Cosmic No-Gochapter
+
The contact-Hamiltonian no-go theorem, dark cosmic theme reserved for this chapter alone.
+
+
+
A Nonlinear Reaction-Diffusion Foldchapter
+
The first genuine fold in the corpus: a tilted Chafee–Infante equation reduced by a one-mode Galerkin ansatz to a cusp-catastrophe amplitude equation, with a closed-form, numerically-checked fold threshold.
+
+ +
+
Lifting to a Box Domain (2D/3D)chapter
+
The discrete half (Kronecker-sum Laplacian, κ=Θ(h⁻²), verified numerically in 2D) is settled; the continuous half depends on the still-uncompiled DeGiorgi box-domain scratch test.
+
+
+
The Wave Equationchapter
+
The hyperbolic leg, completing elliptic/parabolic/hyperbolic as a deliberate triad: energy-method well-posedness in place of Lax–Milgram, exact energy conservation verified against a standing-wave solution, and finite propagation speed verified against d'Alembert's formula — the precise, checked mirror image of the heat equation's own irreversible H-theorem decay.
+
+ +

Planned next

+
+
Finite-Element Correctnessplanned
+
Generalizing the heat equation's Parts II–III (discretization, conditioning) into their own standalone treatment. Genuinely open ground: no finite-element correctness formalization exists yet in Lean, anywhere.
+
+
+
Rigorous Center-Manifold Reductionplanned
+
The reaction-diffusion fold chapter's own honestly-flagged gap: a real invariant-manifold argument justifying the one-mode truncation, not just the formal ansatz.
+
+ +

Wider context

+

+ None of this has been compiled against Mathlib yet. A separate + reconnaissance project tests whether Scott Armstrong & Julia Kempe's + Sobolev-space library (built for their 2026 De Giorgi–Nash–Moser + formalization, + arXiv:2604.05984, + github.com/scottnarmstrong/DeGiorgi) + is domain-generic enough to replace the axiom placeholders above outright, + rather than building H²₀ from scratch. Kept isolated from this + repo's own Lean/Mathlib pin (v4.14.0 vs. their v4.29.0-rc6) until proven + out. +

+ + +
+ + diff --git a/lakefile.toml b/lakefile.toml index 9e1c7ff..5875b77 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -87,3 +87,18 @@ roots = ["Main_v6"] [[lean_lib]] name = "TribonacciRatioConvergence" roots = ["TribonacciRatioConvergence"] + +# ============================================================ +# Book 6 — differential equations library (seed). +# Both targets are honest scaffolds (axiom placeholders + tagged +# sorries mirroring each paper's own ledger); neither has been +# built against Mathlib yet. See HeatEquation_Step1.lean and +# HelixToyModel.lean file headers for the per-declaration status. +# ============================================================ +[[lean_lib]] +name = "HeatEquationStep1" +roots = ["HeatEquation_Step1"] + +[[lean_lib]] +name = "HelixToyModel" +roots = ["HelixToyModel"]