Cost Symplectic Action

The symplectic ledger

In classical mechanics, a symplectic structure is a geometric way of describing systems that conserve a quantity like energy or momentum; the area of a region in phase space stays fixed as the system evolves. The cost symplectic action in Recognition Science is the discovery that the same structure appears when you keep records for a universe. A ledger, a discrete record of events, can be treated as a two-dimensional phase space: each state is a pair (debit, credit). A recognition event is a linear map that transforms one state into another. The framework's central conservation law, that no net imbalance is ever created, is exactly the statement that this map preserves area. For a two-by-two matrix, preserving area is the same as having determinant equal to one, which is the definition of the symplectic group Sp(2,ℝ).

The payoff is that the cost function J(x) = ½(x + x⁻¹) − 1, which the framework proves is forced by five plain conditions, is not an arbitrary bookkeeping choice. On the symplectic group, the cost of an event is simply half its trace minus one: traceCost(M) = ½ tr(M) − 1. For the simplest kind of event, one that scales a debit by a factor x and a credit by 1/x, this cost reduces exactly to J(x). The composition law that was previously a stated primitive, the rule J(x·y) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), now follows as a theorem from the trace identity of the area-preserving group. The ledger's conservation law forces the symplectic structure, which forces the composition law, which forces the cost function. The loop closes: σ = 0 implies symplectic implies RCL implies J.

The machine-checked library of formal theorems proves this chain in Lean. The key statements are that conserving sigma is equivalent to preserving area, that the trace identity holds for all area-preserving matrices, and that the cost of the diagonal event is exactly J(x). A final theorem shows that J(eᵗ) = cosh(t) − 1, so the cost grows like a hyperbolic cosine of the event's log-eigenvalue, and is uniquely minimized at the balanced ledger where t = 0. This means the cost of recognition is not a convention; it is the geometric consequence of a conservation law. The framework's cost function is the action of the unique area-preserving recognition dynamics.

/-- **σ = 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 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 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 symplectic structure is not an extra assumption; it is equivalent to the σ = 0 conservation law. The composition law is not a primitive here; it is derived as a theorem from the trace identity. This module does not derive the fine-structure constant or any other specific coupling constant.

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: