Encyclopedia Cost Cost Ndim Curvature Bridge

ARTICLE 3 claims 3 theorems

Cost Ndim Curvature Bridge

A machine-checked proof that a deformed geometric object is curved in any number of dimensions, not just the familiar two.

Verify this page

The curvature bridge

In differential geometry, a Hessian metric is a way to measure distances and angles that comes from taking second derivatives of a single smooth function, called a potential. The curvature bridge is a result in Recognition Science that takes a specific Hessian metric, deforms it by adding a small term, and proves that the result is genuinely curved, no matter how many dimensions the space has. The proof is carried out in a machine-checked library of formal theorems, meaning every algebraic step is verified by a computer.

The construction starts with a potential function Φλ(t) = Σi cosh(ti) + λ(cosh(α·t) − 1). Here t is a vector of coordinates, α is a fixed vector that picks out a direction, and λ is a small positive number that controls the size of the deformation. The Hessian metric hλ is the matrix of second derivatives of this potential. The module builds this metric as a bare array of real numbers, then uses the Sherman-Morrison formula to write down its inverse explicitly. The key theorem here, hFull_mul_hInvFull, proves that this inverse really is the two-sided inverse for any dimension n, with no simplifying assumptions about the number of coordinates.

The next step is to compute curvature. The module uses Shima's formula, which expresses the Riemann tensor of a Hessian metric in terms of the third derivatives of the potential. It builds the third-derivative tensor βijk = ∂i∂j∂kΦλ and then assembles the full Riemann tensor. The capstone theorem, RiemannMixedApply_neg, shows that a particular component of this tensor, Ri0i1,i0,i1, is strictly negative whenever α is supported on just two coordinates and the parameter ti1 is zero. A negative Riemann component means the space is curved, not flat. The proof works by showing that this general-n component collapses algebraically to a closed form, R0101Gen, that was already certified to be negative in a separate scalar certificate file.

What this establishes in plain language is that the deformation introduced by the λ term forces genuine curvature in any ambient dimension. The result does not rely on the space being two-dimensional; it holds for arbitrary n. The proof is notable for its method: it works with bare arrays and syntactic indices rather than abstract manifold machinery, and it avoids a common shortcut argument about connections on submanifolds that the project's panel flagged as dead. The negativity of the Riemann component is the honest, general-n version of an earlier two-dimensional result, and it is what the framework means when it says the deformed metric is non-flat.

THEOREM hFull_mul_hInvFull · IndisputableMonolith/Cost/Ndim/CurvatureBridge.lean
hFull_mul_hInvFull · IndisputableMonolith/Cost/Ndim/CurvatureBridge.lean:74 
/-- **The Sherman-Morrison identity.** For any ambient dimension `n`, `hInvFull` really
is the two-sided inverse of `hFull`, provided the Sherman-Morrison denominator
`1 + λc·S` is nonzero (`S = dot α (D⁻¹α)`, `c = cosh(dot α t)`). This is the genuinely
`n`-dimensional content this module adds: no `TwoSparse` hypothesis anywhere in this
theorem. -/
theorem hFull_mul_hInvFull {n : ℕ} (α t : Vec n) (lam : ℝ) (i j : Fin n)
    (hdenom : 1 + lam * Real.cosh (dot α t) * dot α (sharp (Dinv t) α) ≠ 0) :
    ∑ k : Fin n, hFull α t lam i k * hInvFull α t lam k j = if i = j then (1 : ℝ) else 0 := by
  set c := Real.cosh (dot α t) with hc_def
  set w := sharp (Dinv t) α with hw_def
  set S := dot α w with hS_def
  have hSsum : S = ∑ k : Fin n, α k * w k := by rw [hS_def]; rfl
  have hwj : ∀ k : Fin n, w k = (Real.cosh (t k))⁻¹ * α k := fun k => sharp_Dinv_apply t α k
  have hstep1 : ∑ k : Fin n, hFull α t lam i k * Dinv t k j
      = (if i = j then (1 : ℝ) else 0) + lam * c * α i * w j := by
    rw [Finset.sum_eq_single j]
    · unfold Dinv
      rw [if_pos rfl]
      unfold hFull
      by_cases hij : i = j
      · subst hij
        rw [if_pos rfl, if_pos rfl, hwj i]
        have hne : Real.cosh (t i) ≠ 0 := ne_of_gt (Real.cosh_pos _)
        field_simp
        ring
      · rw [if_neg hij, if_neg hij, hwj j]
        ring
    · intro k _ hk
      unfold Dinv
      rw [if_neg hk]
      ring
    · intro h
      exact absurd (Finset.mem_univ j) h
  have hstep2 : ∑ k : Fin n, hFull α t lam i k * w k = α i * (1 + lam * c * S) := by
    have hexp : ∀ k : Fin n, hFull α t lam i k * w k
        = (if i = k then Real.cosh (t i) * w k else 0) + lam * c * α i * (α k * w k) := by
      intro k
      unfold hFull
      by_cases hik : i = k
      · rw [if_pos hik, if_pos hik]; ring
      · rw [if_neg hik, if_neg hik]; ring
    rw [Finset.sum_congr rfl (fun k _ => hexp k), Finset.sum_add_distrib]
    have hpart1 : ∑ k : Fin n, (if i = k then Real.cosh (t i) * w k else 0)
        = Real.cosh (t i) * w i := by
      rw [Finset.sum_ite_eq (Finset.univ : Finset (Fin n)) i (fun k => Real.cosh (t i) * w k)]
      simp
    have hpart2 : ∑ k : Fin n, lam * c * α i * (α k * w k) = lam * c * α i * S := by
      rw [← Finset.mul_sum, ← hSsum]
    rw [hpart1, hpart2, hwj i]
    have hne : Real.cosh (t i) ≠ 0 := ne_of_gt (Real.cosh_pos _)
    field_simp
  have hsplit : ∑ k : Fin n, hFull α t lam i k * hInvFull α t lam k j
      = ∑ k : Fin n, hFull α t lam i k * Dinv t k j
        - (lam * c / (1 + lam * c * S)) * w j * ∑ k : Fin n, hFull α t lam i k * w k := by
    have heach : ∀ k : Fin n, hFull α t lam i k * hInvFull α t lam k j
        = hFull α t lam i k * Dinv t k j
          - (lam * c / (1 + lam * c * S)) * w j * (hFull α t lam i k * w k) := by
      intro k
      unfold hInvFull
      ring
    rw [Finset.sum_congr rfl (fun k _ => heach k), Finset.sum_sub_distrib, ← Finset.mul_sum]
  rw [hsplit, hstep1, hstep2]
  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

This answer does not claim that the curvature bridge derives the fine-structure constant or any specific coupling constant. This answer does not claim that the Riemann tensor of the deformed metric is non-flat in all components, only the specific mixed component proved negative. This answer does not claim that the physical recognition-to-linking bridge, which would connect this curvature result to three-dimensional space, is proved.

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