Cost Symplectic Action Rcl From Symplectic Action

The symplectic origin of the cost law

In classical mechanics, a symplectic structure is a geometric way of describing systems that conserve a certain quantity, usually energy or phase-space volume. The Recognition Science framework 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 framework's central conservation law, σ = 0, states that no net imbalance is created. Geometrically, this is exactly area preservation: the map preserves the ledger's symplectic area form. For 2×2 maps, area preservation is equivalent to having determinant 1, the group SL(2,ℝ) = Sp(2,ℝ).

The key identity comes from Cayley–Hamilton in two dimensions, which gives that for any area-preserving matrix B, B + adj(B) = tr(B)·I. This yields the SL(2) trace identity: tr(A·B) + tr(A·B⁻¹) = tr(A)·tr(B). The recognition cost of an event is defined as the calibrated trace functional traceCost(M) = ½tr(M) − 1, which vanishes on the identity matrix, the balanced ledger. On the split torus diag(x, x⁻¹), where eigenvalues are forced into a reciprocal pair, this cost is exactly J(x) = ½(x + x⁻¹) − 1.

Specializing the trace identity to the split torus reproduces the Recognition Composition Law (RCL), J(x·y) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), as a theorem rather than a primitive assumption. This is the declaration rcl_from_symplectic_action. The RCL was previously a stated primitive whose physical interpretation was a documented bridge definition; this result discharges that bridge from an independently physical variational principle. The framework proves that σ = 0 implies symplectic, which implies the RCL, which with reciprocity, normalization, calibration, and continuity forces J uniquely. The cost is also cosh of the generator's log-eigenvalue: J(eᵗ) = cosh t − 1, uniquely minimized at the balanced ledger t = 0.

What this does not claim: the identification of J with a physical cost remains a documented bridge definition, not a theorem. The framework does not derive the fine-structure constant or any other coupling from this alone. The declaration establishes a mathematical equivalence between a conservation law and a composition law, not a claim about which physical system realizes this ledger. The physical recognition-to-linking bridge, which would connect this to three spatial dimensions, remains open.

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

/-- **σ = 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 action cost is `cosh` of the generator's log-eigenvalue: with `x = eᵗ`,
`J(eᵗ) = cosh t − 1`.  `t` is the Hamiltonian action of the event; the cost is
minimized at the balanced ledger `t = 0`. -/
theorem jcost_exp_eq_cosh_sub_one (t : ℝ) :
    Cost.Jcost (Real.exp t) = Real.cosh t - 1 := by
  simp only [Cost.Jcost, Real.cosh_eq, Real.exp_neg]

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

What this page does not claim

The identification of J with a physical cost is a documented bridge definition, not a theorem. The declaration does not derive the fine-structure constant or any other coupling constant. The declaration does not claim which physical system realizes the ledger phase space.

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: