module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap2SizeBlindnessReach`

Establishes the reach of size-blindness for Gap 2: blindness to a feature set X forces size-blindness of every labeled weight exactly when X resolves no more than the three index counts. Introduces loopCount, an incidence invariant not fixed by those sizes, plus its disjoint-union and relabeling laws. Downstream posting-cost and inevitability modules cite it to rule out weaker sufficient premises of the blindness shape.

claimFor a complex $K$, let $\mathrm{loopCount}(K)$ be the number of edges whose two endpoints coincide. This is a function of the incidence data and is not a function of the three index sizes alone. Size-blindness of a labeled weight is forced by blindness to a feature set $X$ for every weight if and only if $X$ resolves no more structure than those three counts.

background

Gap 2 in the gravity stack concerns the gauge-counting principle $\nu = 1/|\mathrm{Aut}|$ for the physical mass class. Gap2GaugeVolume shows a gluing law forces the inverse factorial and hence gauge counting, but assumed the gluing law. The gluing-derivation line tries to derive that law rather than postulate it, following the 2026-07-28 adversarial panel route that needs a disjoint union on the carrier.

Premise (i) of that derivation is size-blindness of the labeled weight: the weight cannot see the three index sizes. A natural hope is a weaker premise of the form "the weight cannot distinguish complexes that agree on feature set $X$". This module studies when such $X$-blindness actually yields size-blindness.

The key witness is loopCount: edges with coinciding endpoints. It is built from incidence data, is invariant under relabeling, and adds under disjoint union, yet is not determined by the three index sizes. Proper edge counts and injection lemmas for left/right summand vertices support the disjoint-union calculus.

proof idea

Definition-and-lemma module, not a single theorem. It defines loopCount (and properEdgeCount) on the incidence presentation, proves loopCount equals a sum over edges of an endpoint-coincidence predicate, and establishes congruence under edgewise relabeling.

Invariance under the module's notion of complex isomorphism follows from the relabeling lemma. Disjoint-union identities use injectivity of the left/right vertex embeddings and the corresponding edge-vertex lemmas, yielding additivity of loopCount and the empty-complex base case. Those facts supply the counterexample structure: complexes agreeing on coarser $X$ can still differ in loopCount, so $X$-blindness need not imply size-blindness unless $X$ is no finer than the three counts.

why it matters in Recognition Science

Closes a premise-strength gap on the Gap 2 gluing route. Downstream Gap2PostingCostDerivation states the point directly: Gap2GluingDerivation assumes size-blindness, and this module shows no weaker premise of the form "weight cannot distinguish complexes agreeing on $X$" supplies it, because blindness to $X$ forces size-blindness for every weight exactly when $X$ resolves no more than the three counts. That rules out a weaker sufficient premise of this shape without claiming the two conditions are interchangeable.

GaugeCountingInevitableReasons imports the module into the necessary-reasons census for why richer RecognitionLedger / posting-layer structure would force the gauge-counting principle. Together with GaugeHistoryMeasure and Gap2GluingDerivation, it keeps the gluing-law derivation from silently relocating its assumptions.

scope and limits

Does not derive the gluing law or the gauge-counting principle itself.
Does not claim size-blindness and three-count blindness are interchangeable for every weight.
Does not supply a posting-cost derivation of premise (i); that is downstream.
Does not assert loopCount is the only size-sensitive incidence invariant.
Does not address physical mass spectra or Newtonian limits outside Gap 2 bookkeeping.

used by (2)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCostDerivation module_import
IndisputableMonolith.Gravity.SevenGaps.GaugeCountingInevitableReasons module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2GluingDerivation module_import
IndisputableMonolith.Gravity.SevenGaps.GaugeHistoryMeasure module_import

declarations in this module (94)

def loopCount L154
theorem loopCount_eq_sum L157
theorem loop_iff_of_relabel L165
theorem loopCount_congr L174
theorem loopCount_invariant L191
theorem inlV_inj L201
theorem inrV_inj L204
theorem dunion_edgeVerts_inl L207
theorem dunion_edgeVerts_inr L213
theorem loopCount_dunion L220
theorem loopCount_emptyComplex L245
def properEdgeCount L265
theorem properEdgeCount_eq_sum L268
theorem properEdgeCount_congr L274
theorem properEdgeCount_invariant L291
theorem inlV_eq_iff L296
theorem inrV_eq_iff L300
theorem properEdgeCount_dunion L305
theorem properEdgeCount_eq_zero_of_nV_le_one L327
theorem properEdgeCount_emptyComplex L338
structure AdditiveStat L349
def loopStat L358
def properStat L365
def statWeight L380
theorem gibbsWeight_positive L384
theorem statWeight_invariant L394
theorem statWeight_pos L399
theorem statWeight_emptyComplex L403
theorem classMass_statWeight L411
theorem statWeight_glues L452
theorem statWeight_glues_at_dust_edge L467
theorem also L483
theorem statWeight_not_gluesGenerally L486
def twoLoops L505
def twoBridges L516
theorem loopCount_twoLoops L526
theorem loopCount_twoBridges L528
theorem properEdgeCount_twoLoops L530
theorem properEdgeCount_twoBridges L532
theorem twoLoops_sizes L534
theorem twoBridges_sizes L537
theorem witnesses_same_sizes_different_loops L542
def SizeBlind L555
theorem sizeWeight_sizeBlind L559
theorem sq_ne_one_of_pos_ne_one L566
theorem loopEscape_not_sizeBlind L574
theorem properEscape_not_sizeBlind L590
def NormalizedAtTheAtoms L610
theorem gibbsWeight_eq_one_at_atoms L613
theorem properEscape_normalizedAtTheAtoms L623
theorem loopEscape_fails_the_atoms L635
theorem statWeight_sizeBlind_at_one L652
theorem loopEscape_sizeBlind_at_one L662
theorem properEscape_sizeBlind_at_one L666
def SatisfiesTheOtherHypotheses L684
theorem properEscape_satisfiesTheOtherHypotheses L695
theorem classMass_statWeight_at_one L706
theorem properEscape_classMass_ne_mu L715
theorem size_blindness_not_forced_by_the_other_hypotheses L756
def RespectsKinds L780
theorem postingAlphabet_equiv_iff_total L789
theorem sizes_le_of_respectsKinds L806
theorem exists_respectsKinds_iff_sizes L838
def AlphabetBlindSorted L855
theorem alphabetBlindSorted_iff_sizeBlind L860
theorem loopEscape_not_alphabetBlindSorted L870
def blob L884
def canonicalSizeFun L897
theorem sizeBlind_eq_sizeWeight L900
theorem sizeBlind_iff_exists_sizeFun L919
theorem premise_one_iff_alphabetBlind L936
def Invariant L963
def ResolvesNoMoreThanSizes L967
def BlindTo L972
theorem coarse_invariant_blindness_implies_sizeBlind L979
theorem fine_invariant_blindness_does_not_imply_sizeBlind L994
theorem invariant_coarse_or_fine L1031
theorem blindness_forces_premise_one_iff_coarse L1074
theorem indistinguishability_premises_never_weaken_premise_one L1088
def sizeStatInvariant L1115

… and 14 more