IndisputableMonolith.Cost.Ndim.ScalarCertificates

   1import IndisputableMonolith.Cost.Ndim.Core
   2import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
   3
   4/-!
   5# Non-parallelism and non-flatness certificates for the golden/metallic λ-family
   6
   7This file proves, by direct scalar computation, the two structural claims of the
   8"Golden and Metallic" note that are not yet covered elsewhere in the library:
   9
  101. **`P_λ` is not parallel** with respect to either the canonical flat connection `D`
  11   (Theorem 1a, `dP00_ne_zero`) or the Levi-Civita connection `∇^λ` of `h_λ`
  12   (Theorem 1b, `nablaP000_ne_zero`), on the 2-dimensional slice `α = (1,1)`,
  13   `t = (t, 0)`, `λ = 1`.
  142. **`h_λ` is non-flat** for `λ > 0`: the Riemann tensor component `R^0_{1,0,1}`
  15   is strictly negative for every `t ≠ 0` (Theorem 2, `R0101Closed_neg`).
  16
  17## Setup
  18
  19On the 2-slice with potential `Φ_λ(t₀,t₁) = cosh t₀ + cosh t₁ + λ(cosh(t₀+t₁) - 1)`,
  20metric `h_λ = D + λ g̃` with `D = diag(cosh t₀, cosh t₁)`, `g̃ = cosh(t₀+t₁) · (1,1)⊗(1,1)`,
  21and `P_λ = (1/μ_λ) h_λ⁻¹ g̃` the projector onto `span(1,1)`, evaluating at the point
  22`(t₀, t₁) = (t, 0)` gives (all verified independently by hand and by SymPy against the
  23Christoffel-derivative ground truth `R^0_101(5/4,3/4,1) = -81/4225`):
  24
  25* `P^0_0(t,0,1) = 1/(cosh t + 1)` =: `P00 t`
  26* `∂_0 P^0_0 = -sinh t / (cosh t + 1)^2` =: `dP00 t`
  27* `(∇^λ)_0 P^0_0 = -sinh t · (cosh t + 3) / (2 (cosh t + 1)^2 (cosh t + 2))` =: `nablaP000 t`
  28* `R^0_{1,0,1}(t,0,λ) = -λ sinh² t (λ cosh t + 1) / (4 cosh² t (λ cosh t + λ + 1)^2)`
  29  =: `R0101Closed t λ`
  30
  31These closed forms are the scalar *certificates*: since each is nonvanishing (resp.
  32negative) for every `t ≠ 0` (resp. `λ > 0`, `t ≠ 0`), non-parallelism and non-flatness
  33hold universally on the slice, not just at an isolated point, which avoids ever having
  34to construct a point with `cosh t = 5/4` inside Lean.
  35
  36The identification of these scalar closed forms with the actual tensor components of
  37`h_λ` (via the Hessian/Shima curvature formula for `R^0_{1,0,1}`, and the Christoffel
  38symbols of `h_λ` for `∇^λ`) is the companion geometric bridge; it is recorded as a
  39tagged hypothesis-level fact in the module docstring above and is not re-derived here.
  40This file is the self-contained algebraic core: given the closed forms, it proves the
  41nonvanishing/negativity, including the one nontrivial derivative computation
  42(`hasDerivAt_P00`) needed for Theorem 1a.
  43
  44Reference: "Golden and Metallic" note, Theorems (non-parallelism of `P_λ`) and
  45(non-flatness of `h_λ` for `λ ≠ 0`).
  46-/
  47
  48namespace IndisputableMonolith
  49namespace Cost
  50namespace Ndim
  51
  52noncomputable section
  53
  54/-- `P^0_0` at the slice point `(t, 0)`, `α = (1,1)`, `λ = 1`. -/
  55def P00 (t : ℝ) : ℝ := (Real.cosh t + 1)⁻¹
  56
  57/-- `∂_0 P^0_0` at the slice point, i.e. the derivative of `P00` w.r.t. the flat
  58    connection `D` (ordinary differentiation). -/
  59def dP00 (t : ℝ) : ℝ := -(Real.sinh t) / (Real.cosh t + 1) ^ 2
  60
  61/-- `(∇^λ)_0 P^0_0` at the slice point, `λ = 1`: the covariant derivative of `P_λ`
  62    w.r.t. the Levi-Civita connection of `h_λ`. -/
  63def nablaP000 (t : ℝ) : ℝ :=
  64  -(Real.sinh t) * (Real.cosh t + 3) / (2 * (Real.cosh t + 1) ^ 2 * (Real.cosh t + 2))
  65
  66/-- `R^0_{1,0,1}` at the slice point `(t, 0)`, `α = (1,1)`, general `λ`. -/
  67def R0101Closed (t lam : ℝ) : ℝ :=
  68  -(lam * (Real.sinh t) ^ 2 * (lam * Real.cosh t + 1)) /
  69    (4 * (Real.cosh t) ^ 2 * (lam * Real.cosh t + lam + 1) ^ 2)
  70
  71/-! ### Theorem 1a: `P_λ` is not `D`-parallel -/
  72
  73/-- `P00` is differentiable with derivative `dP00`, via a single `HasDerivAt.inv`
  74    applied to `cosh + 1`. -/
  75theorem hasDerivAt_P00 (t : ℝ) : HasDerivAt P00 (dP00 t) t := by
  76  have hc : HasDerivAt (fun x => Real.cosh x + 1) (Real.sinh t) t :=
  77    (Real.hasDerivAt_cosh t).add_const 1
  78  have hne : Real.cosh t + 1 ≠ 0 := ne_of_gt (by linarith [Real.cosh_pos t])
  79  simpa [P00, dP00] using hc.inv hne
  80
  81/-- **Theorem 1a** (non-parallelism of `P_λ` w.r.t. the flat connection `D`):
  82    the ordinary derivative of the `(0,0)` entry of `P_λ` is nonzero for every `t ≠ 0`.
  83    Hence `D P_λ ≠ 0`, i.e. `P_λ` is not `D`-parallel. -/
  84theorem dP00_ne_zero (t : ℝ) (ht : t ≠ 0) : dP00 t ≠ 0 := by
  85  unfold dP00
  86  apply div_ne_zero
  87  · exact neg_ne_zero.mpr (Real.sinh_ne_zero.mpr ht)
  88  · exact pow_ne_zero 2 (ne_of_gt (by linarith [Real.cosh_pos t]))
  89
  90/-! ### Theorem 1b: `P_λ` is not `∇^λ`-parallel -/
  91
  92/-- **Theorem 1b** (non-parallelism of `P_λ` w.r.t. the Levi-Civita connection `∇^λ`):
  93    the covariant derivative of the `(0,0)` entry of `P_λ` is nonzero for every `t ≠ 0`.
  94    Hence `∇^λ P_λ ≠ 0`, i.e. `P_λ` is not `∇^λ`-parallel. -/
  95theorem nablaP000_ne_zero (t : ℝ) (ht : t ≠ 0) : nablaP000 t ≠ 0 := by
  96  unfold nablaP000
  97  have hsinh_ne : Real.sinh t ≠ 0 := Real.sinh_ne_zero.mpr ht
  98  have hc3_ne : Real.cosh t + 3 ≠ 0 := ne_of_gt (by linarith [Real.cosh_pos t])
  99  apply div_ne_zero
 100  · exact mul_ne_zero (neg_ne_zero.mpr hsinh_ne) hc3_ne
 101  · have h1 : (0:ℝ) < Real.cosh t + 1 := by linarith [Real.cosh_pos t]
 102    have h2 : (0:ℝ) < Real.cosh t + 2 := by linarith [Real.cosh_pos t]
 103    positivity
 104
 105/-! ### Theorem 2: `h_λ` is non-flat for `λ > 0` -/
 106
 107/-- **Theorem 2** (non-flatness of `h_λ`, 2D case): the Riemann tensor component
 108    `R^0_{1,0,1}` is strictly negative for every `λ > 0` and `t ≠ 0`. Hence `h_λ` is
 109    not flat. This matches the SymPy-verified value `R^0_101(5/4,3/4,1) = -81/4225`
 110    (i.e. `R0101Closed t 1 = -81/4225` at `cosh t = 5/4`, `sinh t = 3/4`). -/
 111theorem R0101Closed_neg (t lam : ℝ) (hlam : 0 < lam) (ht : t ≠ 0) :
 112    R0101Closed t lam < 0 := by
 113  unfold R0101Closed
 114  have hc : 0 < Real.cosh t := Real.cosh_pos t
 115  have hs_ne : Real.sinh t ≠ 0 := Real.sinh_ne_zero.mpr ht
 116  have hs2_pos : 0 < (Real.sinh t) ^ 2 := sq_pos_of_ne_zero hs_ne
 117  have h_lc1 : 0 < lam * Real.cosh t + 1 := by nlinarith
 118  have h_lc2 : 0 < lam * Real.cosh t + lam + 1 := by nlinarith
 119  have h_den : 0 < 4 * (Real.cosh t) ^ 2 * (lam * Real.cosh t + lam + 1) ^ 2 := by
 120    positivity
 121  have hpos : 0 < lam * (Real.sinh t) ^ 2 * (lam * Real.cosh t + 1) :=
 122    mul_pos (mul_pos hlam hs2_pos) h_lc1
 123  have h_num : -(lam * (Real.sinh t) ^ 2 * (lam * Real.cosh t + 1)) < 0 := by linarith
 124  exact div_neg_of_neg_of_pos h_num h_den
 125
 126/-! ## General `α = (a, b)`: the panel-greenlit extension
 127
 128The theorems above are specialized to `α = (1,1)`. This section generalizes both
 129theorems 1 and 2 to arbitrary `α = (a, b)` with `a ≠ 0`, `b ≠ 0`, on the same slice
 130`t = (t, 0)`. The closed forms below were derived symbolically (SymPy, differentiating
 131the general-`α` Hessian `Φ(t₀,t₁) = cosh t₀ + cosh t₁ + λ(cosh(a t₀ + b t₁) - 1)` and
 132its inverse metric / Christoffel symbols) and checked at `a = b = 1` against `P00`,
 133`dP00`, `nablaP000`, `R0101Closed` above (difference `0` symbolically). They specialize
 134to the `α = (1,1)` closed forms exactly at `a = b = 1`, so this section is a strict
 135generalization, not a parallel development.
 136
 137* `P00Gen a b t = a² / (a² + b² cosh t)`
 138* `dP00Gen a b t = -a²b² sinh t / (a² + b² cosh t)²`
 139* `κGen a b λ t := a²λ cosh(at) + b²λ cosh t · cosh(at) + cosh t` (the shared denominator
 140  base of the covariant derivative and Riemann closed forms)
 141* `nablaP000Gen a b λ t = -a²b² sinh t · (κGen + cosh t) / (2(a² + b² cosh t)² · κGen)`
 142* `R0101Gen a b λ t = -b²λ(b²λ cosh(at) + 1) · sinh t · (a sinh(at)) / (4 κGen²)`
 143-/
 144
 145/-- `P^0_0` at the slice point `(t, 0)`, general `α = (a, b)`, `λ = 1`. -/
 146def P00Gen (a b t : ℝ) : ℝ := a ^ 2 / (a ^ 2 + b ^ 2 * Real.cosh t)
 147
 148/-- `∂_0 P^0_0` for general `α = (a, b)`. -/
 149def dP00Gen (a b t : ℝ) : ℝ := -(a ^ 2 * b ^ 2 * Real.sinh t) / (a ^ 2 + b ^ 2 * Real.cosh t) ^ 2
 150
 151/-- Shared denominator base for the general-`α` covariant-derivative and Riemann
 152    closed forms: `κ = a²λ cosh(at) + b²λ cosh t · cosh(at) + cosh t`. Always positive
 153    for `a ≠ 0`, `λ > 0` (each of its three summands is nonnegative and the third is
 154    strictly positive), so it never contributes a zero to either closed form. -/
 155def kappaGen (a b lam t : ℝ) : ℝ :=
 156  a ^ 2 * lam * Real.cosh (a * t) + b ^ 2 * lam * Real.cosh t * Real.cosh (a * t) + Real.cosh t
 157
 158/-- `(∇^λ)_0 P^0_0` at the slice point, general `α = (a, b)`, general `λ`. -/
 159def nablaP000Gen (a b lam t : ℝ) : ℝ :=
 160  -(a ^ 2 * b ^ 2 * Real.sinh t) * (kappaGen a b lam t + Real.cosh t) /
 161    (2 * (a ^ 2 + b ^ 2 * Real.cosh t) ^ 2 * kappaGen a b lam t)
 162
 163/-- `R^0_{1,0,1}` at the slice point `(t, 0)`, general `α = (a, b)`, general `λ`. -/
 164def R0101Gen (a b lam t : ℝ) : ℝ :=
 165  -(b ^ 2 * lam * (b ^ 2 * lam * Real.cosh (a * t) + 1)) *
 166    (Real.sinh t * (a * Real.sinh (a * t))) / (4 * kappaGen a b lam t ^ 2)
 167
 168/-- `κGen` is strictly positive whenever `a ≠ 0` and `λ > 0`: each summand is
 169    nonnegative (`cosh ≥ 1 > 0` everywhere, `a² > 0`, `b² ≥ 0`, `λ > 0`) and the third,
 170    `cosh t`, is always strictly positive on its own. -/
 171theorem kappaGen_pos (a b lam t : ℝ) (ha : a ≠ 0) (hlam : 0 < lam) :
 172    0 < kappaGen a b lam t := by
 173  unfold kappaGen
 174  have ha2 : 0 < a ^ 2 := by positivity
 175  have h1 : 0 ≤ a ^ 2 * lam * Real.cosh (a * t) := by positivity
 176  have h2 : 0 ≤ b ^ 2 * lam * Real.cosh t * Real.cosh (a * t) := by positivity
 177  have h3 : 0 < Real.cosh t := Real.cosh_pos t
 178  linarith
 179
 180/-- The sign-of-product cross lemma driving the general-`α` Riemann closed form:
 181    `sinh t · (a · sinh(at))` is strictly positive for `a ≠ 0`, `t ≠ 0`. Intuitively,
 182    `sinh` preserves the sign of its argument, and `a · sinh(at)` has the same sign as
 183    `a · (a·t) = a² t`, i.e. the sign of `t`; so the product has the sign of `t²`,
 184    always positive. -/
 185theorem sinh_cross_pos (a t : ℝ) (ha : a ≠ 0) (ht : t ≠ 0) :
 186    0 < Real.sinh t * (a * Real.sinh (a * t)) := by
 187  rcases ha.lt_or_gt with ha' | ha' <;> rcases ht.lt_or_gt with ht' | ht'
 188  · have hat : 0 < a * t := mul_pos_of_neg_of_neg ha' ht'
 189    have hsat : 0 < Real.sinh (a * t) := Real.sinh_pos_iff.mpr hat
 190    have hst : Real.sinh t < 0 := Real.sinh_neg_iff.mpr ht'
 191    have has : a * Real.sinh (a * t) < 0 := mul_neg_of_neg_of_pos ha' hsat
 192    exact mul_pos_of_neg_of_neg hst has
 193  · have hat : a * t < 0 := mul_neg_of_neg_of_pos ha' ht'
 194    have hsat : Real.sinh (a * t) < 0 := Real.sinh_neg_iff.mpr hat
 195    have hst : 0 < Real.sinh t := Real.sinh_pos_iff.mpr ht'
 196    have has : 0 < a * Real.sinh (a * t) := mul_pos_of_neg_of_neg ha' hsat
 197    exact mul_pos hst has
 198  · have hat : a * t < 0 := mul_neg_of_pos_of_neg ha' ht'
 199    have hsat : Real.sinh (a * t) < 0 := Real.sinh_neg_iff.mpr hat
 200    have hst : Real.sinh t < 0 := Real.sinh_neg_iff.mpr ht'
 201    have has : a * Real.sinh (a * t) < 0 := mul_neg_of_pos_of_neg ha' hsat
 202    exact mul_pos_of_neg_of_neg hst has
 203  · have hat : 0 < a * t := mul_pos ha' ht'
 204    have hsat : 0 < Real.sinh (a * t) := Real.sinh_pos_iff.mpr hat
 205    have hst : 0 < Real.sinh t := Real.sinh_pos_iff.mpr ht'
 206    have has : 0 < a * Real.sinh (a * t) := mul_pos ha' hsat
 207    exact mul_pos hst has
 208
 209/-! ### Theorem 1a (general `α`): `P_λ` is not `D`-parallel -/
 210
 211/-- `P00Gen a b` is differentiable with derivative `dP00Gen a b`. -/
 212theorem hasDerivAt_P00Gen (a b t : ℝ) (ha : a ≠ 0) :
 213    HasDerivAt (P00Gen a b) (dP00Gen a b t) t := by
 214  have hc : HasDerivAt (fun x => a ^ 2 + b ^ 2 * Real.cosh x) (b ^ 2 * Real.sinh t) t := by
 215    have := (Real.hasDerivAt_cosh t).const_mul (b ^ 2)
 216    simpa using this.const_add (a ^ 2)
 217  have ha2 : (0:ℝ) < a ^ 2 := by positivity
 218  have hne : a ^ 2 + b ^ 2 * Real.cosh t ≠ 0 := by
 219    have : (0:ℝ) ≤ b ^ 2 * Real.cosh t := by positivity
 220    linarith
 221  have hnum : HasDerivAt (fun _ : ℝ => a ^ 2) 0 t := hasDerivAt_const t (a ^ 2)
 222  have := (hnum.div hc hne)
 223  simpa [P00Gen, dP00Gen, div_eq_mul_inv] using this |>.congr_deriv (by ring)
 224
 225/-- **Theorem 1a, general `α`**: the ordinary derivative of the `(0,0)` entry of `P_λ`
 226    is nonzero for every `t ≠ 0`, `a ≠ 0`, `b ≠ 0`. Hence `D P_λ ≠ 0` for the whole
 227    `α = (a, b)` family, not just `α = (1,1)`. -/
 228theorem dP00Gen_ne_zero (a b t : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (ht : t ≠ 0) :
 229    dP00Gen a b t ≠ 0 := by
 230  unfold dP00Gen
 231  have ha2 : (0:ℝ) < a ^ 2 := by positivity
 232  have hb2 : (0:ℝ) < b ^ 2 := by positivity
 233  apply div_ne_zero
 234  · exact neg_ne_zero.mpr
 235      (mul_ne_zero (mul_ne_zero (ne_of_gt ha2) (ne_of_gt hb2)) (Real.sinh_ne_zero.mpr ht))
 236  · have hpos : (0:ℝ) < a ^ 2 + b ^ 2 * Real.cosh t := by
 237      have : (0:ℝ) ≤ b ^ 2 * Real.cosh t := by positivity
 238      linarith
 239    exact pow_ne_zero 2 (ne_of_gt hpos)
 240
 241/-! ### Theorem 1b (general `α`): `P_λ` is not `∇^λ`-parallel -/
 242
 243/-- **Theorem 1b, general `α`**: the covariant derivative of the `(0,0)` entry of `P_λ`
 244    is nonzero for every `t ≠ 0`, `a ≠ 0`, `b ≠ 0`, `λ > 0`. -/
 245theorem nablaP000Gen_ne_zero (a b lam t : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (hlam : 0 < lam)
 246    (ht : t ≠ 0) : nablaP000Gen a b lam t ≠ 0 := by
 247  unfold nablaP000Gen
 248  have hkap : 0 < kappaGen a b lam t := kappaGen_pos a b lam t ha hlam
 249  have hc : 0 < Real.cosh t := Real.cosh_pos t
 250  have ha2 : (0:ℝ) < a ^ 2 := by positivity
 251  have hb2 : (0:ℝ) < b ^ 2 := by positivity
 252  have hden_block : (0:ℝ) < a ^ 2 + b ^ 2 * Real.cosh t := by
 253    have : (0:ℝ) ≤ b ^ 2 * Real.cosh t := by positivity
 254    linarith
 255  apply div_ne_zero
 256  · apply mul_ne_zero
 257    · exact neg_ne_zero.mpr
 258        (mul_ne_zero (mul_ne_zero (ne_of_gt ha2) (ne_of_gt hb2)) (Real.sinh_ne_zero.mpr ht))
 259    · exact ne_of_gt (by linarith)
 260  · exact ne_of_gt (by positivity)
 261
 262/-! ### Theorem 2 (general `α`): `h_λ` is non-flat for `λ > 0` -/
 263
 264/-- **Theorem 2, general `α`**: the Riemann tensor component `R^0_{1,0,1}` is strictly
 265    negative for every `a ≠ 0`, `b ≠ 0`, `λ > 0`, `t ≠ 0`. Hence `h_λ` is non-flat for
 266    the whole `α = (a, b)` family, not just `α = (1,1)`. Specializes to
 267    `R0101Closed_neg` at `a = b = 1` (checked symbolically to agree with `R0101Closed`
 268    there). -/
 269theorem R0101Gen_neg (a b lam t : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (hlam : 0 < lam)
 270    (ht : t ≠ 0) : R0101Gen a b lam t < 0 := by
 271  unfold R0101Gen
 272  have hkap : 0 < kappaGen a b lam t := kappaGen_pos a b lam t ha hlam
 273  have hden : 0 < 4 * kappaGen a b lam t ^ 2 := by positivity
 274  have hb2 : (0:ℝ) < b ^ 2 := by positivity
 275  have hfac1 : 0 < b ^ 2 * lam * (b ^ 2 * lam * Real.cosh (a * t) + 1) := by
 276    have hcoshpos : (0:ℝ) < Real.cosh (a * t) := Real.cosh_pos _
 277    have : (0:ℝ) < b ^ 2 * lam * Real.cosh (a * t) + 1 := by positivity
 278    positivity
 279  have hfac2 : 0 < Real.sinh t * (a * Real.sinh (a * t)) := sinh_cross_pos a t ha ht
 280  have hnum : -(b ^ 2 * lam * (b ^ 2 * lam * Real.cosh (a * t) + 1)) *
 281      (Real.sinh t * (a * Real.sinh (a * t))) < 0 := by
 282    have := mul_pos hfac1 hfac2
 283    linarith
 284  exact div_neg_of_neg_of_pos hnum hden
 285
 286/-- Sanity check: `R0101Gen` specializes to `R0101Closed` at `a = b = 1` (verified
 287    symbolically via SymPy; the two closed forms agree identically as functions of
 288    `t, λ`, confirming this section is a genuine generalization). -/
 289example (t lam : ℝ) : R0101Gen 1 1 lam t = R0101Closed t lam := by
 290  unfold R0101Gen R0101Closed kappaGen
 291  simp only [one_pow, one_mul]
 292  ring_nf
 293
 294end
 295
 296end Ndim
 297end Cost
 298end IndisputableMonolith
 299