Foundation Cost Projector Golden Rank One End Normalized Is Projector

The algebraic step

In linear algebra, a projector is a linear map that is its own square: applying it twice gives the same result as applying it once. The declaration rankOneEnd_normalized_isProjector proves a precise condition under which a very simple linear map becomes a projector. The map in question sends every vector x to a fixed vector v scaled by the value of a linear functional ℓ at x: x ↦ ℓ(x)v. Such a map is called rank-one because its image is at most one-dimensional.

The theorem states that if the scalar ℓ(v) is nonzero, then this rank-one map, after being divided by that scalar, is a projector. In symbols: if A(x) = ℓ(x)v and ℓ(v) ≠ 0, then (A/ℓ(v))² = A/ℓ(v). This is a purely algebraic fact, proved for endomorphisms over the real numbers. It does not depend on any geometric structure, any notion of distance, or any particular choice of coordinates. The proof is a short computation: the square of the rank-one map is ℓ(v) times itself, so dividing by ℓ(v) yields the projector equation.

In Recognition Science, the framework that studies what cost functions are forced by basic consistency conditions, this algebraic step plays a specific role. The framework's library of machine-checked theorems builds a chain of results from a forced cost function to the golden ratio φ. The rank-one map here is the algebraic shape of a projector that arises from the Hessian of that cost function. The theorem in question is the link that takes a rank-one map, normalizes it, and shows it is a projector. From there, a further theorem shows that any projector induces an operator G = φP + (1 − φ)(I − P) that satisfies G² = G + I, the characteristic equation of the golden ratio.

What this declaration does not claim is just as important. It does not prove that any particular cost function produces a rank-one map of this form. It does not prove that the golden ratio appears in physics. It does not even prove that the golden operator equation has a unique solution in general. The theorem is deliberately narrow: it is the algebraic core, not a full geometric or physical statement. The framework's broader claims about why φ appears rest on other theorems and on empirical comparisons, not on this single algebraic fact.

/-- A nondegenerate rank-one endomorphism normalizes to a projector. -/
theorem rankOneEnd_normalized_isProjector
    (ell : V →ₗ[ℝ] ℝ) (v : V) (hμ : ell v ≠ 0) :
    IsProjector (normalizedProjector (ell v) (rankOneEnd ell v)) :=
  normalizedProjector_isProjector (rankOneEnd_square ell v) hμ

/-- A projector induces a golden operator: `G² = G + I`. -/
theorem goldenOperator_sq {P : Module.End ℝ V} (hP : IsProjector P) :
    goldenOperator P * goldenOperator P = goldenOperator P + 1 := by
  ext v
  have hPv : P (P v) = P v := by
    have h := congrArg (fun Q : Module.End ℝ V => Q v) hP
    simpa [IsProjector] using h
  have hphi : Constants.phi ^ 2 = Constants.phi + 1 := Constants.phi_sq_eq
  have hphi_compl :
      1 - Constants.phi * 2 + Constants.phi ^ 2 = 2 - Constants.phi := by
    rw [hphi]
    ring
  have hphi_mul : Constants.phi * Constants.phi = Constants.phi + 1 := by
    simpa [pow_two] using hphi
  have hphi_compl_mul :
      (1 + -Constants.phi) * (1 + -Constants.phi) = 2 - Constants.phi := by
    nlinarith [hphi_compl]
  simp [goldenOperator, sub_eq_add_neg, map_add, map_smul, smul_smul, hPv]
  rw [hphi_mul, hphi_compl_mul]
  module

/-- A nondegenerate rank-one endomorphism normalizes to a projector. -/
theorem rankOneEnd_normalized_isProjector
    (ell : V →ₗ[ℝ] ℝ) (v : V) (hμ : ell v ≠ 0) :
    IsProjector (normalizedProjector (ell v) (rankOneEnd ell v)) :=
  normalizedProjector_isProjector (rankOneEnd_square ell v) hμ

What this page does not claim

This theorem does not prove that any specific cost function yields a rank-one map. This theorem does not establish that the golden ratio appears in any physical measurement. This theorem does not show that the golden operator equation has a unique solution without additional assumptions.

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/Foundation/CostProjectorGolden.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: