Encyclopedia Cost Cost Ndim Curvature Bridge Riemann Beta Numerator Zero

ARTICLE 3 claims 3 theorems

Cost Ndim Curvature Bridge Riemann Beta Numerator Zero

A single algebraic identity about a sum of products that must be zero, and the role it plays in a larger proof about the geometry of a deformed metric.

Verify this page

A vanishing term in the curvature sum

In differential geometry, the Riemann curvature tensor measures how much a space bends. For a special class of spaces called Hessian metrics, where the metric comes from a potential function, the curvature has a concrete formula. The declaration riemann_beta_numerator_zero establishes one precise algebraic fact inside that formula: under certain conditions, a specific combination of terms in the curvature sum is exactly zero.

The setting is a deformed metric built from a diagonal base plus a rank-one update. The potential is a sum of hyperbolic cosines plus a coupling term. The curvature is computed using Shima's formula, which sums over pairs of indices. The declaration states that if the vector α has support on only two coordinates, and if either index in the pair is outside that support, then the product of two third-derivative terms minus the product of two other third-derivative terms equals zero. This is a purely algebraic identity, proved by direct manipulation of sums, with no geometric approximation.

The identity is a lemma, not a standalone result. It is a stepping stone in a larger proof. The larger goal is to show that the deformed metric is genuinely non-flat, meaning its Riemann tensor has a nonzero component. The vanishing term simplifies the curvature sum, allowing it to collapse to a known negative value. This is the general-n non-flatness content: the abstract n-dimensional curvature construction specializes to a certified 2-D formula on any two-sparse slice.

What this declaration does not claim is equally important. It does not assert that the full Riemann tensor is negative, nor that the metric is non-flat. It does not claim anything about the physical significance of the curvature. It only establishes that a particular algebraic expression is zero under stated hypotheses. The negativity of the curvature component is a separate theorem, RiemannMixedApply_neg, which uses this lemma as one ingredient.

THEOREM riemann_beta_numerator_zero · IndisputableMonolith/Cost/Ndim/CurvatureBridge.lean
riemann_beta_numerator_zero · IndisputableMonolith/Cost/Ndim/CurvatureBridge.lean:232 
/-- The core vanishing fact driving the Riemann reduction: for `p` or `q` off the
`TwoSparse` support, every term of Shima's `(p,q)`-summand built from `β` at
`(i1, i0, ·)`/`(m, i0, ·)`/`(m, i1, ·)`/`(i1, i1, ·)` vanishes, regardless of `m`. -/
theorem riemann_beta_numerator_zero {n : ℕ} (α t : Vec n) (lam : ℝ) (i0 i1 : Fin n)
    (hne01 : i0 ≠ i1) (h2 : TwoSparse α i0 i1) (m p q : Fin n)
    (hspec : (p ≠ i0 ∧ p ≠ i1) ∨ (q ≠ i0 ∧ q ≠ i1)) :
    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
  rcases hspec with ⟨hp0, hp1⟩ | ⟨hq0, hq1⟩
  · have hzp : α p = 0 := h2 p hp0 hp1
    have h1 : beta α t lam i1 i0 p = 0 :=
      beta_eq_zero α t lam i1 i0 p (Or.inr (Or.inr hzp)) (fun h => hne01 h.1.symm)
    have h3 : beta α t lam m i0 p = 0 :=
      beta_eq_zero α t lam m i0 p (Or.inr (Or.inr hzp)) (fun h => hp0 h.2.symm)
    rw [h1, h3]; ring
  · have hzq : α q = 0 := h2 q hq0 hq1
    have h1 : beta α t lam m i1 q = 0 :=
      beta_eq_zero α t lam m i1 q (Or.inr (Or.inr hzq)) (fun h => hq1 h.2.symm)
    have h3 : beta α t lam i1 i1 q = 0 :=
      beta_eq_zero α t lam i1 i1 q (Or.inr (Or.inr hzq)) (fun h => hq1 h.2.symm)
    rw [h1, h3]; ring
THEOREM RiemannMixedApply_reduce · IndisputableMonolith/Cost/Ndim/CurvatureBridge.lean
RiemannMixedApply_reduce · IndisputableMonolith/Cost/Ndim/CurvatureBridge.lean:255 
/-- **Stage B capstone reduction.** Under a `TwoSparse` `α` (support `{i0, i1}`) and
`t i1 = 0`, the general-`n` mixed Riemann component `R^{i0}_{i1,i0,i1}`, built from the
*actual* deformed metric `hFull`/`hInvFull` and its Hessian third-derivative tensor
`beta` via Shima's formula, collapses **algebraically** to the closed form
`R0101Gen a b lam (t i0)` already certified negative in `ScalarCertificates.lean`. This
is the general-`n` non-flatness content: the abstract `n`-dimensional curvature
construction of Part 3 genuinely specializes to the certified 2-D formula on any
2-sparse slice, for arbitrary ambient dimension `n`. Verified algebraically correct
(independent of any `cosh²-sinh²=1` identity) by direct SymPy computation before this
proof was written. -/
theorem RiemannMixedApply_reduce {n : ℕ} (α t : Vec n) (lam a b : ℝ) (i0 i1 : Fin n)
    (hne01 : i0 ≠ i1) (h2 : TwoSparse α i0 i1)
    (ha : α i0 = a) (hb : α i1 = b) (ht1 : t i1 = 0)
    (ha0 : a ≠ 0) (hlam : 0 < lam) :
    RiemannMixedApply (hInvFull α t lam) (beta α t lam) i0 i1 i0 i1
      = R0101Gen a b lam (t i0) := by
  set t0 := t i0 with ht0_def
  have hct0_pos : 0 < Real.cosh t0 := Real.cosh_pos _
  have hct0_ne : Real.cosh t0 ≠ 0 := ne_of_gt hct0_pos
  have hkap_pos : 0 < kappaGen a b lam t0 := kappaGen_pos a b lam t0 ha0 hlam
  have hkap_ne : kappaGen a b lam t0 ≠ 0 := ne_of_gt hkap_pos
  -- `dot α t` collapses to `a * t0` on the `TwoSparse` slice with `t i1 = 0`.
  have hdot : dot α t = a * t0 := by
    unfold dot
    have hrestrict := sum_restrict_pair i0 i1 hne01 (fun k => α k * t k)
      (fun k hk0 hk1 => by dsimp only; rw [h2 k hk0 hk1]; ring)
    dsimp only at hrestrict
    rw [hrestrict, ha, hb, ht1]
    ring
  have hcat : Real.cosh (dot α t) = Real.cosh (a * t0) := by rw [hdot]
  have hsat : Real.sinh (dot α t) = Real.sinh (a * t0) := by rw [hdot]
  -- `w := sharp (Dinv t) α` at `i0, i1`.
  have hw0 : sharp (Dinv t) α i0 = (Real.cosh t0)⁻¹ * a := by
    rw [sharp_Dinv_apply, ha]
  have hw1 : sharp (Dinv t) α i1 = b := by
    rw [sharp_Dinv_apply, hb, ht1, Real.cosh_zero]; ring
  have hS : dot α (sharp (Dinv t) α) = (Real.cosh t0)⁻¹ * a ^ 2 + b ^ 2 := by
    rw [dot_sharp_Dinv_twoSparse t α i0 i1 hne01 h2, ha, hb, ht1, Real.cosh_zero]
    ring
  -- The Sherman-Morrison denominator, in closed form: `1+λc·S = κ/cosh t0`.
  have hdenom_eq : 1 + lam * Real.cosh (dot α t) * dot α (sharp (Dinv t) α)
      = kappaGen a b lam t0 / Real.cosh t0 := by
    rw [hcat, hS]
    unfold kappaGen
    field_simp
    ring
  -- The four raw `Dinv` values on the block.
  have hDinv00 : Dinv t i0 i0 = (Real.cosh t0)⁻¹ := by unfold Dinv; rw [if_pos rfl]
  have hDinv01 : Dinv t i0 i1 = 0 := by unfold Dinv; rw [if_neg hne01]
  have hDinv11 : Dinv t i1 i1 = 1 := by
    unfold Dinv; rw [if_pos rfl, ht1, Real.cosh_zero]; norm_num
  -- The four `hInvFull` values on the `{i0,i1}` block, in closed form.
  have hInv00 : hInvFull α t lam i0 i0
      = (b ^ 2 * lam * Real.cosh (a * t0) + 1) / kappaGen a b lam t0 := by
    unfold hInvFull
    rw [hDinv00, hdenom_eq, hcat, hw0]
    unfold kappaGen
    field_simp
    ring
  have hInv01 : hInvFull α t lam i0 i1
      = -(a * b * lam * Real.cosh (a * t0)) / kappaGen a b lam t0 := by
    unfold hInvFull
    rw [hDinv01, hdenom_eq, hcat, hw0, hw1]
    unfold kappaGen
    field_simp
    ring
  have hInv10 : hInvFull α t lam i1 i0
      = -(a * b * lam * Real.cosh (a * t0)) / kappaGen a b lam t0 := by
    rw [hInvFull_symm]; exact hInv01
  have hInv11 : hInvFull α t lam i1 i1
      = (a ^ 2 * lam * Real.cosh (a * t0) + Real.cosh t0) / kappaGen a b lam t0 := by
    unfold hInvFull
    rw [hDinv11, hdenom_eq, hcat, hw1]
    unfold kappaGen
    field_simp
    ring
  -- The eight `beta` values on the `{i0,i1}` block.
  have hb000 : beta α t lam i0 i0 i0 = Real.sinh t0 + lam * a ^ 3 * Real.sinh (a * t0) := by
    unfold beta; rw [if_pos (⟨rfl, rfl⟩ : i0 = i0 ∧ i0 = i0), ha, hsat]; ring
  have hb001 : beta α t lam i0 i0 i1 = lam * a ^ 2 * b * Real.sinh (a * t0) := by
    unfold beta; rw [if_neg (fun h : i0 = i0 ∧ i0 = i1 => hne01 h.2), ha, hb, hsat]; ring
  have hb010 : beta α t lam i0 i1 i0 = lam * a ^ 2 * b * Real.sinh (a * t0) := by
    unfold beta; rw [if_neg (fun h : i0 = i1 ∧ i1 = i0 => hne01 h.1), ha, hb, hsat]; ring
  have hb011 : beta α t lam i0 i1 i1 = lam * a * b ^ 2 * Real.sinh (a * t0) := by
    unfold beta; rw [if_neg (fun h : i0 = i1 ∧ i1 = i1 => hne01 h.1), ha, hb, hsat]; ring
  have hb100 : beta α t lam i1 i0 i0 = lam * a ^ 2 * b * Real.sinh (a * t0) := by
    unfold beta; rw [if_neg (fun h : i1 = i0 ∧ i0 = i0 => hne01 h.1.symm), ha, hb, hsat]; ring
  have hb101 : beta α t lam i1 i0 i1 = lam * a * b ^ 2 * Real.sinh (a * t0) := by
    unfold beta; rw [if_neg (fun h : i1 = i0 ∧ i0 = i1 => hne01 h.1.symm), ha, hb, hsat]; ring
  have hb110 : beta α t lam i1 i1 i0 = lam * a * b ^ 2 * Real.sinh (a * t0) := by
    unfold beta; rw [if_neg (fun h : i1 = i1 ∧ i1 = i0 => hne01 h.2.symm), ha, hb, hsat]; ring
  have hb111 : beta α t lam i1 i1 i1 = lam * b ^ 3 * Real.sinh (a * t0) := by
    unfold beta; rw [if_pos (⟨rfl, rfl⟩ : i1 = i1 ∧ i1 = i1), ht1, hb, hsat, Real.sinh_zero]; ring
  -- Reduce the `m`-sum in `RiemannMixedApply` to `{i0, i1}`: spectator `m` contributes
  -- zero because `hInvFull α t lam i0 m = 0` there.
  have hspec_m : ∀ m : Fin n, m ≠ i0 → m ≠ i1 →
      hInvFull α t lam i0 m *
          RiemannLowerApply (hInvFull α t lam) (beta α t lam) m i1 i0 i1 = 0 := by
    intro m hm0 hm1
    have hzm : α m = 0 := h2 m hm0 hm1
    have hz0 : hInvFull α t lam i0 m = 0 := by
      rw [hInvFull_symm]
      exact hInvFull_spectator α t lam i0 i1 m i0 hm0 hm1 hzm hm0
    rw [hz0]; ring
  have hmixed : RiemannMixedApply (hInvFull α t lam) (beta α t lam) i0 i1 i0 i1
      = hInvFull α t lam i0 i0
          * RiemannLowerApply (hInvFull α t lam) (beta α t lam) i0 i1 i0 i1
        + hInvFull α t lam i0 i1
          * RiemannLowerApply (hInvFull α t lam) (beta α t lam) i1 i1 i0 i1 := by
    unfold RiemannMixedApply
    exact sum_restrict_pair i0 i1 hne01
      (fun m => hInvFull α t lam i0 m *
        RiemannLowerApply (hInvFull α t lam) (beta α t lam) m i1 i0 i1)
      hspec_m
  -- Reduce the `(p,q)`-double sum in `RiemannLowerApply m i1 i0 i1` to `{i0,i1}²`, for
  -- any `m` (used below at `m = i0` and `m = i1`).
  have hlower_reduce : ∀ m : Fin n,
      RiemannLowerApply (hInvFull α t lam) (beta α t lam) m i1 i0 i1
        = (1 / 4) *
          (hInvFull α t lam i0 i0
              * (beta α t lam i1 i0 i0 * beta α t lam m i1 i0
                  - beta α t lam m i0 i0 * beta α t lam i1 i1 i0)
            + hInvFull α t lam i1 i0
              * (beta α t lam i1 i0 i1 * beta α t lam m i1 i0
                  - beta α t lam m i0 i1 * beta α t lam i1 i1 i0)
            + (hInvFull α t lam i0 i1
                * (beta α t lam i1 i0 i0 * beta α t lam m i1 i1
                    - beta α t lam m i0 i0 * beta α t lam i1 i1 i1)
              + hInvFull α t lam i1 i1
                * (beta α t lam i1 i0 i1 * beta α t lam m i1 i1
                    - beta α t lam m i0 i1 * beta α t lam i1 i1 i1))) := by
    intro m
    unfold RiemannLowerApply
    congr 1
    exact sum2_restrict_pair i0 i1 hne01
      (fun p q => hInvFull α t lam p q *
        (beta α t lam i1 i0 p * beta α t lam m i1 q
          - beta α t lam m i0 p * beta α t lam i1 i1 q))
                  (fun p q hpq => by
                    dsimp only
                    rw [riemann_beta_numerator_zero α t lam i0 i1 hne01 h2 m p q hpq]; ring)
  rw [hmixed, hlower_reduce i0, hlower_reduce i1,
    hInv00, hInv01, hInv10, hInv11,
    hb000, hb001, hb010, hb011, hb100, hb101, hb110, hb111]
  unfold R0101Gen
  field_simp
  ring
THEOREM riemann_beta_numerator_zero · IndisputableMonolith/Cost/Ndim/CurvatureBridge.lean
riemann_beta_numerator_zero · IndisputableMonolith/Cost/Ndim/CurvatureBridge.lean:232 
/-- The core vanishing fact driving the Riemann reduction: for `p` or `q` off the
`TwoSparse` support, every term of Shima's `(p,q)`-summand built from `β` at
`(i1, i0, ·)`/`(m, i0, ·)`/`(m, i1, ·)`/`(i1, i1, ·)` vanishes, regardless of `m`. -/
theorem riemann_beta_numerator_zero {n : ℕ} (α t : Vec n) (lam : ℝ) (i0 i1 : Fin n)
    (hne01 : i0 ≠ i1) (h2 : TwoSparse α i0 i1) (m p q : Fin n)
    (hspec : (p ≠ i0 ∧ p ≠ i1) ∨ (q ≠ i0 ∧ q ≠ i1)) :
    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
  rcases hspec with ⟨hp0, hp1⟩ | ⟨hq0, hq1⟩
  · have hzp : α p = 0 := h2 p hp0 hp1
    have h1 : beta α t lam i1 i0 p = 0 :=
      beta_eq_zero α t lam i1 i0 p (Or.inr (Or.inr hzp)) (fun h => hne01 h.1.symm)
    have h3 : beta α t lam m i0 p = 0 :=
      beta_eq_zero α t lam m i0 p (Or.inr (Or.inr hzp)) (fun h => hp0 h.2.symm)
    rw [h1, h3]; ring
  · have hzq : α q = 0 := h2 q hq0 hq1
    have h1 : beta α t lam m i1 q = 0 :=
      beta_eq_zero α t lam m i1 q (Or.inr (Or.inr hzq)) (fun h => hq1 h.2.symm)
    have h3 : beta α t lam i1 i1 q = 0 :=
      beta_eq_zero α t lam i1 i1 q (Or.inr (Or.inr hzq)) (fun h => hq1 h.2.symm)
    rw [h1, h3]; ring

What this page does not claim

The declaration does not prove that the metric is non-flat. The declaration does not establish any property of the full Riemann tensor. The declaration does not claim any physical significance for the vanishing term.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/Ndim/CurvatureBridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND