Encyclopedia Cost Cost Ndim Block Reduction Two Sparse

ARTICLE 4 claims 3 theorems 1 model

Cost Ndim Block Reduction Two Sparse

A vector that touches only two coordinates lets a high-dimensional calculation collapse exactly into a two-dimensional one, with no approximation.

Verify this page

The two-coordinate slice

In linear algebra, a vector is called sparse when most of its entries are zero. The declaration TwoSparse names the simplest nontrivial case: a vector in any dimension that has nonzero entries in at most two positions, and zeros everywhere else. Think of a spreadsheet with a thousand columns where only two cells contain numbers; every other column contributes nothing to sums that multiply by this vector. The definition is deliberately plain: for two chosen indices i0 and i1, every other coordinate of the vector must equal zero.

Why care about such a restricted object? Because it turns a potentially enormous calculation into a small one. When a formula sums over all n coordinates of a vector, a TwoSparse vector makes every term outside the two chosen positions vanish. The sum collapses from n terms to exactly two. This is not an approximation or a numerical shortcut; it is an algebraic identity that holds for every dimension n. The theorem sum_twoSparse states this collapse formally: a weighted sum over the vector equals the sum over just its two nonzero coordinates.

The collapse matters in Recognition Science, the framework that derives physical structure from a forced cost of recognition. The framework builds a mathematical object called a projector, a matrix that encodes how a recognition space responds to a perturbation. In full generality the projector is an n-dimensional object with n-squared entries. The framework's library proves a block-reduction identity: when the perturbation vector is TwoSparse, the (i0, i0) entry of the full n-dimensional projector equals exactly the closed two-dimensional formula from the framework's scalar certificates. The theorem PApply_e_eq_P00Gen states this equality of real numbers, computed from the genuinely n-dimensional definitions, for every ambient dimension n, given that the background coordinate t i1 is zero and the perturbation coefficients are nonzero.

This reduction is not merely a curiosity. It transports a previously proved two-dimensional result to arbitrary dimension. The framework had already shown that in two dimensions the projector is not parallel to a certain flat connection; its derivative is never zero. The general-n theorem PApply_not_parallel_gen lifts that fact: on the two-coordinate slice, the n-dimensional projector fails to be parallel along the i0 direction at every point of the slice, for every n at least 2. The high-dimensional object provably obeys the same scalar law as the two-dimensional one. That is the architectural payoff: a result proved in the simplest case becomes a result about every dimension, with no new computation.

What TwoSparse does not claim is equally precise. It does not assert that every projector reduces to two dimensions, only those built from a two-coordinate perturbation. It does not claim anything about the other n minus 2 coordinates of the background; they may be arbitrary and fixed, and the identity still holds. And it does not claim that the full n-by-n projector matrix equals the two-dimensional one, only that a single entry, the (i0, i0) component, matches the closed form. The reduction is a slice statement, not a global equivalence. Within that slice, however, the equality is exact and algebraic, not asymptotic or approximate.

MODEL TwoSparse · IndisputableMonolith/Cost/Ndim/BlockReduction.lean
TwoSparse · IndisputableMonolith/Cost/Ndim/BlockReduction.lean:68 
/-- `α` is supported on (at most) the two indices `i0, i1`: every other coordinate of
`α` vanishes. This is the general-`n` analogue of "`α = (a, b)` with no other
components", i.e. of the 2D setup of `ScalarCertificates.lean`. -/
def TwoSparse {n : ℕ} (α : Vec n) (i0 i1 : Fin n) : Prop :=
  ∀ k : Fin n, k ≠ i0 → k ≠ i1 → α k = 0
THEOREM sum_twoSparse · IndisputableMonolith/Cost/Ndim/BlockReduction.lean
sum_twoSparse · IndisputableMonolith/Cost/Ndim/BlockReduction.lean:102 
/-- A sum `∑ᵢ f i · αᵢ²` over a 2-sparse `α` (supported on `{i0, i1}`, `i0 ≠ i1`)
collapses to the two-term sum over `{i0, i1}`. The general-`n` mechanism that makes
every closed-form 2D scalar identity valid at arbitrary ambient dimension. -/
theorem sum_twoSparse {n : ℕ} (α : Vec n) (i0 i1 : Fin n) (hne : i0 ≠ i1)
    (h2 : TwoSparse α i0 i1) (f : Fin n → ℝ) :
    ∑ i : Fin n, f i * α i ^ 2 = f i0 * α i0 ^ 2 + f i1 * α i1 ^ 2 := by
  have hsub : ({i0, i1} : Finset (Fin n)) ⊆ Finset.univ := Finset.subset_univ _
  have hzero : ∀ x ∈ (Finset.univ : Finset (Fin n)),
      x ∉ ({i0, i1} : Finset (Fin n)) → f x * α x ^ 2 = 0 := by
    intro x _ hx
    simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hx
    rw [h2 x hx.1 hx.2]
    ring
  rw [← Finset.sum_subset hsub hzero, Finset.sum_pair hne]
THEOREM PApply_e_eq_P00Gen · IndisputableMonolith/Cost/Ndim/BlockReduction.lean
PApply_e_eq_P00Gen · IndisputableMonolith/Cost/Ndim/BlockReduction.lean:133 
/-- **The block-reduction identity.** For any ambient dimension `n`, any `α` supported
on two indices `i0 ≠ i1` with `α i0 ≠ 0`, any `λ ≠ 0`, and any background `t` with
`t i1 = 0`, the `(i0, i0)` entry of the abstract, `n`-dimensional projector `P_λ =
PApply lam (Dinv t) α` — applied to the indicator direction `e i0` — equals exactly the
2D closed form `P00Gen (α i0) (α i1) (t i0)` of `ScalarCertificates.lean`. This is the
algebraic content behind "the `n`-dimensional projector reduces to the 2D one on the
2-sparse slice": no approximation, no isomorphism-up-to-relabeling, an equality of
real numbers computed from the genuinely `n`-dimensional definitions. -/
theorem PApply_e_eq_P00Gen {n : ℕ} (t : Vec n) (α : Vec n) (lam : ℝ)
    (i0 i1 : Fin n) (hne : i0 ≠ i1) (h2 : TwoSparse α i0 i1)
    (ha : α i0 ≠ 0) (hlam : lam ≠ 0) (ht1 : t i1 = 0) :
    PApply lam (Dinv t) α (e i0) i0 = P00Gen (α i0) (α i1) (t i0) := by
  have hc : (0 : ℝ) < Real.cosh (t i0) := Real.cosh_pos _
  have hc' : Real.cosh (t i0) ≠ 0 := ne_of_gt hc
  have ha2 : (0 : ℝ) < α i0 ^ 2 := sq_pos_of_ne_zero ha
  have hAA : AApply lam (Dinv t) α (e i0) i0
      = lam * ((Real.cosh (t i0))⁻¹ * α i0) * α i0 := by
    show lam * sharp (Dinv t) α i0 * dot α (e i0) = _
    rw [sharp_Dinv_apply, dot_e]
  have hmu : mu lam (Dinv t) α
      = lam * ((Real.cosh (t i0))⁻¹ * α i0 ^ 2 + α i1 ^ 2) := by
    rw [mu_Dinv_twoSparse t α lam i0 i1 hne h2, ht1, Real.cosh_zero]
    norm_num
  have hmu_pos_part : (0 : ℝ) < (Real.cosh (t i0))⁻¹ * α i0 ^ 2 + α i1 ^ 2 := by
    have h1 : (0 : ℝ) < (Real.cosh (t i0))⁻¹ * α i0 ^ 2 := mul_pos (inv_pos.mpr hc) ha2
    nlinarith [sq_nonneg (α i1)]
  have hdenom_pos : (0 : ℝ) < α i0 ^ 2 + α i1 ^ 2 * Real.cosh (t i0) := by
    nlinarith [sq_nonneg (α i1), mul_nonneg (sq_nonneg (α i1)) (le_of_lt hc)]
  have hPapply : PApply lam (Dinv t) α (e i0) i0
      = (mu lam (Dinv t) α)⁻¹ * AApply lam (Dinv t) α (e i0) i0 := by
    show (mu lam (Dinv t) α)⁻¹ • AApply lam (Dinv t) α (e i0) i0 = _
    rw [smul_eq_mul]
  rw [hPapply, hAA, hmu]
  unfold P00Gen
  rw [eq_div_iff (ne_of_gt hdenom_pos)]
  field_simp
THEOREM PApply_not_parallel_gen · IndisputableMonolith/Cost/Ndim/BlockReduction.lean
PApply_not_parallel_gen · IndisputableMonolith/Cost/Ndim/BlockReduction.lean:170 
/-- **Theorem 1a, arbitrary ambient dimension `n`** (panel-greenlit general-`n`
extension). Embed a 2-sparse `α = (…, α i0, …, α i1, …, 0, …)` supported on indices
`i0 ≠ i1` inside an `n`-dimensional recognition space, and consider the slice `t` with
`t i1 = 0` (all other `n - 2` coordinates arbitrary and fixed). As the `i0`-th
coordinate varies, the `(i0, i0)` entry of the genuinely `n`-dimensional projector
`P_λ` obeys *exactly* the 2D scalar law `dP00Gen`, and — for `α i0 ≠ 0`, `α i1 ≠ 0` —
that derivative is never zero. Hence `P_λ` fails to be `D`-parallel along the `i0`
direction at every point of the slice, for every ambient dimension `n ≥ 2`, not just
`n = 2`. This is the direct general-`n` lift of `ScalarCertificates.dP00Gen_ne_zero`. -/
theorem PApply_not_parallel_gen {n : ℕ} (t : Vec n) (α : Vec n) (lam : ℝ)
    (i0 i1 : Fin n) (hne : i0 ≠ i1) (h2 : TwoSparse α i0 i1)
    (ha : α i0 ≠ 0) (hb : α i1 ≠ 0) (hlam : lam ≠ 0) (ht1 : t i1 = 0) (s : ℝ) :
    HasDerivAt (fun s' => PApply lam (Dinv (Function.update t i0 s')) α (e i0) i0)
        (dP00Gen (α i0) (α i1) s) s
      ∧ (s ≠ 0 → dP00Gen (α i0) (α i1) s ≠ 0) := by
  have hfun_eq : (fun s' => PApply lam (Dinv (Function.update t i0 s')) α (e i0) i0)
      = P00Gen (α i0) (α i1) := by
    funext s'
    have ht1' : Function.update t i0 s' i1 = 0 := by
      rw [Function.update_of_ne (Ne.symm hne)]
      exact ht1
    have hred := PApply_e_eq_P00Gen (Function.update t i0 s') α lam i0 i1 hne h2 ha hlam ht1'
    rwa [Function.update_self] at hred
  refine ⟨?_, fun hs => dP00Gen_ne_zero (α i0) (α i1) s ha hb hs⟩
  rw [hfun_eq]
  exact hasDerivAt_P00Gen (α i0) (α i1) s ha

What this page does not claim

Not every projector reduces to two dimensions, only those built from a two-coordinate perturbation. The full n-by-n projector matrix does not equal the two-dimensional one; only one entry matches the closed form. The other n minus 2 background coordinates need not be zero for the identity to hold.

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/BlockReduction.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