module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPosting`

Gap-2 module on non-equivariant posting: class masses, numerator masses, and the identity that the posted measure equals orbit cardinality times a Gibbs weight. Supplies the comparison sign on naturals and the algebraic mass calculus used when the posting layer is not forced to be gauge-equivariant. Downstream gluing, label-erasure, and hostile-probe modules import it as the posting-side mass layer.

claimOn the Gap-2 posting layer one works with a signed comparison $\mathrm{sgn}_{<}(x,y)\in\{-1,0,1\}$, additive class masses on posted weights, a numerator mass, and a total mass. The central relation is $\mu = |\mathrm{Orbit}|\cdot w_{\mathrm{Gibbs}}$ for the posted measure, without assuming equivariance of the posting map.

background

Gap 2 in the Seven Gaps gravity track asks how much structure the posting layer can carry beyond bare counting. The upstream floor module records the committed answer for Track A1.2: GaugeCountingPrinciple is not derived from richer substrate structure at posting; the pinned carrier, a uniqueness wall, and one unexcluded premise are separated cleanly.

This module sits on that floor and treats posting that need not be gauge-equivariant. It introduces a comparison sign on naturals written as a difference of indicators (so swap is a ring identity), then an additive class-mass calculus (zero, add, neg, one) and the masses of numerators and posted weights. The intended bridge to the path-sum measure is the orbit-card times Gibbs-weight factorization of $\mu$.

Notation is RS-native gravity bookkeeping: posted weights, orbit averages, and Gibbs factors at the posting layer, not yet the full gluing or label-erasure Jacobian.

proof idea

Definition-and-lemma layer, not a single theorem. Comparison sign is defined so that swap is immediate ring algebra; case analysis covers the three trichotomy branches. Class mass is shown to be a group homomorphism-style map (zero, add, neg, one). Posted-weight mass and numerator mass are specialized instances. The headline identity equates $\mu$ to orbit cardinality times the Gibbs weight, tying the non-equivariant posting data to the measure used downstream. No deep tactic proof: algebraic identities and direct unfolding of the mass definitions.

why it matters in Recognition Science

Feeds three Gap-2 consumers. Fugacity-posting gluing imports it when asking whether posting plus gluing force unit-sector fugacity; residual freedom there collapses to three positive constants and the unit-fugacity premise. Label erasure uses the posting mass layer so that $\mu$ is the pushforward of a local relabeling-invariant labeled weight, with $1/|\mathrm{Aut}|$ as erasure Jacobian and surviving freedom in the local numerator and three fugacities. The hostile-probe module runs adversarial checks (e.g. that the orbit-mean-one criterion is not vacuous) against this machinery.

In the broader RS gravity program this is scaffolding for Gap 2 of the seven-gap ledger: pinning what non-equivariant posting can and cannot force before gluing and gauge counting are imposed. It does not close flag 8; that waits on G1 and G2 jointly.

scope and limits

Does not derive GaugeCountingPrinciple from posting-layer substrate structure.
Does not force unit-sector fugacity or close the gluing residual to a unique measure.
Does not assert label-erasure completeness or move flag 8.
Does not claim posting is gauge-equivariant; the point is the non-equivariant case.
Does not supply the hostile-probe checks; those live in a separate non-build module.

used by (3)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityPostingGluing module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasure module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPostingHostileProbe module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2PostingLayerFloor module_import

declarations in this module (68)

def sgnLt L148
theorem sgnLt_swap L152
theorem sgnLt_cases L158
theorem classMass_zero L162
theorem classMass_add L168
theorem classMass_neg L175
theorem classMass_one L187
theorem there L199
def numeratorMass L206
class mass L210
theorem classMass_postedWeight L214
theorem mu_eq_orbitCard_mul_gibbsWeight L231
theorem posts_mu_iff_numeratorMass_eq_orbitCard L248
theorem orbitMeanOne_forces_one_of_invariant L270
def swap01 L301
theorem swap01_involutive L304
theorem swap01_trans_self L313
theorem swap01_apply_zero L316
theorem swap01_apply_one L321
def edgeRelabel L328
def twist L339
theorem twist_nE L341
theorem twist_edgeVerts L343
theorem twist_twist L348
def twistEquiv L354
theorem twistEquiv_apply L360
def twistRel L365
theorem twist_equivalent L374
theorem twist_class L376
theorem classMass_comp_twist L387
theorem classMass_of_twistOdd L398
def keyAt L417
theorem keyAt_of_lt L420
theorem keyAt_twist L426
theorem keyAt_twist_zero L439
theorem keyAt_twist_one L444
def edgeSign L452
theorem edgeSign_cases L455
theorem edgeSign_eq_zero_of_nE_le_one L467
theorem edgeSign_twist L474
def tiltedNumer L491
theorem tiltedNumer_pos L493
theorem tiltedNumer_twist L500
theorem tiltedNumer_eq_one_of_nE_le_one L506
def tiltedCost L514
theorem historyCost_tiltedCost L521
theorem exp_neg_historyCost_tiltedCost L534
theorem postedWeight_tiltedCost L538
theorem numeratorMass_tiltedCost L547
theorem tiltedCost_posts_mu L570
theorem keyAt_loopAndBridge_zero L581
theorem keyAt_loopAndBridge_one L583
theorem edgeSign_loopAndBridge L585
theorem tiltedNumer_loopAndBridge L592
theorem numerator_ne_one_at_loopAndBridge L598
theorem tiltedCost_not_equivariant L612
theorem postedWeight_tiltedCost_not_invariant L629
theorem normalizedAtTheAtoms_tiltedCost L646
theorem nonequivariant_cost_posts_mu_with_nonunit_numerator L661
theorem equivariance_is_load_bearing L680
theorem nonequivariant_posting_family L699
theorem family_injective_at_loopAndBridge L709
theorem nonequivariant_case_verdict L725
structure Index L758
def index L776
theorem index_nonequivariant_settled L785
theorem index_cost_layer_does_not_determine L787
theorem index_premise_still_open L790