Cost Ndim Curvature Bridge H Inv Full Spectator

The spectator index

In the Recognition Science framework, a recognition event is a discrete record of a comparison, and its cost is a forced number, not a choice. The framework's library, a machine-checked collection of formal theorems, models the geometry of these costs with a deformed metric. This metric is a rule for measuring distances in a space whose shape is bent by the cost function. The declaration hInvFull_spectator is a small but load-bearing algebraic fact about that metric: it says that if a coordinate direction has zero weight in the deformation, then the inverse metric has no off-diagonal entries connecting that direction to any other.

Concretely, the metric is built from a diagonal part plus a rank-one update. The inverse metric, which is what you use to compute distances and angles, is given by a standard formula called the Sherman-Morrison identity. The declaration hInvFull_spectator proves that this inverse vanishes in a specific case: when one index corresponds to a coordinate where the deformation weight α is zero, and that index is not equal to the other index. The proof is a direct algebraic manipulation of the definition, using the fact that the correction term in the Sherman-Morrison formula is proportional to the weight, which is zero. This is not a theorem about physics; it is a theorem about the algebraic structure of the framework's own construction.

The payoff is in what the lemma enables. In the framework's curvature bridge, the Riemann tensor, a measure of how much the space is bent, is built from sums over all pairs of coordinates. The lemma hInvFull_spectator, together with a companion result for the third-derivative tensor, shows that any coordinate with zero weight contributes nothing to those sums. The sums collapse to the two coordinates that actually carry the deformation weight. This is what makes the general-n-dimensional curvature computation tractable: most of the space is a silent spectator, and the curvature is determined entirely by the active slice.

What the declaration does not claim is equally precise. It does not say that the metric itself is flat or that the space is trivial. It only states a vanishing condition for the inverse metric in a specific index configuration. It does not prove that the Riemann tensor is negative, which is a separate theorem (RiemannMixedApply_neg) that requires additional hypotheses, including nonzero weights and a nonzero coordinate value. The lemma is a necessary step, not the whole argument. It also does not make any claim about the physical meaning of the spectator coordinates; it is a purely formal statement about the framework's algebraic objects.

/-- `hInvFull` vanishes whenever one argument is a spectator index (`α = 0`, off the
`TwoSparse` support): the Sherman-Morrison correction term is proportional to
`w_k = (cosh t_k)⁻¹ α_k`, which vanishes there, leaving only the *off-diagonal* part
of the (diagonal) `Dinv`, which is itself zero. -/
theorem hInvFull_spectator {n : ℕ} (α t : Vec n) (lam : ℝ) (i0 i1 k j : Fin n)
    (hk0 : k ≠ i0) (hk1 : k ≠ i1) (hz : α k = 0) (hkj : k ≠ j) :
    hInvFull α t lam k j = 0 := by
  unfold hInvFull
  rw [sharp_Dinv_apply t α k, hz]
  unfold Dinv
  rw [if_neg hkj]
  ring

/-- `β_{ijk}` vanishes whenever one of its indices carries a zero `α`-component and the
diagonal term does not fire. This is the key structural fact driving the
block-diagonal collapse of the Riemann sum: a spectator index (`α = 0`, off the
`TwoSparse` support) kills every summand it appears in. -/
theorem beta_eq_zero {n : ℕ} (α t : Vec n) (lam : ℝ) (i j k : Fin n)
    (hz : α i = 0 ∨ α j = 0 ∨ α k = 0) (hne : ¬ (i = j ∧ j = k)) :
    beta α t lam i j k = 0 := by
  unfold beta
  rw [if_neg hne]
  rcases hz with h | h | h <;> rw [h] <;> ring

/-- 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 lemma does not prove that the deformed metric is flat. The lemma does not establish that the Riemann tensor is negative. The lemma makes no claim about the physical meaning of coordinates with zero weight.

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: