Foundation Jhessian Golden Multi Cost Hessian Operator Square

The operator's square

The recognition cost, a discrete record of how much it costs to recognize one state from another, is built from a simple reciprocal formula. In many coordinates at once, its Hessian, the matrix of second derivatives that measures local curvature, takes a special rank-one form. The declaration costHessianOperator_square proves a clean algebraic fact about that matrix: squaring it returns a scalar multiple of the matrix itself. Concretely, if A is the Hessian operator, the theorem states A² = c·A, where c is a positive number that depends on the coordinates.

This property is called being a projector up to scaling: after dividing by c, the operator becomes a genuine projector, meaning it acts like a shadow-caster that collapses everything onto a single line. The positivity of c is the load-bearing fact. It holds because the scalar cosh(α·t) is always greater than zero, and because the comparison direction α is not zero, so the inner product ⟨α, α⟩ is strictly positive. This mirrors the one-dimensional case where the second derivative at the minimum is exactly 1.

The theorem does not by itself produce the golden ratio. It establishes the projector structure, which is the raw material. The golden ratio φ emerges one step later, when the framework combines this projector with its complement to form the golden operator G = φP + (1−φ)(I−P), and then proves G² = G + I. That final equation, whose positive solution is φ, is what the framework credits with forcing the golden ratio as the unique self-similar scaling. The square theorem is the necessary preface, not the conclusion.

In the machine-checked library of formal theorems, this result is verified for any real inner-product space, finite or infinite dimensional. The proof is a direct application of a general lemma about rank-one endomorphisms, with no additional axioms and no unproved assumptions. The declaration's role in the framework is to certify that the multi-coordinate cost manifold carries the same projector structure that the one-dimensional case exhibited, so that the golden-ratio forcing is not an artifact of a single dimension.

/-- The multi-coordinate cost-Hessian operator satisfies `A² = μ A`
(paper Lemma 3.1). -/
theorem costHessianOperator_square (α t : V) :
    costHessianOperator α t * costHessianOperator α t
      = costHessianForm α t α • costHessianOperator α t :=
  rankOneEnd_square (costHessianForm α t) α

/-- **Nondegeneracy of the multi-coordinate J-Hessian.**  For a genuine
comparison direction `α ≠ 0`, the eigenvalue `μ = cosh(α·t)·‖α‖²` is strictly
positive: `cosh > 0` and `⟪α, α⟫ > 0`.  This is the exact multi-coordinate
analogue of `J''(1) = 1 > 0`. -/
lemma costHessianForm_self_pos (α t : V) (hα : α ≠ 0) :
    0 < costHessianForm α t α := by
  rw [costHessianForm_self]
  have hself : 0 < (inner ℝ α α : ℝ) := by
    have hne : (inner ℝ α α : ℝ) ≠ 0 := fun h => hα (inner_self_eq_zero.mp h)
    exact lt_of_le_of_ne real_inner_self_nonneg (Ne.symm hne)
  exact mul_pos (costHessianScalar_pos α t) hself

/-- The multi-coordinate cost-Hessian operator normalizes to a projector
(paper Corollary 3.1). -/
theorem costHessianOperator_normalized_isProjector (α t : V) (hα : α ≠ 0) :
    IsProjector
      (normalizedProjector (costHessianForm α t α) (costHessianOperator α t)) :=
  rankOneEnd_normalized_isProjector (costHessianForm α t) α
    (costHessianForm_self_ne_zero α t hα)

What this page does not claim

The theorem does not by itself derive the golden ratio; that requires the subsequent golden operator construction. The theorem does not assert that the Hessian is positive definite, only that it is positive semidefinite of rank one. The theorem does not establish any empirical claim about physical measurements; it is a purely algebraic result.

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/JHessianGoldenMulti.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: