IndisputableMonolith.Foundation.JHessianGoldenMulti

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Foundation.CostProjectorGolden
   4
   5/-!
   6# The multi-coordinate J-Hessian forces the golden operator (Phase 4 closure)
   7
   8`JHessianGolden` closed the Phase 4 φ-forcing for the one-dimensional recognition
   9scaling ray.  This module extends it to the genuine multi-coordinate recognition
  10cost manifold, following Washburn-Zlatanović, *Golden and Metallic Structures on
  11Hessian Manifolds* (arXiv:2606.02150).
  12
  13The `n`-dimensional reciprocal cost is
  14
  15  `J(x₁,…,xₙ) = ½(R + R⁻¹) − 1`,   `R = ∏ xᵢ^αᵢ`,   `α ∈ ℝⁿ \ {0}`,
  16
  17which in logarithmic coordinates `tᵢ = log xᵢ` is `J(t) = cosh(α·t) − 1`.  Its
  18Hessian is the rank-one tensor (paper, §2.1 and §6)
  19
  20  `∇²J = cosh(α·t) · (α ⊗ α)`,
  21
  22positive semidefinite of rank one *in every dimension*.  Pairing the rank-one
  23tensor with the nondegenerate reference Hessian metric `h₀ = ∇²(Σⱼ J(xⱼ))`
  24(equivalently, on the inner-product model, with the identity metric) gives the
  25`(1,1)`-tensor `A = h₀⁻¹ ∇²J`, which by the paper's Lemma 3.1 satisfies
  26
  27  `A² = μ A`,   `μ = cosh(α·t) · ‖α‖² = tr A`,
  28
  29so `A` normalizes to a projector `P = A/μ` (Corollary 3.1), and the induced
  30golden operator `G = φP + (1−φ)(I−P)` satisfies `G² = G + I` (§4), forcing the
  31positive eigenvalue to be `φ`.
  32
  33The decisive point for Phase 4 is the **nondegeneracy source**: the eigenvalue
  34`μ = cosh(α·t)·‖α‖²` is strictly positive precisely because `cosh > 0` (strict
  35convexity of the recognition well in the comparison direction) and `α ≠ 0` (a
  36genuine recognition comparison exists).  This is the multi-coordinate version of
  37the unit positive curvature `J''(1) = 1` used in `JHessianGolden`, and it holds
  38in arbitrary finite or infinite dimension because the construction is carried out
  39over an arbitrary real inner-product space.
  40
  41Status: 0 sorry, 0 new axiom.
  42-/
  43
  44namespace IndisputableMonolith
  45namespace Foundation
  46namespace JHessianGoldenMulti
  47
  48open CostProjectorGolden
  49
  50variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  51
  52/-! ## The inner-product comparison functional -/
  53
  54/-- The comparison one-form `ω(X) = ⟪α, X⟫` of the recognition cost, as a real
  55linear functional.  On the inner-product model this is the metric dual of the
  56distinguished comparison direction `α` (paper: `ω = Σ αᵢ dxᵢ/xᵢ`, `V = h⁻¹ω`). -/
  57noncomputable def innerForm (α : V) : V →ₗ[ℝ] ℝ where
  58  toFun := fun x => inner ℝ α x
  59  map_add' := by intro x y; simp only [inner_add_right]
  60  map_smul' := by
  61    intro a x
  62    simp only [RingHom.id_apply, smul_eq_mul, real_inner_smul_right]
  63
  64@[simp] lemma innerForm_apply (α x : V) : innerForm α x = inner ℝ α x := rfl
  65
  66/-! ## The cost-Hessian curvature scalar and rank-one operator -/
  67
  68/-- The recognition-cost curvature scalar along the comparison direction:
  69`cosh(α·t)`.  This is the (rank-one) Hessian eigenvalue density of
  70`J(t) = cosh(α·t) − 1` at the log-coordinate point `t`. -/
  71noncomputable def costHessianScalar (α t : V) : ℝ := Real.cosh (inner ℝ α t)
  72
  73/-- The recognition well is strictly curved in every comparison direction:
  74`cosh(α·t) > 0`.  This is the multi-coordinate strict convexity that supplies
  75the golden route's nondegeneracy. -/
  76lemma costHessianScalar_pos (α t : V) : 0 < costHessianScalar α t :=
  77  Real.cosh_pos _
  78
  79/-- The cost-Hessian functional `ℓ(X) = cosh(α·t) · ⟪α, X⟫`, i.e. the rank-one
  80Hessian tensor `cosh(α·t) (α ⊗ α)` with one index lowered. -/
  81noncomputable def costHessianForm (α t : V) : V →ₗ[ℝ] ℝ :=
  82  (costHessianScalar α t) • innerForm α
  83
  84@[simp] lemma costHessianForm_apply (α t x : V) :
  85    costHessianForm α t x = costHessianScalar α t * inner ℝ α x := by
  86  simp [costHessianForm, LinearMap.smul_apply, smul_eq_mul]
  87
  88/-- The multi-coordinate cost-Hessian rank-one operator
  89`A X = cosh(α·t) · ⟪α, X⟫ · α` (paper eq. (6.3) with reference metric the
  90identity). -/
  91noncomputable def costHessianOperator (α t : V) : Module.End ℝ V :=
  92  rankOneEnd (costHessianForm α t) α
  93
  94/-- The rank-one eigenvalue is `μ = cosh(α·t) · ⟪α, α⟫ = cosh(α·t) · ‖α‖²`
  95(paper: `μ = g(V,V) = tr A`). -/
  96lemma costHessianForm_self (α t : V) :
  97    costHessianForm α t α = costHessianScalar α t * inner ℝ α α := by
  98  simp [costHessianForm_apply]
  99
 100/-- **Nondegeneracy of the multi-coordinate J-Hessian.**  For a genuine
 101comparison direction `α ≠ 0`, the eigenvalue `μ = cosh(α·t)·‖α‖²` is strictly
 102positive: `cosh > 0` and `⟪α, α⟫ > 0`.  This is the exact multi-coordinate
 103analogue of `J''(1) = 1 > 0`. -/
 104lemma costHessianForm_self_pos (α t : V) (hα : α ≠ 0) :
 105    0 < costHessianForm α t α := by
 106  rw [costHessianForm_self]
 107  have hself : 0 < (inner ℝ α α : ℝ) := by
 108    have hne : (inner ℝ α α : ℝ) ≠ 0 := fun h => hα (inner_self_eq_zero.mp h)
 109    exact lt_of_le_of_ne real_inner_self_nonneg (Ne.symm hne)
 110  exact mul_pos (costHessianScalar_pos α t) hself
 111
 112/-- The eigenvalue is nonzero for a genuine comparison direction. -/
 113lemma costHessianForm_self_ne_zero (α t : V) (hα : α ≠ 0) :
 114    costHessianForm α t α ≠ 0 :=
 115  ne_of_gt (costHessianForm_self_pos α t hα)
 116
 117/-! ## The golden structure forced by the multi-coordinate J-Hessian -/
 118
 119/-- The multi-coordinate cost-Hessian operator satisfies `A² = μ A`
 120(paper Lemma 3.1). -/
 121theorem costHessianOperator_square (α t : V) :
 122    costHessianOperator α t * costHessianOperator α t
 123      = costHessianForm α t α • costHessianOperator α t :=
 124  rankOneEnd_square (costHessianForm α t) α
 125
 126/-- The multi-coordinate cost-Hessian operator normalizes to a projector
 127(paper Corollary 3.1). -/
 128theorem costHessianOperator_normalized_isProjector (α t : V) (hα : α ≠ 0) :
 129    IsProjector
 130      (normalizedProjector (costHessianForm α t α) (costHessianOperator α t)) :=
 131  rankOneEnd_normalized_isProjector (costHessianForm α t) α
 132    (costHessianForm_self_ne_zero α t hα)
 133
 134/-- **Multi-coordinate Phase 4 φ-forcing.**  The golden operator induced by the
 135`n`-dimensional recognition cost's Hessian satisfies `G² = G + I` (paper §4,
 136eq. (6.7)), for an arbitrary comparison direction `α ≠ 0` at an arbitrary
 137log-coordinate point `t`, over an arbitrary real inner-product space. -/
 138theorem costHessianOperator_goldenOperator_sq (α t : V) (hα : α ≠ 0) :
 139    goldenOperator
 140        (normalizedProjector (costHessianForm α t α) (costHessianOperator α t)) *
 141      goldenOperator
 142        (normalizedProjector (costHessianForm α t α) (costHessianOperator α t)) =
 143        goldenOperator
 144          (normalizedProjector (costHessianForm α t α)
 145            (costHessianOperator α t)) + 1 :=
 146  rankOneEnd_goldenOperator_sq (costHessianForm α t) α
 147    (costHessianForm_self_ne_zero α t hα)
 148
 149/-- The golden scalar equation forces `φ` (re-exported). -/
 150theorem goldenScalar_forces_phi {lam : ℝ}
 151    (h_lam_pos : 0 < lam) (h_lam : lam ^ 2 = lam + 1) :
 152    lam = Constants.phi :=
 153  CostProjectorGolden.goldenScalar_forces_phi h_lam_pos h_lam
 154
 155/-! ## Multi-coordinate certificate -/
 156
 157/-- The multi-coordinate concrete-J-Hessian φ-forcing certificate: the
 158`n`-dimensional recognition cost's own Hessian supplies the nondegenerate
 159rank-one operator the golden route needs, in arbitrary dimension, so φ-forcing
 160no longer rests on either a supplied operator or a single-coordinate
 161restriction. -/
 162structure JHessianGoldenMultiCertificate
 163    (α t : V) (hα : α ≠ 0) : Prop where
 164  /-- The curvature scalar `cosh(α·t)` is strictly positive. -/
 165  curvature_pos : 0 < costHessianScalar α t
 166  /-- The rank-one eigenvalue `μ = cosh(α·t)·⟪α,α⟫` is strictly positive. -/
 167  eigenvalue_pos : 0 < costHessianForm α t α
 168  /-- `A² = μ A` for the concrete multi-coordinate operator. -/
 169  operator_square :
 170    costHessianOperator α t * costHessianOperator α t
 171      = costHessianForm α t α • costHessianOperator α t
 172  /-- The operator normalizes to a projector. -/
 173  normalized_is_projector :
 174    IsProjector
 175      (normalizedProjector (costHessianForm α t α) (costHessianOperator α t))
 176  /-- The induced golden operator satisfies `G² = G + I`. -/
 177  golden_structure :
 178    goldenOperator
 179        (normalizedProjector (costHessianForm α t α) (costHessianOperator α t)) *
 180      goldenOperator
 181        (normalizedProjector (costHessianForm α t α) (costHessianOperator α t)) =
 182        goldenOperator
 183          (normalizedProjector (costHessianForm α t α)
 184            (costHessianOperator α t)) + 1
 185  /-- The golden scalar equation forces `φ`. -/
 186  golden_scalar_forces_phi :
 187    ∀ {lam : ℝ}, 0 < lam → lam ^ 2 = lam + 1 → lam = Constants.phi
 188
 189/-- The multi-coordinate concrete RS J-Hessian discharges the golden-structure
 190φ-forcing hypotheses in arbitrary dimension. -/
 191theorem jHessianGoldenMultiCertificate (α t : V) (hα : α ≠ 0) :
 192    JHessianGoldenMultiCertificate α t hα where
 193  curvature_pos := costHessianScalar_pos α t
 194  eigenvalue_pos := costHessianForm_self_pos α t hα
 195  operator_square := costHessianOperator_square α t
 196  normalized_is_projector := costHessianOperator_normalized_isProjector α t hα
 197  golden_structure := costHessianOperator_goldenOperator_sq α t hα
 198  golden_scalar_forces_phi := @goldenScalar_forces_phi
 199
 200end JHessianGoldenMulti
 201end Foundation
 202end IndisputableMonolith
 203