Encyclopedia Cost Cost Ndim Block Reduction Papply E Eq P00 Gen

ARTICLE 4 claims 4 theorems

Cost Ndim Block Reduction Papply E Eq P00 Gen

A machine-checked theorem shows that a high-dimensional geometric object collapses, on a carefully chosen slice, to an exact two-dimensional formula.

Verify this page

The block reduction identity

The declaration PApply_e_eq_P00Gen is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns a projector, a mathematical operator that picks out a specific component of a vector. The projector here is built from an n-dimensional metric, a way of measuring distances and angles, which itself is constructed from a background vector t and a perturbation vector α.

The theorem's setting is deliberately narrow. The vector α is "2-sparse": it is supported on exactly two coordinates, i0 and i1, meaning all its other entries are zero. The background t has its i1-th coordinate fixed at zero. The theorem then evaluates the projector, applied to the indicator direction e i0, at the (i0, i0) entry. The result is an equality of real numbers: this n-dimensional object equals exactly the closed-form two-dimensional expression P00Gen (α i0) (α i1) (t i0). This is an algebraic identity, not a numerical approximation or an isomorphism up to relabeling.

The proof works because the sums defining the projector collapse. Since α is zero outside {i0, i1}, every term in the defining sums that involves another coordinate vanishes. The theorem's conditions are precise: i0 ≠ i1, α i0 ≠ 0, and the coupling constant λ ≠ 0. These are not optional; they are needed for the collapse to occur and for the result to be meaningful.

In Recognition Science, this reduction is the architectural bridge from two dimensions to arbitrary dimension. The framework's earlier work proved a non-parallelism result for a 2-dimensional slice. This theorem lifts that result to any ambient dimension n, provided the perturbation is 2-sparse. The consequence, proved in a companion theorem PApply_not_parallel_gen, is that the projector still fails to be parallel along the i0 direction, with the same scalar law governing its derivative. The high-dimensional object provably contains the two-dimensional behavior on this slice.

What the theorem does not claim is equally important. It does not assert that every projector in n dimensions reduces to a 2D form; the 2-sparse condition on α is essential. It does not say the reduction holds for arbitrary background t; the condition t i1 = 0 is required. It does not claim the projector is zero or trivial; rather, it shows a specific entry equals a specific nonzero 2D expression. The theorem is a precise, conditional statement about a particular component of a particular operator, not a sweeping statement about all of n-dimensional geometry.

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

The theorem does not claim that all n-dimensional projectors reduce to a 2D form. The theorem does not claim the reduction holds for arbitrary background vectors t. The theorem does not claim the projector entry is zero or trivial. The theorem does not claim the result holds without the conditions α i0 ≠ 0 and λ ≠ 0.

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