module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap2DynamicsKindRule`

Defines the posting dynamics layer for Gap 2: the balanced zero ledger as initial condition, single-unit debit/credit posts, reachability, and mass. Physicists tracing whether dual-entry dynamics force kind-only charge rules cite this carrier. The module packages ledger adjacency into an explicit dynamical system with phi-change lemmas and mass characterizations.

claimA ledger state is a pair of maps (debit, credit). The zero ledger $L_0$ has every column empty. A post at account $a$ adds one unit as debit or credit. Reachability is the reflexive-transitive closure of single posts from $L_0$. The imbalance $\phi = \mathrm{debit}-\mathrm{credit}$ changes by $\pm 1$ at exactly one coordinate per post. Mass is the total posted weight; mass zero iff the state is $L_0$.

background

Gap 2 asks whether the dual-entry substrate forces the counting premises used in posting-cost derivations. The prior arc (Gap2LatticeKindRule) settled whether the lattice alone forces ChargesCountsOnly (charge as a function of three cell counts and letter kind). This module shifts from static lattice structure to dynamics: histories are generated by posts, not selected among fixed states.

Upstream LedgerPostingAdjacency supplies the ledger-shaped model: each tick posts exactly one unit to exactly one account as debit or credit, so a single post changes $\phi=\mathrm{debit}-\mathrm{credit}$ by $\pm 1$ at one coordinate (parity one-bit adjacency). The zero ledger is every column empty; the module doc treats it as the initial condition that CanonicalHistory.state_canonical pins counted histories to.

Sibling content introduces postAt, the reachability predicate generated by posts, mass, and the predecessor relation used to walk histories backward.

proof idea

Definition-and-lemma module, not a single theorem. It introduces the zero ledger, the post operation, and reachability, then proves elementary dynamical facts: self-action of debit/credit posts on $\phi$, that distinct posts move $\phi$ differently, ledger extensionality, mass characterizations (mass zero iff zero ledger; nonzero mass yields a positive coordinate), and a predecessor map on reachable states. Arguments are direct from the posting adjacency model: case splits on debit versus credit and coordinatewise arithmetic on $\phi$.

why it matters in Recognition Science

Supplies the dynamical carrier that later Gap 2 arcs import. Gap2IncidenceSilenceVerdict uses it when banking the scoped no-go that the ledger layer does not force aggregate linearity by kind (FixedKindTotals) on posting cost. Gap2PostingLayerFloor builds the pinned-carrier floor and uniqueness wall against deriving GaugeCountingPrinciple from richer-than-counting substrate at the posting layer. InsertionAsymmetryInevitableReasons draws on the same dynamics when census-ing necessary reasons for asymmetric carrier-enlarging rate laws.

In the Seven Gaps gravity program this is the bridge from static dual-entry structure to time-ordered posting histories, so questions about what the substrate forces can be stated as properties of reachable ledgers rather than free states.

scope and limits

Does not prove that dynamics force ChargesCountsOnly or FixedKindTotals.
Does not derive GaugeCountingPrinciple from posting structure.
Does not address incidence silence; that is a downstream verdict module.
Does not model multi-unit or multi-account posts in one tick.
Does not fix physical units or couple ledgers to spacetime metrics.

used by (3)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2IncidenceSilenceVerdict module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2PostingLayerFloor module_import
IndisputableMonolith.Gravity.SevenGaps.InsertionAsymmetryInevitableReasons module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2LatticeKindRule module_import
IndisputableMonolith.LedgerPostingAdjacency module_import

declarations in this module (39)

def zeroLedger L92
def postAt L99
inductive PostReachable L110
theorem phi_zeroLedger L117
theorem phi_postAt_debit_self L119
theorem phi_postAt_credit_self L128
theorem phi_postAt_ne L137
theorem ledger_ext L155
def mass L165
theorem eq_zeroLedger_of_mass_zero L169
theorem exists_pos_of_ne_zero L182
def predOf L202
theorem postAt_predOf L210
theorem predOf_nonneg L256
theorem mass_predOf_lt L289
theorem postReachable_zero_of_nonneg L362
theorem imbalance_realized L397
structure does L416
abbrev Schedule L417
def runSchedule L420
def phiAfter L428
theorem runSchedule_eq_of_agree_below L432
theorem postReachable_run L445
theorem exists_schedule_of_reachable L458
theorem imbalance_realized_by_schedule L474
def incidenceImbalance L488
theorem dynamics_produces_incidence_countermodel L505
def CountsOnlyImbalance L537
def CountsOnlySchedule L549
def cmEdge0 L554
def cmEdge1 L557
theorem cmEdge1_ne_cmEdge0 L559
def countermodelSchedule L567
theorem schedule_countermodel_not_countsOnly L575
theorem about L606
theorem ledger_forces_countsOnly_at_no_layer L607
structure Index L621
def index L628
theorem index_audit L647