IndisputableMonolith.Gravity.SevenGaps.Gap2PostingLayerFloor
Pinned bounded histories at bound B equal bounded complexes at B in number: with state fixed to the balanced zero state, each counted history is exactly one complex, and dual-entry enrichment multiplies the count by one. The module also sets the Gap 2 posting-layer floor, with equivariant costs contributing no factor and an explicit non-equivariant vertex-index cost. Gravity and ledger-measure authors cite it for counts-only and equivariance boundaries. Proofs are algebraic identities and fiber constancy on canonical histories.
claimAfter the design pin $\mathrm{state}=\mathrm{balancedZeroState}$, the number of pinned bounded histories of bound $B$ equals the number of bounded complexes of bound $B$. Dual-entry enrichment contributes factor $1$. Equivariant letter costs contribute no Boltzmann factor. The module exhibits a non-equivariant cost on two isomorphic vertices (vertex-index cost) and records uniqueness of invariant Gibbs enrichments on the posting layer.
background
Gap 2 asks whether the Recognition Ledger measure on physical mass is forced to the gauge-counting form $\nu=1/|\mathrm{Aut}|$. Earlier arcs reduced the weight to size-blind when cost is kind-only, kind-only when charge is counts-only, and counts-only when lattice imbalance and magnitude are. None of those premises is forced at its own layer; the successor layer is the ledger dynamics: the posting rules that produce states.
This module sits at that posting-layer floor. It works with canonical histories whose state is pinned to the balanced zero state, not unpinned posted bounded histories that still carry a free state. Complexes are the combinatorial skeletons of those histories; dual-entry enrichment is the ledger bookkeeping that pairs opposite postings.
Upstream, Gap2DynamicsKindRule frames the question: do the posting dynamics force the counts-only premise? The present module answers a counting half of that question and supplies the non-equivariant witness class used later.
proof idea
The spine is equinumerosity: after the state pin, a canonical history is determined by its complex, so the two finite sets at bound $B$ are in bijection and dual-entry enrichment is count-neutral. Supporting lemmas give fiber constancy of the canonical state, descent of state-factored weights to complex functions, and uniqueness of invariant Gibbs enrichment on the fiber.
A separate block treats letter costs: any equivariant cost contributes no multiplicative factor to the posted measure (Boltzmann numerator identically one on orbits). The module then builds an explicit counter-model to equivariance, vertex-index cost on a two-vertex isomorphic pair, and proves it is not equivariant. Existence of a label-asymmetric structure seeds the non-equivariant case.
why it matters in Recognition Science
Downstream, Gap2NonEquivariantPosting quotes this module's non-equivariant class: the equivariant posting-cost route closes only when the Boltzmann numerator is identically one, and its docstring defers the unsettled case to the vertex-index cost exhibited here. Without that witness, the non-equivariant branch of Gap 2 has no concrete carrier.
GaugeCountingInevitableReasons imports the module into the necessary-reasons census for the Gap-2 measure target: richer posting-layer structure forcing the gauge-counting principle on physical mass. Counting equality (pinned histories equal complexes) and the equivariant-cost null-factor fact are proved reasons that census lists; the non-equivariant example marks where a reason fails or must be replaced.
In the Seven Gaps gravity program this is floor-setting, not the final measure theorem: it clears the pinned-counting identity and draws the equivariant/non-equivariant boundary at the posting layer.
scope and limits
- Does not treat unpinned posted histories; free state stays outside the equinumerosity.
- Does not force counts-only dynamics; only equates pinned counts to complex counts.
- Does not decide the measure for non-equivariant letter costs; only exhibits the class.
- Does not derive the Gap-2 gauge-counting principle; supplies floor facts for later census.
- Does not claim every letter cost is equivariant; vertex-index cost is a counterexample.
used by (2)
depends on (1)
declarations in this module (17)
-
class
mass -
theorem
canonical_count_eq_complex_count -
theorem
state_factored_weight_is_complex_function -
theorem
canonical_state_fiber_constant -
theorem
invariant_enrichment_unique_gibbs -
theorem
equivariant_cost_contributes_no_factor -
def
twoIsoVerts -
def
twoIsoVertsSwap -
def
vertexIndexCost -
theorem
vertexIndexCost_not_equivariant -
structure
the -
theorem
label_asymmetric_structure_exists -
theorem
irreducible_input_is_orbit_stabilizer -
theorem
posting_layer_floor -
structure
Index -
def
index -
theorem
index_audit