Cost Symplectic Action Conserves Sigma Iff Preserves Area

The ledger as a phase space

A double-entry ledger records every event as a pair of numbers, a debit and a credit. In the Recognition Science framework, such a ledger is modeled as a two-dimensional phase space, and a recognition event is a linear map on that space. The ledger's fundamental conservation law, written σ = 0, says no net imbalance is created by any event. The declaration conservesSigma_iff_preservesArea proves that this conservation law is exactly equivalent to the map preserving the ledger's symplectic area form, and for 2×2 maps this is precisely the condition that the determinant equals 1.

This equivalence is not a definitional choice; it is a proved theorem. The area form ω(v,w) = v₀w₁ − v₁w₀ is the geometric object that measures the signed area of the parallelogram spanned by two vectors. A map preserves area when ω(Mv, Mw) = ω(v, w) for all vectors v and w. The theorem conservesSigma_iff_preservesArea states that this area-preservation condition holds if and only if the map's determinant is 1, which is the definition of ConservesSigma. This means the "symplectic ledger" is not an extra assumption; it is the content of σ = 0.

From this area-preservation condition, the framework derives a trace identity: for any area-preserving map B, and any map A, the trace of A·B plus the trace of A·B⁻¹ equals the trace of A times the trace of B. This identity, proved in trace_identity_of_conservesSigma, is the engine that forces the cost function. The recognition cost of an event is defined as half its trace minus 1, a functional that vanishes on the identity map, which represents the balanced ledger. On a diagonal map diag(x, x⁻¹), this cost evaluates exactly to J(x) = ½(x + x⁻¹) − 1.

The decisive step is that this trace identity, specialized to diagonal maps, reproduces the Recognition Composition Law (RCL): J(x·y) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This law was previously a stated primitive, but here it is derived as a theorem from the area-preservation condition alone. Feeding this derived RCL into the earlier functional equation theorem law_of_logic_forces_jcost closes the loop: σ = 0 implies symplectic, which implies RCL, which, with reciprocity, normalization, calibration, and continuity, forces F = J. The cost function J is therefore not assumed; it is the unique cost of area-preserving recognition dynamics.

What this establishes is a chain of equivalences: the physical conservation law (σ = 0) is the same as a geometric property (area preservation), which forces an algebraic identity (the trace identity), which forces a functional equation (RCL), which forces a unique cost function (J). The declaration conservesSigma_iff_preservesArea is the first link in this chain, and it is a proved theorem in the framework's machine-checked library. The result is that the ledger's cost function is not a free parameter but a forced consequence of its own conservation law.

What this declaration does not claim is that area preservation is the only way to define a cost function, or that the physical interpretation of J as a cost is itself proved. The identification of J with a physical cost is a documented bridge definition, not a theorem. The declaration also does not claim that all recognition events are area-preserving; it only establishes the equivalence for those that are. Finally, it does not claim that the trace identity holds for all maps, only for those where B is area-preserving.

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

This declaration does not prove that all recognition events must be area-preserving. This declaration does not establish the physical interpretation of J as a cost; that remains a documented bridge definition. This declaration does not claim the trace identity holds for all matrices, only for those where the second argument is area-preserving.

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: