Encyclopedia Cost Cost Ndim Projector Fapply Square

ARTICLE 3 claims 3 theorems

Cost Ndim Projector Fapply Square

A linear map that squares to the identity acts like a mirror: apply it twice and you are back where you started.

Verify this page

The reflection operator

In linear algebra, an operator that squares to the identity is called an involution. Applying it twice returns the original vector: F(F(v)) = v. The theorem FApply_square proves that a specific operator built from a cost function has exactly this property, provided a scalar coefficient is nonzero. This operator, written F, is defined as F = 2P - I, where P is a projector and I is the identity. The theorem states that FApply(FApply(v)) = v for every vector v in the space.

The construction starts with a covector β and an inverse metric kernel hInv. These determine a rank-one operator A, whose square is a scalar multiple of itself: A² = μA. When μ is nonzero, the normalized projector P = A/μ is well-defined and idempotent, meaning P(P(v)) = P(v). The operator F = 2P - I then inherits the involution property from P's idempotence. The proof of FApply_square in the machine-checked library of formal theorems verifies this algebra step by step, using the definitions of P and A and the quadratic law for A.

This involution is the algebraic heart of the golden and metallic operators defined in the same module. The golden operator G = (1/2)I + (√5/2)F satisfies G² = G + I, a quadratic whose positive root is the golden ratio φ = (1 + √5)/2 ≈ 1.618. The metallic family MetallicApply(p, q) satisfies M² = pM + qI, generalizing the golden case to p = q = 1. These equations are not new physics; they are the standard recurrence relations for metallic means, now appearing as operator identities in a finite-dimensional setting.

The theorem does not claim that F is the only involution, nor that the golden ratio emerges uniquely from this construction. The scalar μ must be nonzero for the projector to exist; if μ = 0, the definitions collapse and the theorem does not apply. The result is purely algebraic: it says nothing about what the operator F means physically, only that it behaves like a reflection. The framework's broader claims about three spatial dimensions or the fine-structure constant are not part of this declaration.

THEOREM FApply_square · IndisputableMonolith/Cost/Ndim/Projector.lean
FApply_square · IndisputableMonolith/Cost/Ndim/Projector.lean:214 
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 · IndisputableMonolith/Cost/Ndim/Projector.lean
GApply_square · IndisputableMonolith/Cost/Ndim/Projector.lean:247 
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 · IndisputableMonolith/Cost/Ndim/Projector.lean
MetallicApply_square · IndisputableMonolith/Cost/Ndim/Projector.lean:276 
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 theorem does not claim that F is the only operator with the involution property. It does not derive the golden ratio as a unique consequence of the cost function alone. It does not make any physical claim about three spatial dimensions or the fine-structure constant.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND