module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasure`

Defines labeled weights on serially named bounded complexes and the erasure map that forgets serial labels. Relabel-invariant weights push forward to class functions, with the Gibbs weight recovered as the erasure Jacobian (gauge divisor). Gap-2 gravity workers use it to separate combinatorial gauge counting from letter costs before fugacity elimination. The module is mostly definitions plus algebraic identities linking rename, erase, and the pushforward.

claimA labeled weight is a real function on serially named bounded complexes with no built-in Gibbs factor. Renaming acts on serial labels; relabel-invariance means the weight is unchanged under every rename. Erasure forgets labels and pushes the weight to a class function. For relabel-invariant weights the pushforward equals the original weight times a gauge-counting Jacobian, identified with the Gibbs weight, so the class mass factors as $\mu = w_{\mathrm{Gibbs}}\cdot(\mathrm{erase}_\ast 1)$ on the relevant atoms.

background

Gap 2 in the Seven Gaps gravity lane asks how the measure on bounded complexes acquires its gauge-counting (inverse-factorial) factor without smuggling a gluing law or an equivariant posting cost. Upstream, the gluing-derivation module tries to obtain the gluing law from a disjoint-union carrier rather than assume it; the non-equivariant posting module isolates letter costs that are not Aut-equivariant and therefore escape the equivariant posting-cost closure.

This module supplies the intermediate language: a labeled weight is simply a real function of serially named complexes, definitionally free of any Gibbs factor. Rename acts by permuting serial names; RelabelInvariant is the fixed-point property under all renames. Erasure drops names and induces a pushforward on weights. The intended reading is that combinatorial overcounting lives entirely in the fibres of erasure, while dynamical letter costs live in the labeled layer.

The local setting is therefore pre-measure bookkeeping on named complexes, prior to collapsing sector fugacities or invoking a full gluing axiom.

proof idea

Definition block first: labeled weight, rename action, RelabelInvariant predicate, erase, and erasePush. Algebraic lemmas then identify rename with a push along the rename map and show that relabel-invariance implies the weight factors through erasure as a class function. Special cases record that the constant-one weight and the Boltzmann numerator exp(-historyCost) are relabel-invariant when the cost is name-blind.

The load-bearing identities equate the pushforward of a labeled weight to a gauge-divisor expression, factor the class mass as Gibbs weight times erasePush of one, and name the Gibbs weight as the erasure Jacobian. No deep analysis is required: the arguments are definitional unfolding and transport along the rename/erase diagram.

why it matters in Recognition Science

Closes the C4 erasure-Jacobian step that Gap-2 fugacity elimination quotes as already in hand: after that Jacobian, any letter cost whose posted class mass equals mu on the three atoms and is representable by a size-blind weight forces unit fugacity, collapsing the three sector fugacities on the gluing-residue family. Downstream fugacity elimination therefore imports this module as the source of the Jacobian identity rather than re-deriving gauge counting.

The hostile-probe module also imports it to stress-test G1 dependency, definitional collapse, directed-Aut fibre counts, and vacuity. Within the broader RS gravity program the module keeps combinatorial gauge volume cleanly factored from dynamical costs, which is the separation the adversarial panel route needs before a derived gluing law can force the inverse-factorial gauge principle.

scope and limits

Does not derive the gluing law or discharge Gap2GluingDerivation obligations.
Does not settle non-equivariant posting costs or force numerator-one for arbitrary letter costs.
Does not prove unit fugacity or eliminate sector fugacities; that is downstream.
Does not assert physical uniqueness of mu beyond the algebraic pushforward identities.
Does not recompute Aut fibre counts; hostile probes live in a separate module.

used by (2)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityElimination module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasureHostileProbe module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2GluingDerivation module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPosting module_import

declarations in this module (23)

abbrev labeledWeight L69
def rename L74
def RelabelInvariant L82
def erase L88
def erasePush L92
theorem rename_eq_push L98
theorem relabelInvariant_implies_classFun L104
theorem relabelInvariant_one L116
theorem relabelInvariant_exp_neg_history L120
theorem pushforward_labeledWeight_eq_gauge_divisor L133
theorem mu_eq_gibbs_mul_erasePush_one L161
theorem gibbsWeight_is_the_erasure_jacobian L176
theorem dust_twin_admissible L196
theorem autCard_dust_twin L203
theorem autCard_dust_twin_ne_square L210
def LocallyAdditive L221
theorem no_local_additive_cost_realizes_log_aut L228
theorem uniform_is_not_a_local_pushforward L253
structure LabelErasureIndex L289
def labelErasureIndex L297
theorem index_d1 L302
theorem index_d2 L303
theorem index_flag_unmoved L306