Cost Ndim Curvature Bridge Sum2 Restrict Pair

The two-index collapse

The declaration sum2_restrict_pair is a lemma about finite sums. One can have a function of two indices, and you know that the function is zero unless both indices belong to a chosen pair, say i0 and i1. The lemma states that the double sum over all indices equals the sum of just the four values at the pairs (i0,i0), (i1,i0), (i0,i1), and (i1,i1). In plainer terms: if a two-variable function only takes nonzero values on a two-by-two block, then summing it over the whole index set is the same as summing it over just that block.

This is a purely combinatorial fact about finite sums; it does not involve geometry, physics, or any special property of the function beyond its vanishing outside the pair. It is a tool. The proof in the machine-checked library of formal theorems is a direct manipulation of finite sums, using the standard fact that a sum over a set equals a sum over a subset when the function vanishes outside the subset.

In Recognition Science, this lemma appears as a step in a larger argument about curvature. The framework models recognition events as points in a space, and it defines a deformed metric on that space. The metric is built from a potential function, and its curvature is computed using a standard formula. The calculation involves sums over all pairs of indices. The lemma lets the framework reduce those sums to a two-dimensional slice when the metric's defining vector is supported on only two coordinates.

The payoff is that a high-dimensional curvature component collapses to a known two-dimensional formula. This is part of a proof that the deformed metric is genuinely non-flat in any ambient dimension, provided the vector is supported on two coordinates. The lemma itself does not establish non-flatness; it only provides the reduction step. The negativity of the resulting two-dimensional formula is a separate result, proved elsewhere in the library.

What the lemma does not claim is just as important. It does not say anything about the values of the function on the pair; it only says the sum collapses. It does not require the function to be symmetric, continuous, or differentiable. It does not depend on the dimension of the ambient space, as long as the pair of indices exists. It is a statement about sums, not about geometry. The geometric content lives in the theorems that use this lemma, not in the lemma itself.

/-- The double-sum analogue of `sum_restrict_pair`: a function of two arguments
vanishing whenever *either* argument is off `{i0, i1}` collapses to its four values on
the `{i0,i1} × {i0,i1}` support. -/
theorem sum2_restrict_pair {n : ℕ} (i0 i1 : Fin n) (hne : i0 ≠ i1) (f : Fin n → Fin n → ℝ)
    (hz : ∀ p q : Fin n, (p ≠ i0 ∧ p ≠ i1) ∨ (q ≠ i0 ∧ q ≠ i1) → f p q = 0) :
    ∑ p : Fin n, ∑ q : Fin n, f p q = f i0 i0 + f i1 i0 + (f i0 i1 + f i1 i1) := by
  have hFin : ∀ p : Fin n, ∑ q : Fin n, f p q = f p i0 + f p i1 := by
    intro p
    apply sum_restrict_pair i0 i1 hne (f p)
    intro q hq0 hq1
    exact hz p q (Or.inr ⟨hq0, hq1⟩)
  rw [Finset.sum_congr rfl (fun p _ => hFin p), Finset.sum_add_distrib]
  have h1 : ∑ p : Fin n, f p i0 = f i0 i0 + f i1 i0 :=
    sum_restrict_pair i0 i1 hne (fun p => f p i0) (fun p hp0 hp1 => hz p i0 (Or.inl ⟨hp0, hp1⟩))
  have h2 : ∑ p : Fin n, f p i1 = f i0 i1 + f i1 i1 :=
    sum_restrict_pair i0 i1 hne (fun p => f p i1) (fun p hp0 hp1 => hz p i1 (Or.inl ⟨hp0, hp1⟩))
  rw [h1, h2]

What this page does not claim

The lemma does not assert that the deformed metric is non-flat; that is a separate theorem. The lemma does not depend on the values of the function on the pair, only on its vanishing outside the pair. The lemma is not specific to Recognition Science; it is a general fact about finite sums.

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: