Cost Ndim Projector Metallic Apply Square

The metallic operator law

A linear operator is a rule that sends vectors to vectors while respecting addition and scaling. The classical metallic means, such as the golden ratio φ ≈ 1.618 and the silver ratio 1 + √2 ≈ 2.414, are the positive solutions of quadratic equations of the form x² = p x + q. The Recognition Science declaration MetallicApply_square shows that a whole family of operators, built from a rank-one projection, obeys exactly this same quadratic law, with the numbers p and q appearing as coefficients.

The construction starts with a covector β, which is a linear map from vectors to scalars, and an inverse metric kernel hInv, which is a symmetric array of numbers used to raise indices. From these one forms a rank-one operator A, whose action on any vector v is a scalar multiple of a fixed sharp vector β♯. The scalar is λ times the dot product of β with v. The operator A satisfies the simple quadratic relation A² = μ A, where μ is the scalar λ times the dot product of β with its sharp. When μ is nonzero, one can normalize A to obtain a true projector P, meaning P² = P, and from P one defines the almost-product operator F = 2P - I, which satisfies F² = I, the identity.

From F, the framework defines the metallic operator as MetallicApply(p, q) v = (p/2) v + (√(p² + 4q)/2) F v. The theorem MetallicApply_square proves, under the condition that the square root is real, that applying this operator twice gives the same result as p times the operator applied once plus q times the original vector: MetallicApply² v = p · MetallicApply v + q · v. This is precisely the metallic mean equation, now holding for operators rather than numbers. The golden operator is the special case p = 1, q = 1, and the theorem GApply_square proves the corresponding law G² = G + I for that case.

In Recognition Science, this operator algebra is packaged as the finite-dimensional machinery behind the rank-one tensor picture. The declaration itself is a proved theorem in the framework's machine-checked library of formal theorems. It establishes a structural fact about a family of operators defined from a projector: they all share the same quadratic recurrence that defines the metallic means. What it does not claim is that these operators are the only ones satisfying such a law, nor does it claim that the metallic means themselves are derived from first principles here. The theorem takes p and q as given parameters and shows the consequence for the operator built from them.

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]

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]

What this page does not claim

The theorem does not claim that the metallic means themselves are derived from the cost function's forcing chain. It does not claim that the operator family is unique or that no other operators satisfy the same quadratic law. It does not claim any numerical values for p and q beyond the golden case p = 1, q = 1.

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: