Encyclopedia Cost Cost Ndim Block Reduction Papply Not Parallel Gen

ARTICLE 4 claims 4 theorems

Cost Ndim Block Reduction Papply Not Parallel Gen

A machine-checked proof shows that a high-dimensional recognition projector, on a specially chosen slice, obeys exactly the same non-flatness law as its two-dimensional counterpart.

Verify this page

The block reduction

In differential geometry, a projector is a linear map that sends vectors onto a subspace. The Recognition Science framework builds a projector from a metric and a covector, and one of its central questions is whether that projector is flat, meaning whether it stays parallel as you move along a direction. The declaration PApply_not_parallel_gen answers that question for a general ambient dimension n, not just for the two-dimensional case that was proved earlier.

The setup is this. Take a vector α that is supported on only two coordinates, i0 and i1, so all other entries are zero. The projector is built from the inverse of a diagonal metric D, where D is the Hessian of a sum of cosh terms. The theorem evaluates the projector at the indicator direction e i0, which extracts the (i0, i0) matrix entry. The key condition is that the background coordinate t i1 is set to zero, while all other n minus 2 coordinates are arbitrary and fixed.

Under those conditions, the theorem proves an exact algebraic reduction: the n-dimensional projector entry equals the closed two-dimensional form P00Gen, evaluated at the two nonzero α components and the coordinate t i0. This is not an approximation and not an isomorphism up to relabeling. It is an equality of real numbers computed from the genuinely n-dimensional definitions. The proof works because every term in the defining sum that involves a coordinate outside {i0, i1} vanishes, since α is zero there.

From that reduction, the theorem derives the derivative law. As the i0-th coordinate varies, the projector entry obeys exactly the same scalar derivative dP00Gen as in the 2D case. For α i0 and α i1 both nonzero, that derivative is never zero. Therefore the projector fails to be D-parallel along the i0 direction at every point of the slice, for every ambient dimension n ≥ 2. The machine-checked library of formal theorems proves this for all n at once, not case by case.

The consequence is that the non-flatness phenomenon is not an artifact of low dimension. A recognition space of any size, when it contains a two-sparse structure, exhibits the same failure of parallelism along that direction. The theorem does not claim that the reduction holds for arbitrary α, nor that the derivative is nonzero when either α component is zero, nor that the physical recognition-to-linking bridge is closed. It establishes a precise algebraic fact about the projector on a specific slice.

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
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
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 reduction holds for arbitrary α, not just 2-sparse vectors. The derivative is nonzero when either α i0 or α i1 is zero. The physical recognition-to-linking bridge is closed by this theorem.

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