IndisputableMonolith.Foundation.CostProjectorGolden

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Foundation.PhiForcingDerived
   4
   5/-!
   6# Projectors force golden operators
   7
   8The paper `Golden and Metallic Structures on Hessian Manifolds` uses the
   9rank-one Hessian tensor of reciprocal cost geometry to construct a normalized
  10projector `P`.  The theorem needed by the forcing stack is algebraic: once
  11`P² = P`, the almost-product operator `F = 2P - I` satisfies `F² = I`, and the
  12golden operator
  13
  14`G = φ P + (1 - φ)(I - P)`
  15
  16satisfies `G² = G + I`.
  17
  18This module proves that projector-to-golden step for endomorphisms over a real
  19module.  It is deliberately the algebraic core, not a full Hessian-manifold
  20formalization.
  21
  22Status: 0 sorry, 0 new axiom.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Foundation
  27namespace CostProjectorGolden
  28
  29variable {V : Type*} [AddCommGroup V] [Module ℝ V]
  30
  31/-- A projector endomorphism. -/
  32def IsProjector (P : Module.End ℝ V) : Prop :=
  33  P * P = P
  34
  35/-- The almost-product operator induced by a projector. -/
  36noncomputable def almostProduct (P : Module.End ℝ V) : Module.End ℝ V :=
  37  2 • P - 1
  38
  39/-- The golden operator induced by a projector. -/
  40noncomputable def goldenOperator (P : Module.End ℝ V) : Module.End ℝ V :=
  41  Constants.phi • P + (1 - Constants.phi) • (1 - P)
  42
  43/-- Normalize an operator satisfying `A² = μA` by its trace scalar `μ`. -/
  44noncomputable def normalizedProjector (μ : ℝ) (A : Module.End ℝ V) : Module.End ℝ V :=
  45  μ⁻¹ • A
  46
  47/-- Rank-one endomorphism `x ↦ ℓ(x) v`.  This is the algebraic shape of the
  48rank-one Hessian projector construction used by the golden-structure route. -/
  49noncomputable def rankOneEnd (ell : V →ₗ[ℝ] ℝ) (v : V) : Module.End ℝ V where
  50  toFun := fun x => ell x • v
  51  map_add' := by
  52    intro x y
  53    simp [map_add, add_smul]
  54  map_smul' := by
  55    intro a x
  56    simp [map_smul, smul_smul]
  57
  58/-- A rank-one endomorphism squares to a scalar multiple of itself:
  59`A² = ℓ(v) A`. -/
  60theorem rankOneEnd_square (ell : V →ₗ[ℝ] ℝ) (v : V) :
  61    rankOneEnd ell v * rankOneEnd ell v = ell v • rankOneEnd ell v := by
  62  ext x
  63  simp [rankOneEnd, smul_smul, mul_comm]
  64
  65/-- The algebraic projector step from the Hessian-geometry paper:
  66`A² = μA` and `μ ≠ 0` imply `P = μ⁻¹A` is a projector. -/
  67theorem normalizedProjector_isProjector
  68    {μ : ℝ} {A : Module.End ℝ V}
  69    (hA : A * A = μ • A) (hμ : μ ≠ 0) :
  70    IsProjector (normalizedProjector μ A) := by
  71  ext v
  72  have hAv : A (A v) = μ • A v := by
  73    have h := congrArg (fun Q : Module.End ℝ V => Q v) hA
  74    simpa using h
  75  have hscalar : μ⁻¹ * μ⁻¹ * μ = μ⁻¹ := by
  76    field_simp [hμ]
  77  simp [normalizedProjector, smul_smul, hAv]
  78  rw [hscalar]
  79
  80/-- `P²=P` implies `(2P-I)²=I`, the algebraic almost-product structure. -/
  81theorem almostProduct_sq {P : Module.End ℝ V} (hP : IsProjector P) :
  82    almostProduct P * almostProduct P = 1 := by
  83  ext v
  84  have hPv : P (P v) = P v := by
  85    have h := congrArg (fun Q : Module.End ℝ V => Q v) hP
  86    simpa [IsProjector] using h
  87  simp [almostProduct, sub_eq_add_neg, hPv]
  88  module
  89
  90/-- A projector induces a golden operator: `G² = G + I`. -/
  91theorem goldenOperator_sq {P : Module.End ℝ V} (hP : IsProjector P) :
  92    goldenOperator P * goldenOperator P = goldenOperator P + 1 := by
  93  ext v
  94  have hPv : P (P v) = P v := by
  95    have h := congrArg (fun Q : Module.End ℝ V => Q v) hP
  96    simpa [IsProjector] using h
  97  have hphi : Constants.phi ^ 2 = Constants.phi + 1 := Constants.phi_sq_eq
  98  have hphi_compl :
  99      1 - Constants.phi * 2 + Constants.phi ^ 2 = 2 - Constants.phi := by
 100    rw [hphi]
 101    ring
 102  have hphi_mul : Constants.phi * Constants.phi = Constants.phi + 1 := by
 103    simpa [pow_two] using hphi
 104  have hphi_compl_mul :
 105      (1 + -Constants.phi) * (1 + -Constants.phi) = 2 - Constants.phi := by
 106    nlinarith [hphi_compl]
 107  simp [goldenOperator, sub_eq_add_neg, map_add, map_smul, smul_smul, hPv]
 108  rw [hphi_mul, hphi_compl_mul]
 109  module
 110
 111/-- Normalizing an operator with `A² = μA` and `μ ≠ 0` gives a golden
 112operator satisfying `G² = G + I`. -/
 113theorem normalizedProjector_goldenOperator_sq
 114    {μ : ℝ} {A : Module.End ℝ V}
 115    (hA : A * A = μ • A) (hμ : μ ≠ 0) :
 116    goldenOperator (normalizedProjector μ A) *
 117      goldenOperator (normalizedProjector μ A) =
 118        goldenOperator (normalizedProjector μ A) + 1 :=
 119  goldenOperator_sq (normalizedProjector_isProjector hA hμ)
 120
 121/-- A nondegenerate rank-one endomorphism normalizes to a projector. -/
 122theorem rankOneEnd_normalized_isProjector
 123    (ell : V →ₗ[ℝ] ℝ) (v : V) (hμ : ell v ≠ 0) :
 124    IsProjector (normalizedProjector (ell v) (rankOneEnd ell v)) :=
 125  normalizedProjector_isProjector (rankOneEnd_square ell v) hμ
 126
 127/-- A nondegenerate rank-one endomorphism induces the golden-operator equation
 128after normalization. -/
 129theorem rankOneEnd_goldenOperator_sq
 130    (ell : V →ₗ[ℝ] ℝ) (v : V) (hμ : ell v ≠ 0) :
 131    goldenOperator (normalizedProjector (ell v) (rankOneEnd ell v)) *
 132      goldenOperator (normalizedProjector (ell v) (rankOneEnd ell v)) =
 133        goldenOperator (normalizedProjector (ell v) (rankOneEnd ell v)) + 1 :=
 134  normalizedProjector_goldenOperator_sq (rankOneEnd_square ell v) hμ
 135
 136/-- A positive scalar satisfying the golden-operator characteristic equation is
 137forced to be the RS golden ratio. -/
 138theorem goldenScalar_forces_phi {lam : ℝ}
 139    (h_lam_pos : 0 < lam) (h_lam : lam ^ 2 = lam + 1) :
 140    lam = Constants.phi := by
 141  have h_lam_ne_one : lam ≠ 1 := by
 142    intro h1
 143    rw [h1] at h_lam
 144    norm_num at h_lam
 145  have hclosure : 1 + lam = lam ^ 2 := by
 146    linarith
 147  exact PhiForcingDerived.phi_forcing_complete lam h_lam_pos h_lam_ne_one hclosure
 148
 149/-- The algebraic projector package supplied by the cost-induced projector
 150construction in the Hessian-geometry paper. -/
 151structure ProjectorGoldenCertificate : Prop where
 152  almost_product :
 153    ∀ {V : Type} [AddCommGroup V] [Module ℝ V] (P : Module.End ℝ V),
 154      IsProjector P → almostProduct P * almostProduct P = 1
 155  golden_structure :
 156    ∀ {V : Type} [AddCommGroup V] [Module ℝ V] (P : Module.End ℝ V),
 157      IsProjector P → goldenOperator P * goldenOperator P = goldenOperator P + 1
 158  normalized_operator_is_projector :
 159    ∀ {V : Type} [AddCommGroup V] [Module ℝ V] (μ : ℝ) (A : Module.End ℝ V),
 160      A * A = μ • A → μ ≠ 0 → IsProjector (normalizedProjector μ A)
 161  normalized_operator_golden_structure :
 162    ∀ {V : Type} [AddCommGroup V] [Module ℝ V] (μ : ℝ) (A : Module.End ℝ V),
 163      A * A = μ • A → μ ≠ 0 →
 164        goldenOperator (normalizedProjector μ A) *
 165          goldenOperator (normalizedProjector μ A) =
 166            goldenOperator (normalizedProjector μ A) + 1
 167  rank_one_square :
 168    ∀ {V : Type} [AddCommGroup V] [Module ℝ V] (ell : V →ₗ[ℝ] ℝ) (v : V),
 169      rankOneEnd ell v * rankOneEnd ell v = ell v • rankOneEnd ell v
 170  rank_one_normalized_projector :
 171    ∀ {V : Type} [AddCommGroup V] [Module ℝ V] (ell : V →ₗ[ℝ] ℝ) (v : V),
 172      ell v ≠ 0 → IsProjector (normalizedProjector (ell v) (rankOneEnd ell v))
 173  rank_one_golden_structure :
 174    ∀ {V : Type} [AddCommGroup V] [Module ℝ V] (ell : V →ₗ[ℝ] ℝ) (v : V),
 175      ell v ≠ 0 →
 176        goldenOperator (normalizedProjector (ell v) (rankOneEnd ell v)) *
 177          goldenOperator (normalizedProjector (ell v) (rankOneEnd ell v)) =
 178            goldenOperator (normalizedProjector (ell v) (rankOneEnd ell v)) + 1
 179  golden_scalar_forces_phi :
 180    ∀ {lam : ℝ}, 0 < lam → lam ^ 2 = lam + 1 → lam = Constants.phi
 181
 182/-- Any cost-induced normalized projector carries the golden-operator equation.
 183The cost geometry supplies the projector; this theorem supplies the polynomial
 184structure forced by being a projector. -/
 185theorem projector_golden_certificate : ProjectorGoldenCertificate where
 186  almost_product := @almostProduct_sq
 187  golden_structure := @goldenOperator_sq
 188  normalized_operator_is_projector := @normalizedProjector_isProjector
 189  normalized_operator_golden_structure := @normalizedProjector_goldenOperator_sq
 190  rank_one_square := @rankOneEnd_square
 191  rank_one_normalized_projector := @rankOneEnd_normalized_isProjector
 192  rank_one_golden_structure := @rankOneEnd_goldenOperator_sq
 193  golden_scalar_forces_phi := @goldenScalar_forces_phi
 194
 195end CostProjectorGolden
 196end Foundation
 197end IndisputableMonolith
 198