module module high

`IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerGenerated`

A letter cost is ledger-generated when each letter's charge depends only on that letter's own double-entry posting row (debits minus credits), with edges and top-cells fixed at null-row constants. The module formalizes this local predicate and proves that the recognition cost J meets it under explicit caps. Gravity Gap-2 workers cite it to pin C14 before gluing and J-diamond rank arguments. The development is definitional plus finite case checks on vertex charges.

claimA letter cost $c$ is ledger-generated if there is a fixed map $f$ from posting rows such that the charge on each letter $\ell$ equals $f$ of $\ell$'s own debit-minus-credit row, while edge and top-cell letters take constant null-row values. No orbit sums, isomorphism-class data, or global census enter $c$. In particular the recognition cost $J$ is ledger-generated on the stated finite caps.

background

Gap 2 in the gravity stack asks how gauge-counting and gluing arise without smuggling global census data into the cost. Upstream, Gap2JDiamondRank records that the recognition cost $J$ built from vertex-level ledger imbalance has no fixed kind totals, is not a valuation, and its moment vector lies outside the census span; the successor test is rank and consistency of J-diamonds (four-term inclusion-exclusion defects of $J$ on overlaps). Separately, Gap2GluingDerivation aims to derive the gluing law that earlier forced inverse factorials, rather than assume it.

This module pre-registers the C14 model: ledger generation. A letter's charge is a fixed function of that letter's own double-entry posting row only. Edges and top-cells carry constant null-row values. The sibling predicates LedgerGenerated / LedgerGeneratedAt and the vertex charge map for $J$ make that locality checkable. The hostile-probe sibling later attacks witness arithmetic and decoy discrimination against the same predicate.

proof idea

Definition module with supporting lemmas, not a single deep theorem. It introduces the ledger-generated predicate (global and at a configuration), the vertex charge extracted from a posting row, and a family of cap lemmas showing $J$ satisfies ledger generation on finite bounds (caps 1--3) together with decision forms and an equality form for cap 1. Arguments are direct unfolding of the posting-row map and case splits on letter kind (vertex versus null edge/top-cell), with no orbit or census machinery.

why it matters in Recognition Science

C14 is the locality gate for Gap 2: costs that secretly use global census or isomorphism-class data are ruled out before gluing derivation and J-diamond rank tests proceed. Downstream, Gap2LedgerGeneratedHostileProbe imports this module unchanged and adversarially checks that letterwise $J$ matches the quadratic vertex form $f_V(m)=m^2/(2\kappa)$ with null edges/tets, and that a census-based decoy fails the global predicate. Closing ledger generation keeps the forcing route aligned with double-entry locality rather than relocating the gap into hidden global data. In the broader RS gravity program this protects the claim that recognition cost structure, not an assumed gluing ansatz alone, drives the gauge-counting step.

scope and limits

Does not derive the gluing law or inverse-factorial gauge counts.
Does not prove J-diamond rank, consistency, or Ehrhart-span claims.
Does not treat infinite configurations beyond the stated finite caps.
Does not assert uniqueness of the posting-row charge map among all possible costs.
Does not incorporate orbit sums, isomorphism classes, or census data into the cost.

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerGeneratedHostileProbe module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2GluingDerivation module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondRank module_import

declarations in this module (72)

def LedgerGenerated L79
def LedgerGeneratedAt L90
theorem LedgerGenerated_implies_at L98
def jCostVertexCharge L109
theorem jCost_ledgerGenerated L115
theorem jCost_ledgerGenerated_cap1 L127
theorem jCost_ledgerGenerated_cap2 L131
theorem jCost_ledgerGenerated_cap3 L135
def jCost_ledgerGenerated_decision_cap1 L140
def jCost_ledgerGenerated_decision_cap2 L141
def jCost_ledgerGenerated_decision_cap3 L142
theorem jCost_ledgerGenerated_decision_cap1_eq L144
theorem jCost_ledgerGenerated_decision_cap2_eq L146
theorem jCost_ledgerGenerated_decision_cap3_eq L148
def censusVertexCost L158
theorem censusVertexCost_not_ledgerGenerated L166
theorem historyCost_jCost_one L184
def loop1Complex L190
theorem imbalanceSq_point L200
theorem imbalanceSq_edge L201
theorem imbalanceSq_path L202
theorem imbalanceSq_loop1 L203
theorem imbalanceSq_empty_cap1 L204
theorem imbalanceSq_edge_native L209
theorem imbalanceSq_path_native L210
theorem imbalanceSq_loop1_native L211
theorem imbalanceSq_loopPoint_native L212
theorem imbalanceSq_fork_native L214
theorem historyCost_jCost_one_edge L216
theorem historyCost_jCost_one_point L221
theorem historyCost_jCost_one_path L225
theorem historyCost_jCost_one_loopPoint L230
theorem historyCost_jCost_one_fork L234
theorem historyCost_loop1 L239
theorem historyCost_empty_cap1 L244
theorem historyCost_table_cap1 L251
def historyCost_identically_zero_decision_cap1 L257
theorem historyCost_identically_zero_decision_cap1_eq L258
theorem historyCost_not_identically_zero_cap2 L263
def historyCost_identically_zero_decision_cap2 L268
theorem historyCost_identically_zero_decision_cap2_eq L269
theorem historyCost_not_identically_zero_cap3 L273
def historyCost_identically_zero_decision_cap3 L282
theorem historyCost_identically_zero_decision_cap3_eq L283
def historyCostRational L294
theorem historyCostRational_edge L296
theorem historyCostRational_fork L298
theorem historyCostRational_zero L300
def historyCostSeedTable L304
theorem historyCostSeedTable_length L313
theorem historyCostSeedTable_edge_row L315
theorem historyCostSeedTable_edge_row_native L318
structure CapHistoryTally L323
def measuredHistoryCaps L329
theorem measured_cap1_zero L337
theorem measured_cap2_nonzero L341
theorem measured_cap3_nonzero L345
def C27TriggerAt L355
theorem edgeComplex_fits_cap2 L360
theorem edgeComplex_fits_cap3 L364
theorem C27_trigger_armed_cap2 L369
theorem C27_trigger_armed_cap3 L375
def C27_hard_stop_armed L381
theorem C27_hard_stop_armed_eq L382
theorem C27_not_armed_by_cap1_seeds L385
structure LedgerGeneratedVerdict L396
theorem ledgerGeneratedVerdict L413
structure LedgerGeneratedIndex L425
def ledgerGeneratedIndex L433
theorem index_c27_armed L441
theorem index_flag_unmoved L442
theorem index_jCost_true L443