module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasureHostileProbe`

Hostile audit of Gap 2 label-erasure: class mass is definitionally a fibre sum over labels, with no automorphism factor in the measure. It checks that push and edge-commutation preserve ordered incidence, records orbit-stabilizer as proved, and runs small-complex counts (path plus isolated vertex; two-edge complex). Cite when verifying that the erasure Jacobian story does not smuggle an Aut denominator into the mass.

claimThe class mass of a combinatorial type is the fibre sum of the labeled weight over the preimage of that type under the forgetful map; it carries no $1/|\mathrm{Aut}|$ factor. Pushforward along local relabeling preserves ordered incidence, edge commutation is ordered, and the orbit-stabilizer identity holds on the finite complexes used as probes (path plus isolated vertex; two-edge complex).

background

Gap 2 sits in the gravity seven-gaps ledger. Upstream Gap2LabelErasure states the scoped headline: $\mu$ is the pushforward of a local relabeling-invariant labeled weight; $1/|\mathrm{Aut}|$ is the erasure Jacobian; surviving freedom is the local numerator and three fugacities. That module does not close flag 8.

Gap2JEhrhartSpan tests fixing the three rates by reading recognition cost $J$ from ledger imbalance structure after aggregate linearity by kind (FixedKindTotals) left the rates free under posting-plus-gluing.

This probe module interrogates whether class mass is really a plain fibre sum (no hidden Aut factor), and whether the incidence and counting lemmas needed for that reading hold on minimal complexes.

proof idea

Definitional and small-case audit, not a single theorem. One lemma asserts that classMass is definitionally the fibre sum (inspectable by #print), with no Aut factor. Separate lemmas show push preserves ordered incidence and that relabel edge-commutation is ordered. Orbit-stabilizer is recorded as proved, with an explicit corollary factor. Concrete probes: path-plus-isolated and two-edge complexes, with count identities and edge-commutation OK certificates, plus elementary evaluation lemmas on those complexes.

why it matters in Recognition Science

Keeps the Gap 2 / A18 label-erasure lane honest: if class mass silently included $1/|\mathrm{Aut}|$, the erasure Jacobian and the three-fugacity residual freedom would be double-counted or mis-normalized. Feeds the C2 census-span / $J$-from-imbalance route in Gap2JEhrhartSpan by confirming the mass side has no Aut contamination. No downstream modules import it yet; it is a gate check before flag-8 motion, which still requires G1$\wedge$G2 PASS plus later steps. Lands in the gravity domain of the seven-gaps program rather than the T0–T8 forcing chain directly.

scope and limits

Does not close flag 8 or assert G1∧G2 PASS.
Does not derive the three fugacity rates or the full $J$-cost of a letter.
Does not prove label erasure for arbitrary complexes beyond the named probes.
Does not introduce a new measure; it audits the existing class-mass definition.
Does not claim Aut is absent from the Jacobian story, only from class mass.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasure module_import

declarations in this module (30)

theorem g1_hyp_defs_avoid_aut L30
theorem push_preserves_ordered_incidence L42
theorem relabel_edge_comm_is_ordered L48
theorem classMass_def_is_fibre_sum L56
theorem orbit_stabilizer_is_proved L64
theorem corollary_factor_explicit L69
def pathPlusIsolated L83
theorem pathPlusIsolated_counts L93
theorem twoEdgeComplex_counts L97
def edgeCommOK L101
def twoEdgeEV L105
def pathPlusEV L108
def twoEdgeAutCount L111
def pathPlusAutCount L115
theorem twoEdge_autCount_eq_two L120
theorem pathPlus_autCount_eq_one L123
def twoEdgeSwapV L126
theorem twoEdge_component_swap_ok L129
theorem twoEdge_id_ok L134
theorem twoEdge_edge_flip_fails_comm L139
theorem enumerated_mu_ratio_is_half L144
theorem dust_aut_arithmetic L149
theorem pathPlus_aut_inhabited L156
theorem locallyAdditive_is_explicit L161
theorem uniform_quantifies_all_Q L165
theorem relabelInvariant_inhabited_constant L176
theorem relabelInvariant_inhabited_equivariant_numerator L180
theorem dust_twin_admissible_real L185
theorem wreath_proved_not_assumed L190
theorem flag_still_false L195