Encyclopedia Cost Cost Ndim Curvature Bridge H Full Mul H Inv Full

ARTICLE 3 claims 3 theorems

Cost Ndim Curvature Bridge H Full Mul H Inv Full

In any number of dimensions, a certain deformed geometry has a two-sided inverse, a fact that later proves the space is curved.

Verify this page

The inverse metric

A metric is a rule for measuring distances and angles in a space. In the Recognition Science framework, a specific deformed metric is built by starting with a simple diagonal one and adding a rank-one perturbation. The declaration hFull_mul_hInvFull proves that this deformed metric, called hFull, has a genuine two-sided inverse, called hInvFull. This holds for any ambient dimension n, with no sparsity assumptions. The proof uses the Sherman-Morrison formula, a standard linear algebra tool for inverting a matrix after a rank-one update.

The inverse is not just a formal object. Its existence is the load-bearing step for proving that the deformed metric is non-flat, meaning the space it describes is genuinely curved. The theorem states that multiplying hFull by its inverse on either side yields the identity matrix. This is the algebraic foundation for the later curvature calculation, which shows a specific component of the Riemann tensor is strictly negative. That negativity is the signature of curvature.

In Recognition Science, this is part of a chain of forced results. The framework models physical structure from a ledger of recognition events, and this theorem is a step in deriving the geometry of space. The declaration itself, however, does not claim that the metric is non-flat. It only establishes the inverse. The non-flatness is a separate, later theorem that builds on this one. The declaration also does not claim anything about the physical interpretation of the metric or its components, only their algebraic relationship.

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 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 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

What this page does not claim

The declaration does not prove that the metric is non-flat. The declaration does not make any claims about the physical interpretation of the metric. The declaration does not require any sparsity assumptions on the perturbation vector.

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