module module high

`IndisputableMonolith.Gravity.SevenGaps.Gap5ChartFromLedgerMomentum`

Defines the chart carrier for Gap 5 gravity work: ledger states as debit-credit pairs in R×R, the phase space of the symplectic J-cost action. Introduces imbalance, total, Casimir, balanced locus, and the uniqueness of imbalance as the linear functional vanishing on balance. Downstream momentum-additivity proofs cite this carrier and its linear selection lemma.

claimA ledger state is a pair $(d,c)\in\mathbb{R}\times\mathbb{R}$ (debit, credit). Derived scalars: imbalance $d-c$, total $d+c$, and the Casimir. The balanced locus is $\{d=c\}$. On that locus every linear functional vanishing at balance is a scalar multiple of imbalance; imbalance is the unique (normalized) linear selection of the off-balance direction.

background

Recognition Science treats the double-entry ledger as the phase space of the canonical cost. Upstream, Cost.SymplecticAction records that $J(x)=\frac12(x+x^{-1})-1$ is the symplectic action uniquely forced by the Recognition Composition Law together with reciprocity, normalization, calibration, and continuity. The area form on that phase space is what sigma-conservation preserves.

This module fixes the concrete chart: states are pairs in $\mathbb{R}\times\mathbb{R}$. From a state one reads imbalance (net debit-credit skew), total charge, and the Casimir invariant of the orbit. The balanced set is the diagonal where debit equals credit. Linear observables on the chart are classified by how they act on that diagonal.

The Gravity.SevenGaps program isolates seven missing steps between the ledger cost and continuum momentum. Gap 5 needs a carrier on which momentum can be read as a chart function of ledger data; this file supplies that carrier and the linear algebra of the imbalance coordinate.

proof idea

Definition-first module. It introduces the chart type, the scalar extractors (imbalance, total, Casimir), the balanced predicate, and the predicate that a linear functional vanishes on the balanced locus. The main theorem-shaped content is the uniqueness statement: any linear functional vanishing at balance is a multiple of imbalance, so imbalance is the unique linear selection of the off-balance direction (up to the stated normalization). Supporting equivalences connect the vanishes-at-balanced predicate to the balanced set. No long tactic developments; the argument is elementary linear algebra on $\mathbb{R}^2$.

why it matters in Recognition Science

Parent consumer is Gap5MomentumAdditivity (Track B, step B1). That module states that on this chart carrier, additivity of the momentum observable under ledger consolidation is proved from three named properties, each load-bearing by an exhibited countermodel. Its first premise is the kinetic condition that pointwise $|p|=|\mathrm{imbalance}|$, the magnitude half of the momentum reading.

Without a fixed $\mathbb{R}\times\mathbb{R}$ chart and a unique linear imbalance coordinate, those conditional closures have nowhere to sit. The module therefore anchors Gap 5 of the Seven Gaps gravity stack: it turns the abstract symplectic ledger of the J-cost into coordinates a continuum momentum observable can use. It does not itself close momentum additivity; it supplies the geometric stage on which that closure is stated.

scope and limits

Does not prove momentum additivity under consolidation; that lives downstream.
Does not derive J-uniqueness or the RCL; those are imported from Cost.
Does not identify imbalance with physical three-momentum beyond the chart reading.
Does not treat curved or field-valued ledgers; carrier is flat R×R.
Does not fix units or the phi-ladder mass formula.

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivity module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.SymplecticAction module_import

declarations in this module (48)

abbrev LedgerState L160
def balanced L164
def imbalance L168
def total L171
def casimir L175
theorem below L180
def orbitPoint L181
def linFunctional L186
def VanishesAtBalanced L190
def Balanced L197
theorem vanishesAtBalanced_iff L210
theorem imbalance_is_the_unique_linear_selection L220
theorem imbalance_vanishesAtBalanced L230
theorem linFunctional_one_neg_one L233
theorem vanishesOnBalancedLocus_iff L250
theorem imbalance_forced_by_balance_locus L265
theorem tolerated_family_is_a_scale_ray L281
def toVec L302
def imbalanceTotalMap L305
theorem imbalanceTotalMap_apply L307
theorem imbalanceTotalMap_det L314
theorem imbalance_total_is_a_canonical_pair L321
theorem Jlog_eq_two_sinh_half_sq L335
theorem orbitPoint_casimir L343
theorem orbitPoint_imbalance L355
theorem Jlog_eq_imbalance_sq_div_two_casimir L366
theorem chart_variable_is_the_normalized_imbalance L376
theorem chart_is_the_imbalance_coordinate L387
theorem sinh_two_arsinh L398
def powTwoJlog L408
theorem powTwoJlog_not_quadratic_in_imbalance L415
def nlP L451
def nlQ L455
theorem nlP_factor L457
theorem nlP_eq_zero_iff L462
theorem nlP_strictMono L471
theorem nlP_hasDerivAt L476
theorem nlP_hasDerivAt_snd L483
theorem nlQ_hasDerivAt_snd L486
theorem nl_jacobian_det_eq_one L499
theorem cost_not_quadratic_in_nlP L508
theorem chart_not_forced_without_linearity L523
theorem event_cost_differs_from_state_cost L539
theorem orbitPoint_is_reached_by_event L551
theorem additive_continuous_balanced_is_imbalance L593
theorem imbalance_is_additive_continuous_balanced L626
structure ChartStipulatedVerdict L648
theorem chartStipulatedVerdict L708