Cost Symplectic Action Trace Identity Of Conserves Sigma

The trace identity

The trace of a matrix is the sum of its diagonal entries. The trace identity states that for any two 2x2 matrices A and B, where B has determinant 1, the trace of A times B plus the trace of A times B inverse equals the trace of A times the trace of B. In symbols: tr(A·B) + tr(A·B⁻¹) = tr(A)·tr(B). This is a theorem about 2x2 matrices, proved in the framework's machine-checked library of formal theorems.

The identity matters because it connects the ledger's conservation law to the framework's central cost function. In the framework, a ledger (a discrete record of events) is modeled as a two-dimensional phase space, and a recognition event is a linear map on that space. The conservation law σ = 0, meaning no net imbalance is created, is exactly the condition that the map preserves area. For 2x2 matrices, area preservation is equivalent to having determinant 1. The trace identity holds precisely for matrices with determinant 1, so it is a direct consequence of the conservation law.

The framework defines a cost for each event as half its trace minus one. On the special case of a diagonal matrix with entries x and x⁻¹, this cost equals J(x) = ½(x + x⁻¹) − 1. Substituting such diagonal matrices into the trace identity yields the Recognition Composition Law, the equation that uniquely forces J. This is a key step: the composition law, previously a stated primitive, is now derived as a theorem from the more physical principle of area preservation.

In Recognition Science, this establishes that the cost function J is not an arbitrary choice but is forced by the conservation law. The framework proves that any cost function satisfying the composition law, along with reciprocity, normalization, calibration, and continuity, must equal J. The trace identity provides the physical grounding for that composition law. The framework's library shows that the cost of an event with log-eigenvalue t is cosh(t) − 1, minimized at the balanced ledger where t = 0.

What the declaration does not claim is that the conservation law σ = 0 is itself derived from something more fundamental. It is a stated primitive of the framework. The trace identity also does not establish that the framework's model of physics is correct; it only shows that within the framework, the cost function follows from the conservation law. The bridge from the mathematical structure to physical reality remains a documented definition, not a theorem.

/-- **The SL(2,ℝ) trace identity of the area-preserving ledger group.**  When the
"reverse event" `B⁻¹` exists (σ = 0, i.e. `det B = 1`), the adjugate is the
inverse and the trace identity becomes
`tr(A·B) + tr(A·B⁻¹) = tr A · tr B`.  This is the Fricke/SL(2) identity; below it
specializes to the Recognition Composition Law. -/
theorem trace_identity_of_conservesSigma (A B : Matrix (Fin 2) (Fin 2) ℝ)
    (hB : ConservesSigma B) :
    (A * B).trace + (A * B⁻¹).trace = A.trace * B.trace := by
  have hdet : B.det = 1 := hB
  have hadj : B⁻¹ = B.adjugate := by
    rw [Matrix.inv_def, hdet]; simp
  rw [hadj]
  exact trace_mul_add_trace_mul_adjugate A B

/-- **σ = 0 is exactly symplectic (area-preserving).**  A ledger event conserves
σ iff it preserves the ledger area form, iff `det = 1`. -/
theorem conservesSigma_iff_preservesArea (M : Matrix (Fin 2) (Fin 2) ℝ) :
    ConservesSigma M ↔
      ∀ v w : Fin 2 → ℝ, areaForm (M.mulVec v) (M.mulVec w) = areaForm v w := by
  unfold ConservesSigma
  constructor
  · intro hdet v w
    rw [areaForm_mulVec, hdet, one_mul]
  · intro h
    have h01 := h ![1, 0] ![0, 1]
    rw [areaForm_mulVec] at h01
    have hbase : areaForm (![1, 0] : Fin 2 → ℝ) ![0, 1] = 1 := by
      simp [areaForm]
    rw [hbase, mul_one] at h01
    exact h01

/-- **The symplectic action cost is `J`.**  On the split torus the calibrated
trace functional equals the canonical recognition cost. -/
@[simp] theorem traceCost_diagSL (x : ℝ) : traceCost (diagSL x) = Cost.Jcost x := by
  unfold traceCost Cost.Jcost
  rw [diagSL_trace]

/-- **The Recognition Composition Law is the SL(2) trace identity.**  The
previously-primitive RCL is derived here as the trace identity of the
area-preserving (σ = 0) ledger group, specialized to the split torus. -/
theorem rcl_from_symplectic_action (x y : ℝ) (_hx : 0 < x) (hy : 0 < y) :
    Cost.Jcost (x * y) + Cost.Jcost (x / y)
      = 2 * Cost.Jcost x * Cost.Jcost y + 2 * Cost.Jcost x + 2 * Cost.Jcost y := by
  have key := split_torus_trace_identity x y hy.ne'
  have hJxy : Cost.Jcost (x * y) = (x * y + x⁻¹ * y⁻¹) / 2 - 1 := by
    unfold Cost.Jcost; rw [_root_.mul_inv_rev]; ring
  have hJxiy : Cost.Jcost (x / y) = (x * y⁻¹ + x⁻¹ * y) / 2 - 1 := by
    unfold Cost.Jcost
    simp only [div_eq_mul_inv, _root_.mul_inv_rev, inv_inv]
    ring
  rw [hJxy, hJxiy]
  unfold Cost.Jcost
  linear_combination (1 / 2 : ℝ) * key

/-- **The recognition cost is forced to be `J` by the symplectic action.**  Any
reciprocal, normalized, calibrated, continuous cost whose composition law is the
symplectic trace identity (`SatisfiesCompositionLaw`, here supplied by the
area-preserving ledger group) equals `J`.  This composes the σ = 0 ⇒ symplectic
⇒ RCL derivation of this module with the cost-shape uniqueness theorem
`law_of_logic_forces_jcost`, closing the documented bridge. -/
theorem jcost_forced_by_symplectic_action (F : ℝ → ℝ)
    [FunctionalEquation.AczelSmoothnessPackage]
    (hRecip : FunctionalEquation.IsReciprocalCost F)
    (hNorm : FunctionalEquation.IsNormalized F)
    (hComp : FunctionalEquation.SatisfiesCompositionLaw F)
    (hCalib : FunctionalEquation.IsCalibrated F)
    (hCont : ContinuousOn F (Set.Ioi 0)) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
  FunctionalEquation.law_of_logic_forces_jcost F hRecip hNorm hComp hCalib hCont

What this page does not claim

The conservation law σ = 0 is not derived from a more fundamental principle. The trace identity does not establish the correctness of the framework's physical model. The bridge from the mathematical structure to physical reality is not a theorem.

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/Cost/SymplecticAction.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: