Foundation Cost Projector Golden Rank One End Square

The rank-one square law

A linear map is a rule that sends vectors to vectors while preserving addition and scaling. A rank-one linear map is the simplest nontrivial kind: it sends every vector to a multiple of a single fixed vector, with the multiple chosen by a fixed linear measurement. If the fixed vector is v and the measurement is ℓ, the map sends x to ℓ(x)·v. The theorem rankOneEnd_square states that applying this map twice equals applying it once, multiplied by the scalar ℓ(v). In symbols, if A is the rank-one map, then A² = ℓ(v)·A.

This fact is elementary and purely algebraic. It holds for any real vector space, any linear measurement ℓ, and any vector v. The proof in the machine-checked library of formal theorems is a short computation using the defining properties of linear maps. The theorem does not require the vector space to have finite dimension, does not require any metric or inner product, and does not involve the golden ratio or any other constant. It is a statement about the algebraic shape of rank-one maps and nothing more.

The significance appears in the next step. When ℓ(v) is nonzero, the map can be normalized: divide by ℓ(v) to get P = A/ℓ(v). The theorem rankOneEnd_square then implies P² = P, which is the defining property of a projector, a map that acts as the identity on its image and sends everything else to zero. From this projector, the framework constructs two further operators. The almost-product operator F = 2P − I satisfies F² = I, meaning it is an involution that flips the space between two complementary parts. The golden operator G = φP + (1−φ)(I−P), where φ is the golden ratio, satisfies G² = G + I, the same polynomial equation that φ itself satisfies.

In Recognition Science, this algebraic chain is the bridge from the cost geometry to the golden ratio. The framework's cost function produces a rank-one Hessian tensor, which supplies a rank-one map of exactly this shape. The theorem rankOneEnd_square is the algebraic core that lets the framework normalize that map into a projector, and then derive the golden-operator equation. The theorem itself, however, makes no claim about cost, geometry, or physics. It is a standalone result about linear algebra, deliberately isolated so the forcing chain can rest on a verified algebraic foundation.

What the theorem does not claim is equally precise. It does not claim that every rank-one map arises from a cost function, nor that every projector produces a golden operator with the specific constant φ. The golden-operator equation G² = G + I holds for the specific operator defined above; the theorem goldenScalar_forces_phi separately shows that a positive scalar satisfying x² = x + 1 must equal φ, but that is a different result. The rank-one square law is a lemma, not a physical law. Its role is to make the later steps rigorous, not to assert them.

/-- A rank-one endomorphism squares to a scalar multiple of itself:
`A² = ℓ(v) A`. -/
theorem rankOneEnd_square (ell : V →ₗ[ℝ] ℝ) (v : V) :
    rankOneEnd ell v * rankOneEnd ell v = ell v • rankOneEnd ell v := by
  ext x
  simp [rankOneEnd, smul_smul, mul_comm]

/-- 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 positive scalar satisfying the golden-operator characteristic equation is
forced to be the RS golden ratio. -/
theorem goldenScalar_forces_phi {lam : ℝ}
    (h_lam_pos : 0 < lam) (h_lam : lam ^ 2 = lam + 1) :
    lam = Constants.phi := by
  have h_lam_ne_one : lam ≠ 1 := by
    intro h1
    rw [h1] at h_lam
    norm_num at h_lam
  have hclosure : 1 + lam = lam ^ 2 := by
    linarith
  exact PhiForcingDerived.phi_forcing_complete lam h_lam_pos h_lam_ne_one hclosure

What this page does not claim

The theorem does not claim that every rank-one map arises from a cost function. The theorem does not claim that every projector produces a golden operator with the specific constant φ. The theorem does not involve the golden ratio or any physical constant directly.

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: