Encyclopedia Cost Cost Ndim Block Reduction

ARTICLE 3 claims 3 theorems

Cost Ndim Block Reduction

A 2-dimensional calculation in Recognition Science holds exactly in every higher dimension, a theorem that keeps the framework's core result intact.

Verify this page

Block reduction in any dimension

In Recognition Science, a ledger, a discrete record of events, assigns a cost to each possible state. The framework's central object is a projector built from that cost, a mathematical operator that picks out the states the ledger recognizes. A key early result, Theorem 1a, showed that in a 2-dimensional space this projector is never parallel to a certain flat connection, meaning the recognition structure is genuinely curved. The question was whether that result depended on the space having exactly two dimensions.

The module called BlockReduction answers that question. It proves that the 2-dimensional calculation is not a special case but a block that sits inside any higher-dimensional space. The setup: take a vector α that is nonzero on only two coordinates, say i0 and i1, and zero everywhere else. This is called 2-sparse. Embed that vector in an n-dimensional space, build the full n×n projector from it, and look at the (i0, i0) entry of that projector. The theorem states that this entry is exactly equal to the 2-dimensional closed form, provided the other coordinate t i1 is zero.

The reduction is algebraic, not numerical. The general n-dimensional sum defining the projector collapses because every term outside the two support coordinates vanishes. The theorem PApply_e_eq_P00Gen states this equality as a theorem: the n-dimensional object is the 2D form on this slice, for every n, not merely isomorphic to it or expected to reduce to it. The derivative of that entry then obeys the same scalar law as in 2D, and it is never zero. So the projector fails to be parallel along the i0 direction at every point of the slice, for every ambient dimension n ≥ 2.

In Recognition Science, this means the framework's core geometric fact is dimension-independent. A 2-sparse structure embedded in a 100-dimensional recognition space behaves exactly as it does in 2 dimensions, at least along the slice where one coordinate is fixed at zero. The other n−2 coordinates can be anything; they do not need to be at equilibrium. This is the block-diagonal architecture the review panel identified: the n-dimensional object provably is the 2D closed form on this slice, algebraically, for every n.

What this changes is the scope of the framework's claims. A result proved in 2 dimensions is not confined to 2 dimensions. The same scalar law, the same non-parallelism, the same curvature signature holds in any ambient space. The framework's recognition structure is not an artifact of low dimension; it is a property that persists when the space grows.

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

What this page does not claim

The module does not prove that the full n-dimensional projector is block-diagonal, only that its (i0, i0) entry reduces to the 2D form. The result requires α to be 2-sparse and t i1 = 0; it does not cover general vectors or arbitrary backgrounds. The physical recognition-to-linking bridge in three dimensions is not established here; this is a topological theorem about the projector.

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