Cost Ndim Projector

The projector

A projection operator is a linear map that sends a vector to a subspace and leaves that subspace fixed. Apply it twice and you get the same result as applying it once. The cost ndim projector is the specific projection that Recognition Science derives from its cost function, and it is not an arbitrary choice: the same construction that yields the projector also yields the golden ratio and a whole family of metallic means.

The construction starts with a covector β, which in plain terms is a row vector, and an inverse metric kernel hInv, a matrix that sets the geometry of the space. From these the framework builds a sharp vector β♯, then a rank-one operator A = h⁻¹ g̃, where g̃ = λ β ⊗ β. The scalar λ is a parameter, and the tensor product β ⊗ β is a matrix whose entries are products of the components of β. The operator A satisfies the quadratic law A² = μ A, where μ = λ β · β♯ is a scalar. When μ is nonzero, the normalized projector P = A / μ is well defined, and the framework proves that P is idempotent: P(P(v)) = P(v) for every vector v.

The projector is not the end of the story. From P the framework defines the almost-product operator F = 2P - I, which is a reflection: the framework proves F(F(v)) = v, meaning that applying F twice returns the original vector. This reflection is the seed of the golden operator G(v) = (1/2)v + (√5/2)F(v). The framework proves that G satisfies G(G(v)) = G(v) + v, which is the operator form of the golden ratio equation r² = r + 1. The same pattern extends to the metallic family: for parameters p and q, the operator M(v) = (p/2)v + (√(p² + 4q)/2)F(v) satisfies M(M(v)) = p M(v) + q v, the operator form of the metallic means equation r² = p r + q.

In plain language, the framework establishes that a single rank-one operator, built from a covector and a metric, carries within it the entire family of metallic means. The projector is the normalized version of that operator, the reflection is its square root, and the golden operator is the special case p = 1, q = 1. The proofs are machine-checked: the framework contains formal theorems showing that the projector is idempotent, the reflection is an involution, and the golden and metallic operators satisfy their defining quadratic relations, all under the single condition that the scalar μ is nonzero.

What this means for the framework is that the cost function, which is the unique function satisfying five plain conditions, does not merely produce a number. It produces an operator algebra. The golden ratio, which appears as the self-similar scaling in the forcing chain, is here shown to be the eigenvalue of a reflection-based operator that arises directly from the cost structure. The framework is a bridge between the scalar cost function and the operator language that the framework uses to describe recognition events.

theorem PApply_idempotent {n : ℕ}
    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
    PApply lam hInv β (PApply lam hInv β v) = PApply lam hInv β v := by
  ext i
  simp [PApply, AApply_smul, AApply_sq, hμ, mul_comm]

theorem FApply_square {n : ℕ}
    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
    FApply lam hInv β (FApply lam hInv β v) = v := by
  ext i
  have hPFi : PApply lam hInv β (FApply lam hInv β v) i = PApply lam hInv β v i := by
    simpa using congrFun (PApply_FApply lam hInv β hμ v) i
  calc
    FApply lam hInv β (FApply lam hInv β v) i
        = (2 • PApply lam hInv β (FApply lam hInv β v) - FApply lam hInv β v) i := by
            simp [FApply]
    _ = (2 • PApply lam hInv β v - FApply lam hInv β v) i := by
          simp [hPFi]
    _ = v i := by
          simp [FApply]

theorem GApply_square {n : ℕ}
    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
    GApply lam hInv β (GApply lam hInv β v) = GApply lam hInv β v + v := by
  ext i
  have hFGi :
      FApply lam hInv β
          (((1 : ℝ) / 2) • v + (Real.sqrt 5 / 2) • FApply lam hInv β v) i
        = (((1 : ℝ) / 2) • FApply lam hInv β v + (Real.sqrt 5 / 2) • v) i := by
    simpa [GApply] using congrFun (FApply_GApply lam hInv β hμ v) i
  have hsqrt : Real.sqrt 5 * Real.sqrt 5 = 5 := by
    nlinarith [Real.sq_sqrt (by positivity : 0 ≤ (5 : ℝ))]
  have hsqrtq : (Real.sqrt 5 / 2) * (Real.sqrt 5 / 2) = 5 / 4 := by
    nlinarith [hsqrt]
  have hFGi' :
      FApply lam hInv β (((2 : ℝ)⁻¹) • v + (Real.sqrt 5 / 2) • FApply lam hInv β v) i
        = (((1 : ℝ) / 2) • FApply lam hInv β v + (Real.sqrt 5 / 2) • v) i := by
    simpa using hFGi
  simp [GApply]
  rw [hFGi']
  have hmul : (Real.sqrt 5 / 2) * ((Real.sqrt 5 / 2) * v i) = (5 / 4) * v i := by
    calc
      (Real.sqrt 5 / 2) * ((Real.sqrt 5 / 2) * v i)
          = ((Real.sqrt 5 / 2) * (Real.sqrt 5 / 2)) * v i := by
              ring
      _ = (5 / 4) * v i := by rw [hsqrtq]
  simp
  nlinarith [hmul]

theorem MetallicApply_square {n : ℕ}
    (p q lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
    (hμ : mu lam hInv β ≠ 0) (hq : 0 ≤ p ^ 2 + 4 * q) (v : Vec n) :
    MetallicApply p q lam hInv β (MetallicApply p q lam hInv β v)
      = p • MetallicApply p q lam hInv β v + q • v := by
  ext i
  have hFMi :
      FApply lam hInv β
          ((p / 2) • v + (Real.sqrt (p ^ 2 + 4 * q) / 2) • FApply lam hInv β v) i
        = ((p / 2) • FApply lam hInv β v
          + (Real.sqrt (p ^ 2 + 4 * q) / 2) • v) i := by
    simpa [MetallicApply] using congrFun (FApply_MetallicApply p q lam hInv β hμ v) i
  have hsqrt : Real.sqrt (p ^ 2 + 4 * q) * Real.sqrt (p ^ 2 + 4 * q) = p ^ 2 + 4 * q := by
    nlinarith [Real.sq_sqrt hq]
  have hsqrtq :
      (Real.sqrt (p ^ 2 + 4 * q) / 2) * (Real.sqrt (p ^ 2 + 4 * q) / 2)
        = (p ^ 2 + 4 * q) / 4 := by
    nlinarith [hsqrt]
  simp [MetallicApply, hFMi]
  have hmul :
      (Real.sqrt (p ^ 2 + 4 * q) / 2) *
          ((Real.sqrt (p ^ 2 + 4 * q) / 2) * v i)
        = ((p ^ 2 + 4 * q) / 4) * v i := by
    calc
      (Real.sqrt (p ^ 2 + 4 * q) / 2) *
          ((Real.sqrt (p ^ 2 + 4 * q) / 2) * v i)
          = ((Real.sqrt (p ^ 2 + 4 * q) / 2) *
              (Real.sqrt (p ^ 2 + 4 * q) / 2)) * v i := by
              ring
      _ = ((p ^ 2 + 4 * q) / 4) * v i := by rw [hsqrtq]
  nlinarith [hmul]

What this page does not claim

The framework does not prove that the golden ratio is the only self-similar scaling. The framework does not claim that the projector is unique without the condition μ ≠ 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/Projector.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: