module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCostDerivation`

Derives the class measure on labeled complexes from a posted, kind-only letter cost normalized at the atoms, without a gluing premise. Size-blindness follows from invariance of posting weights under the sort-respecting alphabet gauge, identified with the existing sector group. Gap-2 gravity work cites this for aggregate linearity by kind and for isolating the residual kind clause. The development is definitional setup plus short invariance and normalization lemmas.

claimThe posting alphabet admits a sort-respecting gauge group $G$ (independent relabelings of the vertex, edge, and tetrahedron blocks), identical to the sector group of the labeling. A letter cost depending only on kind, posted and normalized at the atoms, induces history costs and positive posted weights invariant under $G$. The induced class measure is size-blind and aggregate-linear by kind: the total charge of each kind equals a fixed rate times that kind's count. The three kind rates remain free at this layer; the substrate kind rule is not forced here.

background

Gap 2 in the SevenGaps gravity chain asks what forces the class measure on labeled complexes. Upstream, Gap2SizeBlindnessReach records that the gluing derivation needs two premises plus normalizations: (i) size-blindness (labeled weight depends only on the three index sizes) and (ii) gluing multiplicativity (class mass multiplies over disjoint unions where automorphism counts multiply). That module also explains why the posting layer alone cannot close the gap.

This module works at the posting layer. The alphabet has three blocks (vertices, edges, tetrahedra). The sort-respecting gauge is the product of their independent relabelings; it is identified with the sector group already studied in the gauge-volume development, whose content is the bijection with (target, witness) pairs out of $K$, not a bare product of symmetric groups. Letter cost assigns a real per letter; history cost sums along a history; posted weight is the corresponding positive Boltzmann-style weight. Equivariance means these quantities are invariant under the gauge. Kind rates package the three free reals, one per combinatorial kind.

proof idea

Mostly definitional scaffolding with short invariance proofs, not a single deep theorem. The alphabet gauge is introduced and equated to the sector group so no new group is claimed. Cardinality and Gibbs-weight lemmas tie the gauge order to uniform alphabet weights. History cost and posted weight are built from letter cost; positivity of posted weight is immediate for real costs. When cost depends only on kind, blockwise relabeling gives gauge invariance of history cost and posted weight. From a kind-only posted cost normalized at the atoms one obtains size-blindness (premise (i)) and the measure in aggregate-linear-by-kind form, with no gluing hypothesis. Whether the substrate forces the kind rule is left open (incidence_silence_derived false).

why it matters in Recognition Science

Downstream, the J-Ehrhart span module takes the aggregate-linearity reduction and tests whether recognition cost $J$ read from ledger imbalance can fix the three free rates via a census span test. The kind-rule module attacks the residual left open here: whether a letter's cost is forced to depend only on its kind, with the same three reals at every complex. Together they continue the Gap 2 arc after the size-blindness reach analysis and the fugacity-posting-gluing work (which showed posting plus gluing leave the rates free).

In the Recognition gravity program this is the posting-cost derivation step that isolates FixedKindTotals-style aggregate linearity and cleanly flags what remains for the kind rule and $J$-based rate fixing. No forcing-chain landmark (T0–T8), RCL identity, or numerical constant band is discharged; the contribution is local to the ledger/posting measure on complexes.

scope and limits

Does not force the three kind rates; they stay free parameters at this layer.
Does not prove the kind rule from the substrate (incidence silence left underived).
Does not assume or discharge gluing multiplicativity.
Does not introduce a new gauge group; the alphabet gauge equals the sector group.
Does not derive numerical gravity constants, alpha, or the mass ladder.

used by (2)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2KindRule module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2SizeBlindnessReach module_import

declarations in this module (98)

abbrev AlphabetGauge L222
theorem alphabetGauge_eq_sectorGroup L227
theorem card_alphabetGauge L230
theorem gibbsWeight_eq_inv_card_alphabetGauge L238
def LetterCost L249
def historyCost L255
def postedWeight L260
theorem postedWeight_pos L263
def Equivariant L270
theorem historyCost_invariant L276
theorem postedWeight_invariant L282
def KindRates L292
def KindOnly L303
theorem historyCost_of_kindRates L309
theorem kindOnly_equivariant L330
theorem postedWeight_sizeBlind L344
theorem posting_cost_derives_premise_one L354
theorem linearCost_atoms_force_zero L365
theorem kindRates_atoms_force_zero L400
theorem posting_cost_derives_gibbs L407
theorem classMass_gibbsWeight_eq_mu L418
theorem posting_cost_derives_mu L437
def PostedBy L458
theorem postedBy_postedWeight L462
theorem postedBy_eq_postedWeight L468
theorem measure_from_posting_premises L492
def CostSizeBlind L511
theorem postedWeight_sizeBlind_iff L518
theorem kindOnly_costSizeBlind L539
def squareCost L547
theorem historyCost_squareCost L552
theorem costSizeBlind_not_kindOnly L565
def pairCost L598
theorem historyCost_pairCost L603
theorem costSizeBlind_and_atoms_do_not_give_gibbs L620
def zeroCost L658
theorem zeroCost_kindRates L660
theorem zeroCost_kindOnly L663
theorem postedWeight_zeroCost L666
theorem zeroCost_normalizedAtTheAtoms L671
theorem posting_premises_satisfiable L678
def incidenceCost L690
theorem incidenceCost_inl L696
theorem incidenceCost_edge L699
theorem incidenceCost_tet L703
theorem historyCost_incidenceCost L709
theorem postedWeight_incidenceCost L725
theorem postedWeight_incidenceCost_eq L738
theorem exp_neg_pos L743
theorem exp_neg_ne_one L745
theorem that L753
theorem incidenceCost_equivariant L755
theorem twoBridges_edges_proper L765
theorem twoLoops_edges_loop L769
theorem incidenceCost_not_kindOnly L775
theorem incidencePosting_not_sizeBlind L787
theorem incidencePosting_satisfiesTheOtherHypotheses L796
theorem incidencePosting_classMass_ne_mu L802
theorem incidence_silence_suffices_and_equivariance_does_not L841
theorem equivariance_does_not_give_kindOnly L869
theorem sizeBlind_not_always_posted L890
theorem kindOnly_and_atoms_force_zeroCost L989
theorem card_postingAlphabet L1001
theorem card_alphabetGauge_pos L1005
theorem postedBy_constrains_only_the_empty_complex L1022
def KindTotalRates L1051
def FixedKindTotals L1058
theorem historyCost_of_kindTotalRates L1060
theorem kindRates_kindTotalRates L1069
theorem kindOnly_fixedKindTotals L1085
theorem fixedKindTotals_costSizeBlind L1089
theorem measure_from_fixedKindTotals L1098
def centeredIncidenceCost L1124
theorem centeredIncidenceCost_inl L1132
theorem centeredIncidenceCost_edge L1135
theorem centeredIncidenceCost_tet L1140
theorem edgeSum_centeredIncidenceCost L1145
theorem historyCost_centeredIncidenceCost L1160
theorem postedWeight_centeredIncidenceCost L1169
theorem centeredIncidenceCost_equivariant L1176

… and 18 more