IndisputableMonolith.Cost.Ndim.CurvatureBridge

   1import IndisputableMonolith.Cost.Ndim.BlockReduction
   2
   3/-!
   4# General-`n` non-flatness: the full deformed metric, its inverse, and the Riemann tensor
   5
   6`BlockReduction.lean` generalizes Theorem 1a (non-parallelism of `P_λ`) to arbitrary
   7ambient dimension `n` by working directly with the mixed-tensor projector `PApply` and
   8the *undeformed* inverse `Dinv`. This module carries Theorem 2 (non-flatness of `h_λ`)
   9the same distance: it builds the *actual* deformed metric `h_λ = D + λ g̃` as a bare
  10array (`hFull`), proves its two-sided inverse via the Sherman-Morrison formula
  11(`hFull_mul_hInvFull`, genuinely `n`-dimensional, no 2-sparsity needed), builds the
  12third-derivative ("β") tensor of the potential and the Riemann tensor via Shima's
  13curvature formula for Hessian metrics, and proves that under a `TwoSparse` `α` and
  14`t i1 = 0`, the mixed Riemann component `R^{i0}_{i1,i0,i1}` collapses exactly to the
  15closed form `R0101Gen` already certified negative in `ScalarCertificates.lean`.
  16
  17## Shima's formula
  18
  19For a Hessian metric `h_{ij} = ∂_i∂_jΦ` with inverse `h^{ij}`, the Riemann tensor is
  20(Shima, *The Geometry of Hessian Structures*, Thm 2.1; sign convention fixed below by
  21direct SymPy comparison against the certified `R0101Gen` closed form):
  22
  23`R_{ijkl} = (1/4) Σ_{p,q} h^{pq} (β_{jkp} β_{ilq} - β_{ikp} β_{jlq})`,  `β_{ijk} = ∂_i∂_j∂_kΦ`,
  24
  25and `R^i_{jkl} = Σ_m h^{im} R_{mjkl}`. This module implements exactly this construction
  26as bare arrays over `Fin n`.
  27
  28## Architecture (panel-greenlit, `state/panel/hessian_theorems_*.json`)
  29
  30Bare-array + syntactic-index throughout: no `Matrix`, no manifold/`TangentSpace` API.
  31`hFull`/`hInvFull`/`beta`/`RiemannMixedApply` are plain functions `Fin n → Fin n → ℝ`
  32(resp. three-index), and the capstone theorem is a Christoffel/curvature-*component*
  33identity proved by direct sum manipulation, exactly the strategy that closed Stage A
  34(`PApply_e_eq_P00Gen`) — never an abstract "the connection restricted to a totally
  35geodesic submanifold agrees with the ambient one" argument (flagged `DEAD` by the
  36panel).
  37-/
  38
  39namespace IndisputableMonolith
  40namespace Cost
  41namespace Ndim
  42
  43open scoped BigOperators
  44
  45noncomputable section
  46
  47/-! ## Part 1: the deformed metric `h_λ` and its Sherman-Morrison inverse -/
  48
  49/-- The full `n`-dimensional deformed Hessian metric
  50`h_λ(i,j) = δ_{ij} cosh(t_i) + λ cosh(dot α t) · α_i α_j`, i.e. the Hessian of
  51`Φ_λ(t) = Σ_i cosh(t_i) + λ(cosh(dot α t) - 1)` (matches `hessianEntry` in
  52`Hessian.lean`, generalized to a named `λ` and packaged here for the curvature
  53bridge). -/
  54def hFull {n : ℕ} (α t : Vec n) (lam : ℝ) (i j : Fin n) : ℝ :=
  55  (if i = j then Real.cosh (t i) else 0) + lam * Real.cosh (dot α t) * α i * α j
  56
  57/-- The Sherman-Morrison inverse of `hFull`: for the rank-one update
  58`h_λ = D + (λc)·α⊗α` of the invertible diagonal `D = diag(cosh t_i)`, the inverse is
  59`D⁻¹ - (λc/(1+λc·S))·(D⁻¹α)⊗(D⁻¹α)`, where `S = dot α (D⁻¹α)` is α's self-energy
  60w.r.t. `D⁻¹` and `c = cosh(dot α t)`. -/
  61def hInvFull {n : ℕ} (α t : Vec n) (lam : ℝ) (i j : Fin n) : ℝ :=
  62  Dinv t i j -
  63    (lam * Real.cosh (dot α t) /
  64        (1 + lam * Real.cosh (dot α t) * dot α (sharp (Dinv t) α))) *
  65      (sharp (Dinv t) α i) * (sharp (Dinv t) α j)
  66
  67theorem hInvFull_symm {n : ℕ} (α t : Vec n) (lam : ℝ) (i j : Fin n) :
  68    hInvFull α t lam i j = hInvFull α t lam j i := by
  69  unfold hInvFull Dinv
  70  by_cases h : i = j
  71  · subst h; ring
  72  · rw [if_neg h, if_neg (Ne.symm h)]; ring
  73
  74/-- **The Sherman-Morrison identity.** For any ambient dimension `n`, `hInvFull` really
  75is the two-sided inverse of `hFull`, provided the Sherman-Morrison denominator
  76`1 + λc·S` is nonzero (`S = dot α (D⁻¹α)`, `c = cosh(dot α t)`). This is the genuinely
  77`n`-dimensional content this module adds: no `TwoSparse` hypothesis anywhere in this
  78theorem. -/
  79theorem hFull_mul_hInvFull {n : ℕ} (α t : Vec n) (lam : ℝ) (i j : Fin n)
  80    (hdenom : 1 + lam * Real.cosh (dot α t) * dot α (sharp (Dinv t) α) ≠ 0) :
  81    ∑ k : Fin n, hFull α t lam i k * hInvFull α t lam k j = if i = j then (1 : ℝ) else 0 := by
  82  set c := Real.cosh (dot α t) with hc_def
  83  set w := sharp (Dinv t) α with hw_def
  84  set S := dot α w with hS_def
  85  have hSsum : S = ∑ k : Fin n, α k * w k := by rw [hS_def]; rfl
  86  have hwj : ∀ k : Fin n, w k = (Real.cosh (t k))⁻¹ * α k := fun k => sharp_Dinv_apply t α k
  87  have hstep1 : ∑ k : Fin n, hFull α t lam i k * Dinv t k j
  88      = (if i = j then (1 : ℝ) else 0) + lam * c * α i * w j := by
  89    rw [Finset.sum_eq_single j]
  90    · unfold Dinv
  91      rw [if_pos rfl]
  92      unfold hFull
  93      by_cases hij : i = j
  94      · subst hij
  95        rw [if_pos rfl, if_pos rfl, hwj i]
  96        have hne : Real.cosh (t i) ≠ 0 := ne_of_gt (Real.cosh_pos _)
  97        field_simp
  98        ring
  99      · rw [if_neg hij, if_neg hij, hwj j]
 100        ring
 101    · intro k _ hk
 102      unfold Dinv
 103      rw [if_neg hk]
 104      ring
 105    · intro h
 106      exact absurd (Finset.mem_univ j) h
 107  have hstep2 : ∑ k : Fin n, hFull α t lam i k * w k = α i * (1 + lam * c * S) := by
 108    have hexp : ∀ k : Fin n, hFull α t lam i k * w k
 109        = (if i = k then Real.cosh (t i) * w k else 0) + lam * c * α i * (α k * w k) := by
 110      intro k
 111      unfold hFull
 112      by_cases hik : i = k
 113      · rw [if_pos hik, if_pos hik]; ring
 114      · rw [if_neg hik, if_neg hik]; ring
 115    rw [Finset.sum_congr rfl (fun k _ => hexp k), Finset.sum_add_distrib]
 116    have hpart1 : ∑ k : Fin n, (if i = k then Real.cosh (t i) * w k else 0)
 117        = Real.cosh (t i) * w i := by
 118      rw [Finset.sum_ite_eq (Finset.univ : Finset (Fin n)) i (fun k => Real.cosh (t i) * w k)]
 119      simp
 120    have hpart2 : ∑ k : Fin n, lam * c * α i * (α k * w k) = lam * c * α i * S := by
 121      rw [← Finset.mul_sum, ← hSsum]
 122    rw [hpart1, hpart2, hwj i]
 123    have hne : Real.cosh (t i) ≠ 0 := ne_of_gt (Real.cosh_pos _)
 124    field_simp
 125  have hsplit : ∑ k : Fin n, hFull α t lam i k * hInvFull α t lam k j
 126      = ∑ k : Fin n, hFull α t lam i k * Dinv t k j
 127        - (lam * c / (1 + lam * c * S)) * w j * ∑ k : Fin n, hFull α t lam i k * w k := by
 128    have heach : ∀ k : Fin n, hFull α t lam i k * hInvFull α t lam k j
 129        = hFull α t lam i k * Dinv t k j
 130          - (lam * c / (1 + lam * c * S)) * w j * (hFull α t lam i k * w k) := by
 131      intro k
 132      unfold hInvFull
 133      ring
 134    rw [Finset.sum_congr rfl (fun k _ => heach k), Finset.sum_sub_distrib, ← Finset.mul_sum]
 135  rw [hsplit, hstep1, hstep2]
 136  field_simp
 137  ring
 138
 139/-! ## Part 2: the third-derivative tensor `β` -/
 140
 141/-- The (Hessian-)symmetric third-derivative tensor of the potential
 142`Φ_λ(t) = Σ_i cosh(t_i) + λ(cosh(dot α t) - 1)`:
 143`β_{ijk} = ∂_i∂_j∂_kΦ_λ = (if i=j=k then sinh(t_i) else 0) + λ α_iα_jα_k sinh(dot α t)`.
 144Direct closed-form definition, mirroring `hessianEntry`'s treatment of the second
 145derivative in `Hessian.lean`. -/
 146def beta {n : ℕ} (α t : Vec n) (lam : ℝ) (i j k : Fin n) : ℝ :=
 147  (if i = j ∧ j = k then Real.sinh (t i) else 0) + lam * α i * α j * α k * Real.sinh (dot α t)
 148
 149/-- `β_{ijk}` vanishes whenever one of its indices carries a zero `α`-component and the
 150diagonal term does not fire. This is the key structural fact driving the
 151block-diagonal collapse of the Riemann sum: a spectator index (`α = 0`, off the
 152`TwoSparse` support) kills every summand it appears in. -/
 153theorem beta_eq_zero {n : ℕ} (α t : Vec n) (lam : ℝ) (i j k : Fin n)
 154    (hz : α i = 0 ∨ α j = 0 ∨ α k = 0) (hne : ¬ (i = j ∧ j = k)) :
 155    beta α t lam i j k = 0 := by
 156  unfold beta
 157  rw [if_neg hne]
 158  rcases hz with h | h | h <;> rw [h] <;> ring
 159
 160/-! ## Part 3: Shima's curvature formula and the Riemann tensor -/
 161
 162/-- Shima's formula for the doubly-lowered Riemann tensor of a Hessian metric:
 163`R_{ijkl} = (1/4) Σ_{p,q} h^{pq}(β_{jkp}β_{ilq} - β_{ikp}β_{jlq})`. -/
 164def RiemannLowerApply {n : ℕ} (ginv : Fin n → Fin n → ℝ) (b : Fin n → Fin n → Fin n → ℝ)
 165    (i j k l : Fin n) : ℝ :=
 166  (1 / 4) * ∑ p : Fin n, ∑ q : Fin n, ginv p q * (b j k p * b i l q - b i k p * b j l q)
 167
 168/-- The mixed Riemann tensor `R^i_{jkl} = Σ_m h^{im} R_{mjkl}`. -/
 169def RiemannMixedApply {n : ℕ} (ginv : Fin n → Fin n → ℝ) (b : Fin n → Fin n → Fin n → ℝ)
 170    (i j k l : Fin n) : ℝ :=
 171  ∑ m : Fin n, ginv i m * RiemannLowerApply ginv b m j k l
 172
 173/-! ## Part 4: block-diagonal reduction machinery -/
 174
 175/-- A generic single-index restriction: a function vanishing off `{i0, i1}` sums to the
 176sum of its two values on the support. (Same content as `sum_twoSparse` in
 177`BlockReduction.lean`, stated for a bare function rather than an `α i ^ 2`-weighted
 178one, so it is reusable for the Riemann reduction below.) -/
 179theorem sum_restrict_pair {n : ℕ} (i0 i1 : Fin n) (hne : i0 ≠ i1) (f : Fin n → ℝ)
 180    (hz : ∀ k : Fin n, k ≠ i0 → k ≠ i1 → f k = 0) :
 181    ∑ k : Fin n, f k = f i0 + f i1 := by
 182  have hsub : ({i0, i1} : Finset (Fin n)) ⊆ Finset.univ := Finset.subset_univ _
 183  have hzero : ∀ x ∈ (Finset.univ : Finset (Fin n)), x ∉ ({i0, i1} : Finset (Fin n)) → f x = 0 := by
 184    intro x _ hx
 185    simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hx
 186    exact hz x hx.1 hx.2
 187  rw [← Finset.sum_subset hsub hzero, Finset.sum_pair hne]
 188
 189/-- The double-sum analogue of `sum_restrict_pair`: a function of two arguments
 190vanishing whenever *either* argument is off `{i0, i1}` collapses to its four values on
 191the `{i0,i1} × {i0,i1}` support. -/
 192theorem sum2_restrict_pair {n : ℕ} (i0 i1 : Fin n) (hne : i0 ≠ i1) (f : Fin n → Fin n → ℝ)
 193    (hz : ∀ p q : Fin n, (p ≠ i0 ∧ p ≠ i1) ∨ (q ≠ i0 ∧ q ≠ i1) → f p q = 0) :
 194    ∑ p : Fin n, ∑ q : Fin n, f p q = f i0 i0 + f i1 i0 + (f i0 i1 + f i1 i1) := by
 195  have hFin : ∀ p : Fin n, ∑ q : Fin n, f p q = f p i0 + f p i1 := by
 196    intro p
 197    apply sum_restrict_pair i0 i1 hne (f p)
 198    intro q hq0 hq1
 199    exact hz p q (Or.inr ⟨hq0, hq1⟩)
 200  rw [Finset.sum_congr rfl (fun p _ => hFin p), Finset.sum_add_distrib]
 201  have h1 : ∑ p : Fin n, f p i0 = f i0 i0 + f i1 i0 :=
 202    sum_restrict_pair i0 i1 hne (fun p => f p i0) (fun p hp0 hp1 => hz p i0 (Or.inl ⟨hp0, hp1⟩))
 203  have h2 : ∑ p : Fin n, f p i1 = f i0 i1 + f i1 i1 :=
 204    sum_restrict_pair i0 i1 hne (fun p => f p i1) (fun p hp0 hp1 => hz p i1 (Or.inl ⟨hp0, hp1⟩))
 205  rw [h1, h2]
 206
 207/-- `hInvFull` vanishes whenever one argument is a spectator index (`α = 0`, off the
 208`TwoSparse` support): the Sherman-Morrison correction term is proportional to
 209`w_k = (cosh t_k)⁻¹ α_k`, which vanishes there, leaving only the *off-diagonal* part
 210of the (diagonal) `Dinv`, which is itself zero. -/
 211theorem hInvFull_spectator {n : ℕ} (α t : Vec n) (lam : ℝ) (i0 i1 k j : Fin n)
 212    (hk0 : k ≠ i0) (hk1 : k ≠ i1) (hz : α k = 0) (hkj : k ≠ j) :
 213    hInvFull α t lam k j = 0 := by
 214  unfold hInvFull
 215  rw [sharp_Dinv_apply t α k, hz]
 216  unfold Dinv
 217  rw [if_neg hkj]
 218  ring
 219
 220/-- `S = dot α (D⁻¹α)` restricted to a `TwoSparse` support: only the `i0, i1`
 221components survive. -/
 222theorem dot_sharp_Dinv_twoSparse {n : ℕ} (t α : Vec n) (i0 i1 : Fin n) (hne : i0 ≠ i1)
 223    (h2 : TwoSparse α i0 i1) :
 224    dot α (sharp (Dinv t) α)
 225      = (Real.cosh (t i0))⁻¹ * α i0 ^ 2 + (Real.cosh (t i1))⁻¹ * α i1 ^ 2 := by
 226  have hpt : ∀ i : Fin n, α i * sharp (Dinv t) α i = (Real.cosh (t i))⁻¹ * α i ^ 2 := by
 227    intro i; rw [sharp_Dinv_apply]; ring
 228  unfold dot
 229  rw [Finset.sum_congr rfl (fun i _ => hpt i)]
 230  exact sum_twoSparse α i0 i1 hne h2 (fun i => (Real.cosh (t i))⁻¹)
 231
 232/-- The core vanishing fact driving the Riemann reduction: for `p` or `q` off the
 233`TwoSparse` support, every term of Shima's `(p,q)`-summand built from `β` at
 234`(i1, i0, ·)`/`(m, i0, ·)`/`(m, i1, ·)`/`(i1, i1, ·)` vanishes, regardless of `m`. -/
 235theorem riemann_beta_numerator_zero {n : ℕ} (α t : Vec n) (lam : ℝ) (i0 i1 : Fin n)
 236    (hne01 : i0 ≠ i1) (h2 : TwoSparse α i0 i1) (m p q : Fin n)
 237    (hspec : (p ≠ i0 ∧ p ≠ i1) ∨ (q ≠ i0 ∧ q ≠ i1)) :
 238    beta α t lam i1 i0 p * beta α t lam m i1 q - beta α t lam m i0 p * beta α t lam i1 i1 q = 0 := by
 239  rcases hspec with ⟨hp0, hp1⟩ | ⟨hq0, hq1⟩
 240  · have hzp : α p = 0 := h2 p hp0 hp1
 241    have h1 : beta α t lam i1 i0 p = 0 :=
 242      beta_eq_zero α t lam i1 i0 p (Or.inr (Or.inr hzp)) (fun h => hne01 h.1.symm)
 243    have h3 : beta α t lam m i0 p = 0 :=
 244      beta_eq_zero α t lam m i0 p (Or.inr (Or.inr hzp)) (fun h => hp0 h.2.symm)
 245    rw [h1, h3]; ring
 246  · have hzq : α q = 0 := h2 q hq0 hq1
 247    have h1 : beta α t lam m i1 q = 0 :=
 248      beta_eq_zero α t lam m i1 q (Or.inr (Or.inr hzq)) (fun h => hq1 h.2.symm)
 249    have h3 : beta α t lam i1 i1 q = 0 :=
 250      beta_eq_zero α t lam i1 i1 q (Or.inr (Or.inr hzq)) (fun h => hq1 h.2.symm)
 251    rw [h1, h3]; ring
 252
 253/-! ## Part 5: the capstone — `RiemannMixedApply` collapses to `R0101Gen` -/
 254
 255/-- **Stage B capstone reduction.** Under a `TwoSparse` `α` (support `{i0, i1}`) and
 256`t i1 = 0`, the general-`n` mixed Riemann component `R^{i0}_{i1,i0,i1}`, built from the
 257*actual* deformed metric `hFull`/`hInvFull` and its Hessian third-derivative tensor
 258`beta` via Shima's formula, collapses **algebraically** to the closed form
 259`R0101Gen a b lam (t i0)` already certified negative in `ScalarCertificates.lean`. This
 260is the general-`n` non-flatness content: the abstract `n`-dimensional curvature
 261construction of Part 3 genuinely specializes to the certified 2-D formula on any
 2622-sparse slice, for arbitrary ambient dimension `n`. Verified algebraically correct
 263(independent of any `cosh²-sinh²=1` identity) by direct SymPy computation before this
 264proof was written. -/
 265theorem RiemannMixedApply_reduce {n : ℕ} (α t : Vec n) (lam a b : ℝ) (i0 i1 : Fin n)
 266    (hne01 : i0 ≠ i1) (h2 : TwoSparse α i0 i1)
 267    (ha : α i0 = a) (hb : α i1 = b) (ht1 : t i1 = 0)
 268    (ha0 : a ≠ 0) (hlam : 0 < lam) :
 269    RiemannMixedApply (hInvFull α t lam) (beta α t lam) i0 i1 i0 i1
 270      = R0101Gen a b lam (t i0) := by
 271  set t0 := t i0 with ht0_def
 272  have hct0_pos : 0 < Real.cosh t0 := Real.cosh_pos _
 273  have hct0_ne : Real.cosh t0 ≠ 0 := ne_of_gt hct0_pos
 274  have hkap_pos : 0 < kappaGen a b lam t0 := kappaGen_pos a b lam t0 ha0 hlam
 275  have hkap_ne : kappaGen a b lam t0 ≠ 0 := ne_of_gt hkap_pos
 276  -- `dot α t` collapses to `a * t0` on the `TwoSparse` slice with `t i1 = 0`.
 277  have hdot : dot α t = a * t0 := by
 278    unfold dot
 279    have hrestrict := sum_restrict_pair i0 i1 hne01 (fun k => α k * t k)
 280      (fun k hk0 hk1 => by dsimp only; rw [h2 k hk0 hk1]; ring)
 281    dsimp only at hrestrict
 282    rw [hrestrict, ha, hb, ht1]
 283    ring
 284  have hcat : Real.cosh (dot α t) = Real.cosh (a * t0) := by rw [hdot]
 285  have hsat : Real.sinh (dot α t) = Real.sinh (a * t0) := by rw [hdot]
 286  -- `w := sharp (Dinv t) α` at `i0, i1`.
 287  have hw0 : sharp (Dinv t) α i0 = (Real.cosh t0)⁻¹ * a := by
 288    rw [sharp_Dinv_apply, ha]
 289  have hw1 : sharp (Dinv t) α i1 = b := by
 290    rw [sharp_Dinv_apply, hb, ht1, Real.cosh_zero]; ring
 291  have hS : dot α (sharp (Dinv t) α) = (Real.cosh t0)⁻¹ * a ^ 2 + b ^ 2 := by
 292    rw [dot_sharp_Dinv_twoSparse t α i0 i1 hne01 h2, ha, hb, ht1, Real.cosh_zero]
 293    ring
 294  -- The Sherman-Morrison denominator, in closed form: `1+λc·S = κ/cosh t0`.
 295  have hdenom_eq : 1 + lam * Real.cosh (dot α t) * dot α (sharp (Dinv t) α)
 296      = kappaGen a b lam t0 / Real.cosh t0 := by
 297    rw [hcat, hS]
 298    unfold kappaGen
 299    field_simp
 300    ring
 301  -- The four raw `Dinv` values on the block.
 302  have hDinv00 : Dinv t i0 i0 = (Real.cosh t0)⁻¹ := by unfold Dinv; rw [if_pos rfl]
 303  have hDinv01 : Dinv t i0 i1 = 0 := by unfold Dinv; rw [if_neg hne01]
 304  have hDinv11 : Dinv t i1 i1 = 1 := by
 305    unfold Dinv; rw [if_pos rfl, ht1, Real.cosh_zero]; norm_num
 306  -- The four `hInvFull` values on the `{i0,i1}` block, in closed form.
 307  have hInv00 : hInvFull α t lam i0 i0
 308      = (b ^ 2 * lam * Real.cosh (a * t0) + 1) / kappaGen a b lam t0 := by
 309    unfold hInvFull
 310    rw [hDinv00, hdenom_eq, hcat, hw0]
 311    unfold kappaGen
 312    field_simp
 313    ring
 314  have hInv01 : hInvFull α t lam i0 i1
 315      = -(a * b * lam * Real.cosh (a * t0)) / kappaGen a b lam t0 := by
 316    unfold hInvFull
 317    rw [hDinv01, hdenom_eq, hcat, hw0, hw1]
 318    unfold kappaGen
 319    field_simp
 320    ring
 321  have hInv10 : hInvFull α t lam i1 i0
 322      = -(a * b * lam * Real.cosh (a * t0)) / kappaGen a b lam t0 := by
 323    rw [hInvFull_symm]; exact hInv01
 324  have hInv11 : hInvFull α t lam i1 i1
 325      = (a ^ 2 * lam * Real.cosh (a * t0) + Real.cosh t0) / kappaGen a b lam t0 := by
 326    unfold hInvFull
 327    rw [hDinv11, hdenom_eq, hcat, hw1]
 328    unfold kappaGen
 329    field_simp
 330    ring
 331  -- The eight `beta` values on the `{i0,i1}` block.
 332  have hb000 : beta α t lam i0 i0 i0 = Real.sinh t0 + lam * a ^ 3 * Real.sinh (a * t0) := by
 333    unfold beta; rw [if_pos (⟨rfl, rfl⟩ : i0 = i0 ∧ i0 = i0), ha, hsat]; ring
 334  have hb001 : beta α t lam i0 i0 i1 = lam * a ^ 2 * b * Real.sinh (a * t0) := by
 335    unfold beta; rw [if_neg (fun h : i0 = i0 ∧ i0 = i1 => hne01 h.2), ha, hb, hsat]; ring
 336  have hb010 : beta α t lam i0 i1 i0 = lam * a ^ 2 * b * Real.sinh (a * t0) := by
 337    unfold beta; rw [if_neg (fun h : i0 = i1 ∧ i1 = i0 => hne01 h.1), ha, hb, hsat]; ring
 338  have hb011 : beta α t lam i0 i1 i1 = lam * a * b ^ 2 * Real.sinh (a * t0) := by
 339    unfold beta; rw [if_neg (fun h : i0 = i1 ∧ i1 = i1 => hne01 h.1), ha, hb, hsat]; ring
 340  have hb100 : beta α t lam i1 i0 i0 = lam * a ^ 2 * b * Real.sinh (a * t0) := by
 341    unfold beta; rw [if_neg (fun h : i1 = i0 ∧ i0 = i0 => hne01 h.1.symm), ha, hb, hsat]; ring
 342  have hb101 : beta α t lam i1 i0 i1 = lam * a * b ^ 2 * Real.sinh (a * t0) := by
 343    unfold beta; rw [if_neg (fun h : i1 = i0 ∧ i0 = i1 => hne01 h.1.symm), ha, hb, hsat]; ring
 344  have hb110 : beta α t lam i1 i1 i0 = lam * a * b ^ 2 * Real.sinh (a * t0) := by
 345    unfold beta; rw [if_neg (fun h : i1 = i1 ∧ i1 = i0 => hne01 h.2.symm), ha, hb, hsat]; ring
 346  have hb111 : beta α t lam i1 i1 i1 = lam * b ^ 3 * Real.sinh (a * t0) := by
 347    unfold beta; rw [if_pos (⟨rfl, rfl⟩ : i1 = i1 ∧ i1 = i1), ht1, hb, hsat, Real.sinh_zero]; ring
 348  -- Reduce the `m`-sum in `RiemannMixedApply` to `{i0, i1}`: spectator `m` contributes
 349  -- zero because `hInvFull α t lam i0 m = 0` there.
 350  have hspec_m : ∀ m : Fin n, m ≠ i0 → m ≠ i1 →
 351      hInvFull α t lam i0 m *
 352          RiemannLowerApply (hInvFull α t lam) (beta α t lam) m i1 i0 i1 = 0 := by
 353    intro m hm0 hm1
 354    have hzm : α m = 0 := h2 m hm0 hm1
 355    have hz0 : hInvFull α t lam i0 m = 0 := by
 356      rw [hInvFull_symm]
 357      exact hInvFull_spectator α t lam i0 i1 m i0 hm0 hm1 hzm hm0
 358    rw [hz0]; ring
 359  have hmixed : RiemannMixedApply (hInvFull α t lam) (beta α t lam) i0 i1 i0 i1
 360      = hInvFull α t lam i0 i0
 361          * RiemannLowerApply (hInvFull α t lam) (beta α t lam) i0 i1 i0 i1
 362        + hInvFull α t lam i0 i1
 363          * RiemannLowerApply (hInvFull α t lam) (beta α t lam) i1 i1 i0 i1 := by
 364    unfold RiemannMixedApply
 365    exact sum_restrict_pair i0 i1 hne01
 366      (fun m => hInvFull α t lam i0 m *
 367        RiemannLowerApply (hInvFull α t lam) (beta α t lam) m i1 i0 i1)
 368      hspec_m
 369  -- Reduce the `(p,q)`-double sum in `RiemannLowerApply m i1 i0 i1` to `{i0,i1}²`, for
 370  -- any `m` (used below at `m = i0` and `m = i1`).
 371  have hlower_reduce : ∀ m : Fin n,
 372      RiemannLowerApply (hInvFull α t lam) (beta α t lam) m i1 i0 i1
 373        = (1 / 4) *
 374          (hInvFull α t lam i0 i0
 375              * (beta α t lam i1 i0 i0 * beta α t lam m i1 i0
 376                  - beta α t lam m i0 i0 * beta α t lam i1 i1 i0)
 377            + hInvFull α t lam i1 i0
 378              * (beta α t lam i1 i0 i1 * beta α t lam m i1 i0
 379                  - beta α t lam m i0 i1 * beta α t lam i1 i1 i0)
 380            + (hInvFull α t lam i0 i1
 381                * (beta α t lam i1 i0 i0 * beta α t lam m i1 i1
 382                    - beta α t lam m i0 i0 * beta α t lam i1 i1 i1)
 383              + hInvFull α t lam i1 i1
 384                * (beta α t lam i1 i0 i1 * beta α t lam m i1 i1
 385                    - beta α t lam m i0 i1 * beta α t lam i1 i1 i1))) := by
 386    intro m
 387    unfold RiemannLowerApply
 388    congr 1
 389    exact sum2_restrict_pair i0 i1 hne01
 390      (fun p q => hInvFull α t lam p q *
 391        (beta α t lam i1 i0 p * beta α t lam m i1 q
 392          - beta α t lam m i0 p * beta α t lam i1 i1 q))
 393                  (fun p q hpq => by
 394                    dsimp only
 395                    rw [riemann_beta_numerator_zero α t lam i0 i1 hne01 h2 m p q hpq]; ring)
 396  rw [hmixed, hlower_reduce i0, hlower_reduce i1,
 397    hInv00, hInv01, hInv10, hInv11,
 398    hb000, hb001, hb010, hb011, hb100, hb101, hb110, hb111]
 399  unfold R0101Gen
 400  field_simp
 401  ring
 402
 403/-- **Theorem 2, general `n`.** Under the block-diagonal hypotheses plus `b ≠ 0` and
 404`t i0 ≠ 0`, the mixed Riemann tensor `R^{i0}_{i1,i0,i1}` of the *actual* `n`-dimensional
 405deformed metric `h_λ` is strictly negative: `h_λ` is genuinely non-flat, for any
 406ambient dimension `n` and any `α` supported on two coordinates. This is the honest
 407general-`n` generalization of `R0101Gen_neg` (`ScalarCertificates.lean`), assembled
 408from the algebraic reduction above plus the already-certified 2-D negativity. -/
 409theorem RiemannMixedApply_neg {n : ℕ} (α t : Vec n) (lam a b : ℝ) (i0 i1 : Fin n)
 410    (hne01 : i0 ≠ i1) (h2 : TwoSparse α i0 i1)
 411    (ha : α i0 = a) (hb : α i1 = b) (ht1 : t i1 = 0)
 412    (ha0 : a ≠ 0) (hb0 : b ≠ 0) (hlam : 0 < lam) (ht0 : t i0 ≠ 0) :
 413    RiemannMixedApply (hInvFull α t lam) (beta α t lam) i0 i1 i0 i1 < 0 := by
 414  rw [RiemannMixedApply_reduce α t lam a b i0 i1 hne01 h2 ha hb ht1 ha0 hlam]
 415  exact R0101Gen_neg a b lam (t i0) ha0 hb0 hlam ht0
 416
 417end
 418
 419end Ndim
 420end Cost
 421end IndisputableMonolith
 422