module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap2PoissonCoarea`

Defines tet-free, serially named cell complexes at a fixed cap B as the bare state space for the first C16 kill test in Gap 2. No automorphism, orbit, or gauge quotient is built in. Gravity measure work cites it as the combinatorial substrate on which posting moves, arrival counts, and erasure weights act. The module is definitional scaffolding: named types and bookkeeping lemmas, not a closed theorem.

claimAt cap $B$, the state space consists of tet-free serially named complexes (no Aut/orbit/gauge). On that space one tracks unused vertices, posted vertices and edges, LIFO unpost maxima, move rates, sort-respecting arrival counts, and order-erasure weights, with dimension bookkeeping $n_V$ and $n_E$ after each post.

background

Gap 2 in the gravity stack aims to fix the three free rates left by posting-plus-gluing. Upstream, Gap2JEhrhartSpan sets the route: define recognition cost $J$ of a letter from the ledger's imbalance structure and read rates off a census span test, after aggregate linearity by kind (FixedKindTotals) has already reduced the measure.

This module supplies the combinatorial arena for the C16 process-side test. A tet-free serially named complex at cap $B$ is a finite named cell complex with no tetrahedral cells and with serial naming of cells; the definition deliberately omits automorphism, orbit, and gauge structure so that discrimination can be stated on raw named data.

Sibling constructions record the LIFO posting dynamics on that space: which vertices remain unused, how vertices and edges are posted or unposted at the current maximum, the instantaneous move rate, sort-respecting arrival counts, and the order-erasure weight that will feed the Jacobian side of the measure.

proof idea

This is a definition module with supporting bookkeeping lemmas, not a single closed proof. It introduces the tet-free named-complex type and empty initial state, then defines the posting and unposting operations on vertices and edges, the move-rate and arrival-count functionals, and the order-erasure weight. Small lemmas relate posted vertex and edge counts to $n_V$ and $n_E$. No Aut quotient or gauge identification is proved or assumed here.

why it matters in Recognition Science

Downstream, Gap2MeasureDerivation assembles the measure-substrate blocker for the class mass of the Gibbs weight from the C4 erasure Jacobian and C17 fugacity elimination, naming the C16 LIFO process as the process-side discrimination premise. This module is the named state space on which that LIFO process runs.

In the Gap 2 chain it sits after the $J$-from-imbalance and Ehrhart-span setup and before the assembled measure derivation. It keeps the C16 kill test honest: rates and erasure weights are computed on bare tet-free named complexes, so any later gauge or orbit counting must be added explicitly rather than smuggled into the state type. It does not itself flip the measure flag; that remains deferred in the assembly module.

scope and limits

Does not quotient by Aut, orbits, or gauge; state space is bare named complexes.
Does not prove the C16 kill or fix the three posting rates.
Does not derive the Gibbs class mass or flip the measure-substrate flag.
Does not import or depend on FullTheoryLedger.
Does not assert Poisson or coarea identities as theorems; it only stages the named complex substrate.

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureDerivation module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan module_import

declarations in this module (82)

structure TetFree L69
def emptyTF L77
def vertexUnused L85
def postVertex L89
def unpostMaxVertex L100
def postEdge L121
def unpostMaxEdge L134
def moveRate L145
def sortRespectingArrivalCount L149
def orderErasureWeight L155
theorem postVertex_nV L162
theorem postEdge_nE L165
theorem unpostMaxEdge_nE L168
theorem postEdge_unpost_nE L172
theorem moveRate_symm_lifo_vertex L180
theorem moveRate_symm_lifo_edge L185
def uniformNamed L191
theorem uniform_detailed_balance_of_rate_symm L199
theorem moveRate_symm L208
theorem uniform_detailed_balance L211
structure Cap3Tally L229
def measuredCap3 L243
theorem measuredCap3_nStates L256
theorem measuredCap3_irreducible L257
theorem measuredCap3_symmetric L260
theorem measuredCap3_pi L261
theorem measuredCap3_small_ge L263
theorem measuredCap3_decoy L267
theorem measuredCap3_sj_decoy L268
theorem cap3_stationary_is_uniform L273
def pathPlusIsolated L289
theorem pathPlusIsolated_counts L299
theorem twoEdge_counts L303
def edgeCommOK L310
def twoEdgeEV L314
def pathPlusEV L317
def twoEdgeAutCount L321
def pathPlusAutCount L326
theorem twoEdge_autCount_eq_two L330
theorem pathPlus_autCount_eq_one L331
def inFibre L335
def twoEdgeFibre L340
def pathPlusFibre L345
theorem twoEdge_fibre_card L350
theorem pathPlus_fibre_card L353
abbrev NamedPi L365
def classMassPi L368
def uniformPi L373
theorem classMassPi_of_uniform L377
def classMassRatioPi L385
def UniformNamedPremise L395
theorem classMassRatioPi_of_uniform_eq_fibre_ratio L399
theorem classMassRatioPi_of_uniform_eq_half L415
def classMassRatio_420 L424
theorem classMassRatio_420_eq_half L427
theorem autInverseRatio_eq_half L432
theorem fibre_ratio_eq_aut_inverse_ratio L439
def SJ_twoEdge L447
def SJ_pathPlus L448
theorem SJ_twoEdge_rfl L450
theorem SJ_pathPlus_rfl L451
def predictedRatio_qSJ L455
theorem predictedRatio_qSJ_at_one L458
theorem predictedRatio_qSJ_at_two L461
def residualOverHalf L467
theorem residualOverHalf_eq_one L470
theorem deltaCounts_zero L475
theorem residual_family_silent L488
theorem arrivalCount_420 L501
theorem twoEdge_fibre_eq_orders_div_aut L505
theorem pathPlus_fibre_eq_orders_div_aut L511
theorem coarea_at_twoEdge L519
theorem coarea_at_pathPlus L526
structure PoissonCoareaIndex L535
def poissonCoareaIndex L551
theorem index_firewall L560
theorem index_cap3 L561
theorem index_ratio L562
theorem index_residual L563
theorem index_coarea L564

… and 2 more