Cost Symplectic Action Trace Mul Add Trace Mul Adjugate

The trace identity

In linear algebra, the trace of a square matrix is the sum of its diagonal entries. For any two 2x2 matrices A and B, the trace identity states that the trace of A times B, plus the trace of A times the adjugate of B, equals the trace of A times the trace of B. The adjugate of a 2x2 matrix is a related matrix built from its entries, and for a matrix with determinant 1, the adjugate is exactly its inverse. This identity is a classical result, a direct consequence of the Cayley-Hamilton theorem, which says a matrix satisfies its own characteristic equation.

The identity gains physical meaning in the Recognition Science framework, which models a double-entry ledger as a two-dimensional phase space. A state is a pair (debit, credit), and a recognition event is a linear map on this space. The conservation law that no net imbalance is created is equivalent to the map preserving area, meaning its determinant is 1. For such area-preserving maps, the adjugate is the inverse, so the trace identity becomes: trace(A·B) + trace(A·B⁻¹) = trace(A) · trace(B).

In Recognition Science, the cost of an event is defined as half its trace minus 1. On a diagonal matrix with entries x and 1/x, this cost is exactly J(x) = (x + 1/x)/2 - 1. The trace identity then forces the Recognition Composition Law, the equation that J(x·y) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), to hold. This is significant because the composition law was previously a stated primitive; now it is derived from the area-preserving nature of the ledger.

This chain of reasoning is verified in the framework's machine-checked library of formal theorems. The declaration trace_mul_add_trace_mul_adjugate is the foundational 2x2 matrix identity. From it, the framework derives the trace identity for area-preserving maps, then the composition law, and finally the uniqueness of J as the cost function. The framework proves that the symplectic structure, the area-preserving geometry, is not an extra assumption but is forced by the conservation law.

The declaration does not claim that the trace identity itself is new; it is a standard result. It does not claim that the physical interpretation of J as a cost is derived from the identity alone; that identification is a documented bridge definition. It also does not claim that the framework's derivation of three spatial dimensions or other physical constants follows directly from this single identity; those results depend on the full forcing chain.

/-- **The trace identity, adjugate form.**  Holds for all 2×2 maps (pure
Cayley–Hamilton; no determinant hypothesis):
`tr(A·B) + tr(A·adj B) = tr A · tr B`. -/
theorem trace_mul_add_trace_mul_adjugate (A B : Matrix (Fin 2) (Fin 2) ℝ) :
    (A * B).trace + (A * B.adjugate).trace = A.trace * B.trace := by
  have hsum := ledger_adjugate_sum B
  have h1 : (A * B).trace + (A * B.adjugate).trace
      = (A * (B + B.adjugate)).trace := by
    rw [Matrix.mul_add, Matrix.trace_add]
  rw [h1, hsum, Matrix.mul_smul, Matrix.mul_one, Matrix.trace_smul, smul_eq_mul,
    mul_comm]

/-- **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

/-- **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 trace identity is a new mathematical result. The identification of J with a physical cost is derived solely from the trace identity. The framework's derivation of three spatial dimensions follows directly from this single identity.

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: