Foundation Cost Projector Golden Normalized Projector Golden Operator Sq

The golden operator

A projection is a linear map that, applied twice, gives the same result as applying it once. This declaration concerns a specific construction built from such a map, and it proves a clean algebraic fact about the result.

The construction starts with any linear map A whose square is a scalar multiple of itself, say A² = μA. If μ is not zero, dividing A by μ turns it into a true projection P, meaning P² = P. From that projection, the framework forms a new operator G = φP + (1 - φ)(I - P), where φ is the golden ratio, the number satisfying φ² = φ + 1, approximately 1.618. The declaration proves that this G always satisfies the same golden-ratio equation: G² = G + I. The operator inherits the defining polynomial of the golden ratio itself.

The proof is algebraic and does not depend on any particular space or dimension. It works for any real vector space V and any linear map on it. The library states the result as a theorem, verified with no gaps in its formal check. The construction also works for a rank-one map, one whose image is a single line, which is the shape that appears in the geometric route the framework follows.

What the declaration does not claim is just as important. It does not assert that any specific physical projector exists, nor that the golden ratio emerges from physics on its own. It proves a conditional statement: if a map squares to a scalar multiple of itself and that scalar is nonzero, then the normalized construction obeys the golden-ratio equation. The framework's broader claims about cost and recognition are separate theorems, not part of this declaration.

/-- Normalizing an operator with `A² = μA` and `μ ≠ 0` gives a golden
operator satisfying `G² = G + I`. -/
theorem normalizedProjector_goldenOperator_sq
    {μ : ℝ} {A : Module.End ℝ V}
    (hA : A * A = μ • A) (hμ : μ ≠ 0) :
    goldenOperator (normalizedProjector μ A) *
      goldenOperator (normalizedProjector μ A) =
        goldenOperator (normalizedProjector μ A) + 1 :=
  goldenOperator_sq (normalizedProjector_isProjector hA hμ)

/-- Normalizing an operator with `A² = μA` and `μ ≠ 0` gives a golden
operator satisfying `G² = G + I`. -/
theorem normalizedProjector_goldenOperator_sq
    {μ : ℝ} {A : Module.End ℝ V}
    (hA : A * A = μ • A) (hμ : μ ≠ 0) :
    goldenOperator (normalizedProjector μ A) *
      goldenOperator (normalizedProjector μ A) =
        goldenOperator (normalizedProjector μ A) + 1 :=
  goldenOperator_sq (normalizedProjector_isProjector hA hμ)

/-- Normalizing an operator with `A² = μA` and `μ ≠ 0` gives a golden
operator satisfying `G² = G + I`. -/
theorem normalizedProjector_goldenOperator_sq
    {μ : ℝ} {A : Module.End ℝ V}
    (hA : A * A = μ • A) (hμ : μ ≠ 0) :
    goldenOperator (normalizedProjector μ A) *
      goldenOperator (normalizedProjector μ A) =
        goldenOperator (normalizedProjector μ A) + 1 :=
  goldenOperator_sq (normalizedProjector_isProjector hA hμ)

What this page does not claim

The declaration does not prove that any specific physical projector exists. The declaration does not derive the golden ratio from physics on its own. The declaration does not establish the framework's broader cost or recognition theorems.

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: