Cost Ndim Block Reduction Mu Dinv Two Sparse

The two-coordinate collapse

In mathematics, a sum over many terms often simplifies when most of those terms are zero. The theorem called mu_Dinv_twoSparse states one such simplification precisely. It concerns a vector α in n-dimensional space that is supported on just two coordinates, meaning every entry of α outside those two positions is zero. The theorem says that a particular scalar quantity, built from α and from a diagonal metric, reduces to a sum over exactly those two coordinates. No approximation is involved: the equality holds for every ambient dimension n, from 2 upward.

The scalar quantity in question comes from the Recognition Science framework's projector construction. In that framework, a ledger (a discrete record of events) carries a cost, and the framework derives geometric objects from that cost. One such object is a projector, a linear map that selects a subspace. The theorem computes a scalar μ that appears inside the projector's definition. The metric used here is diagonal, with entries that are reciprocals of hyperbolic cosines of the coordinates. For a two-sparse α, the theorem shows that μ equals λ times a weighted sum of the squares of the two nonzero components of α, with weights given by those reciprocal cosines.

The history of such reductions is classical. When a problem has symmetry, or when most variables vanish, a high-dimensional expression often collapses to a low-dimensional one. The novel content here is that the collapse is proved as an exact identity in a machine-checked library of formal theorems, not asserted as a numerical approximation. The theorem is a lemma: it feeds into a larger result that the n-dimensional projector, on a slice where one coordinate is fixed at zero, obeys exactly the same scalar law as the 2-dimensional case. That larger result is the block-reduction identity, which the framework uses to lift a 2D non-parallelism statement to arbitrary dimension.

What the theorem does not claim is just as important. It does not say that the full n-dimensional projector equals the 2D projector as an operator; it only equates one matrix entry, the (i0, i0) component, under the stated conditions. It does not require the other n minus 2 coordinates to be at equilibrium or zero; they may be arbitrary, as long as the i1 coordinate is zero. It does not assert anything about the derivative or non-parallelism by itself; that is the job of the subsequent theorem PApply_not_parallel_gen. And it does not apply to vectors supported on more than two coordinates, or to non-diagonal metrics. The theorem is narrow, and its power comes from that narrowness being exactly what the larger proof needs.

/-- The scalar `μ_λ` of `Projector.lean`, specialized to `hInv = Dinv t` and a
2-sparse `α`, collapses to the two-term closed form. -/
theorem mu_Dinv_twoSparse {n : ℕ} (t : Vec n) (α : Vec n) (lam : ℝ)
    (i0 i1 : Fin n) (hne : i0 ≠ i1) (h2 : TwoSparse α i0 i1) :
    mu lam (Dinv t) α =
      lam * ((Real.cosh (t i0))⁻¹ * α i0 ^ 2 + (Real.cosh (t i1))⁻¹ * α i1 ^ 2) := by
  unfold mu
  have hpt : ∀ i : Fin n, α i * sharp (Dinv t) α i = (Real.cosh (t i))⁻¹ * α i ^ 2 := by
    intro i
    rw [sharp_Dinv_apply]
    ring
  have hdot : dot α (sharp (Dinv t) α) = ∑ i : Fin n, (Real.cosh (t i))⁻¹ * α i ^ 2 := by
    unfold dot
    exact Finset.sum_congr rfl (fun i _ => hpt i)
  rw [hdot, sum_twoSparse α i0 i1 hne h2 (fun i => (Real.cosh (t i))⁻¹)]

/-- The scalar `μ_λ` of `Projector.lean`, specialized to `hInv = Dinv t` and a
2-sparse `α`, collapses to the two-term closed form. -/
theorem mu_Dinv_twoSparse {n : ℕ} (t : Vec n) (α : Vec n) (lam : ℝ)
    (i0 i1 : Fin n) (hne : i0 ≠ i1) (h2 : TwoSparse α i0 i1) :
    mu lam (Dinv t) α =
      lam * ((Real.cosh (t i0))⁻¹ * α i0 ^ 2 + (Real.cosh (t i1))⁻¹ * α i1 ^ 2) := by
  unfold mu
  have hpt : ∀ i : Fin n, α i * sharp (Dinv t) α i = (Real.cosh (t i))⁻¹ * α i ^ 2 := by
    intro i
    rw [sharp_Dinv_apply]
    ring
  have hdot : dot α (sharp (Dinv t) α) = ∑ i : Fin n, (Real.cosh (t i))⁻¹ * α i ^ 2 := by
    unfold dot
    exact Finset.sum_congr rfl (fun i _ => hpt i)
  rw [hdot, sum_twoSparse α i0 i1 hne h2 (fun i => (Real.cosh (t i))⁻¹)]

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

What this page does not claim

The full n-dimensional projector equals the 2D projector as an operator, only one matrix entry is equated. The other n minus 2 coordinates must be at equilibrium or zero, they may be arbitrary. The theorem itself proves non-parallelism or any derivative statement, that is the later theorem PApply_not_parallel_gen.

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: