module module moderate

`IndisputableMonolith.Cost.SymplecticAction`

Defines the ledger symplectic area form on the two-dimensional debit/credit phase space and the associated conservation predicates. Gravity and strain-dynamics modules import it to relate recognition cost to momentum charts, additivity, and kinetic rigidity. The module packages the area form, defect measures, and trace/adjugate identities that characterize area-preserving linear maps.

claimOn the $2$D debit/credit phase space, the ledger symplectic area form $\omega$ is introduced, together with the defect that measures failure of a linear map to preserve $\omega$, and the predicate that a map conserves the ledger area (equivalently, has vanishing defect). Supporting identities relate traces, adjugates, and reciprocal eigenvalue pairing for such maps.

background

Recognition Science treats the elementary ledger as a two-dimensional phase space whose coordinates are debit and credit. The cost functional $J$ (unique under the T5 forcing chain, with $J(x)=(x+x^{-1})/2-1$) lives on positive reals; the present module supplies the symplectic geometry of the underlying ledger plane rather than the cost itself.

The parent Cost module and the FunctionalEquation helpers for T5 uniqueness sit upstream. Here the focus is the area form on debit/credit, the defect that quantifies non-preservation of that form, and linear-algebraic characterizations (trace identities, adjugate sums, reciprocal eigenvalue pairing) of maps that conserve ledger area.

Downstream gravity work (Gap5 momentum charts, momentum additivity, HKT kinetic rigidity, strain-dynamics kernel reach) imports this geometry when asking whether recognition primitives force classical momentum or kinetic structure.

proof idea

Definition-and-lemma module, not a single theorem. It introduces the area form and its action on vectors, the conservation predicate and the sigma-area defect, then proves equivalences: conservation iff defect vanishes, and conservation iff the map preserves area. Trace and adjugate identities, reciprocal eigenvalue pairing, and diagonal SL(2)-type constructions support those characterizations. No single forcing argument; the content is the geometric toolkit.

why it matters in Recognition Science

Supplies the symplectic ledger geometry consumed by the Gravity.SevenGaps stack. Gap5ChartFromLedgerMomentum asks whether a half-imbalance chart is derived or stipulated (verdict: stipulated). Gap5MomentumAdditivityComposition runs a composition-law attack on unconditional momentum additivity. HKTKineticFromRecognitionCost targets halving the disclosed kinetic premise in Pillar 1. StrainDynamicsKernelReach asks how far the recognition kernel reaches: it fixes cost, not motion.

Within the framework, this sits under the Cost domain that feeds T5 J-uniqueness and the Recognition Composition Law. It does not itself force $D=3$ or the eight-tick octave; it equips the debit/credit plane so later modules can test whether cost geometry yields classical gravity primitives.

scope and limits

Does not derive classical gravity or prove that the half-imbalance chart is forced.
Does not establish unconditional momentum additivity or kinetic rigidity alone.
Does not replace T5 J-uniqueness or the Recognition Composition Law.
Does not claim the area form determines strain dynamics or equations of motion.
Does not fix spacetime dimension or the eight-tick period.

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.Gap5ChartFromLedgerMomentum module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivityComposition module_import
IndisputableMonolith.Gravity.SevenGaps.HKTKineticFromRecognitionCost module_import
IndisputableMonolith.Gravity.SevenGaps.StrainDynamicsKernelReach module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.FunctionalEquation module_import

declarations in this module (25)

def areaForm L84
theorem areaForm_mulVec L87
def ConservesSigma L97
def sigmaAreaDefect L100
theorem conservesSigma_iff_defect_zero L102
theorem conservesSigma_iff_preservesArea L109
theorem ledger_adjugate_sum L127
theorem trace_mul_add_trace_mul_adjugate L138
theorem trace_identity_of_conservesSigma L152
theorem reciprocal_eigenvalue_pairing L165
def diagSL L174
theorem diagSL_trace L176
theorem diagSL_det L179
theorem diagSL_conservesSigma L182
def traceCost L187
theorem traceCost_diagSL L191
theorem jcost_exp_eq_cosh_sub_one L198
theorem trace_diagSL_mul L204
theorem trace_diagSL_mul_inv L208
theorem split_torus_trace_identity L218
theorem rcl_from_symplectic_action L229
theorem jcost_satisfiesCompositionLaw_via_symplectic L248
theorem jcost_forced_by_symplectic_action L258
structure SymplecticActionCert L276
theorem symplecticActionCert L298