Encyclopedia Cost Cost Ndim Curvature Bridge Riemann Mixed Apply Reduce

ARTICLE 3 claims 3 theorems

Cost Ndim Curvature Bridge Riemann Mixed Apply Reduce

A machine-checked proof shows that a certain high-dimensional geometric object, built from a deformed metric, reduces exactly to a known two-dimensional formula under specific conditions.

Verify this page

The curvature bridge

The Riemann tensor is a standard object in differential geometry that measures how much a space curves. In any number of dimensions, it is a large collection of numbers, one for each choice of four directions. The declaration RiemannMixedApply_reduce in the framework's machine-checked library of formal theorems proves a precise statement about one such number, built from a particular kind of metric called a Hessian metric, which comes from a potential function.

A space whose geometry is defined by a function of several variables. The metric, which tells you how to measure distances, is the matrix of second derivatives of that function. The declaration considers a specific deformed metric, written as a diagonal part plus a rank-one correction, and its inverse. It then builds the Riemann tensor component R with indices (i0, i1, i0, i1) using a standard curvature formula. The theorem states that, under two conditions, this complicated high-dimensional number collapses exactly to a much simpler closed form, called R0101Gen, which is already known to be negative.

The two conditions are that the vector α, which controls the deformation, is supported on only two coordinates (i0 and i1), and that the coordinate t i1 is zero. When these hold, the theorem proves that the full n-dimensional curvature component equals the two-dimensional formula, for any ambient dimension n. This is a genuine reduction: it shows that the abstract high-dimensional construction is consistent with the earlier two-dimensional result, not an approximation but an exact algebraic identity.

In Recognition Science, this is a step toward showing that the deformed metric is genuinely curved, not flat. A separate theorem, RiemannMixedApply_neg, uses this reduction to prove that the same component is strictly negative under slightly stronger conditions, namely that both α components are non-zero and t i0 is non-zero. This negativity is the mathematical content of non-flatness for this component.

What the declaration does not claim is just as important. It does not prove that the entire Riemann tensor is negative, only one specific component. It does not apply to arbitrary deformations, only to those with support on two coordinates and with t i1 = 0. It does not claim that the metric is non-flat in any global sense; it establishes a property of a single curvature component. The reduction is algebraic, and it does not depend on any trigonometric identity, as the documentation notes.

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 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 RiemannMixedApply_neg · IndisputableMonolith/Cost/Ndim/CurvatureBridge.lean
RiemannMixedApply_neg · IndisputableMonolith/Cost/Ndim/CurvatureBridge.lean:403 
/-- **Theorem 2, general `n`.** Under the block-diagonal hypotheses plus `b ≠ 0` and
`t i0 ≠ 0`, the mixed Riemann tensor `R^{i0}_{i1,i0,i1}` of the *actual* `n`-dimensional
deformed metric `h_λ` is strictly negative: `h_λ` is genuinely non-flat, for any
ambient dimension `n` and any `α` supported on two coordinates. This is the honest
general-`n` generalization of `R0101Gen_neg` (`ScalarCertificates.lean`), assembled
from the algebraic reduction above plus the already-certified 2-D negativity. -/
theorem RiemannMixedApply_neg {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) (hb0 : b ≠ 0) (hlam : 0 < lam) (ht0 : t i0 ≠ 0) :
    RiemannMixedApply (hInvFull α t lam) (beta α t lam) i0 i1 i0 i1 < 0 := by
  rw [RiemannMixedApply_reduce α t lam a b i0 i1 hne01 h2 ha hb ht1 ha0 hlam]
  exact R0101Gen_neg a b lam (t i0) ha0 hb0 hlam ht0

What this page does not claim

The declaration does not prove that the entire Riemann tensor is negative, only one specific component. The theorem does not apply to arbitrary deformations, only to those with support on two coordinates and with t i1 = 0. The reduction does not establish global non-flatness of the metric, only a property of a single curvature component.

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