module module high

`IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure`

Defines the scoped configuration space for the recognition path sum: bounded combinatorial complexes (at most B vertices, edges, tetrahedra) with incidence data, finite coding, and the relabeling groupoid. Postulates the discrete-gravity measure μ(K)=1/|Aut K|. Gravity and QG campaign modules cite it as the common state space for quotient bookkeeping, gauge preflight, UV shell sums, and measure no-gos.

claimAt fixed lattice scale, a configuration is a bounded combinatorial complex $K$ with at most $B$ vertices, edges, and tetrahedra and abstract incidence data (equilateral CDT-style, no metric field). The module supplies a finite code equivalence, a positive cardinality bound, the relabeling relation (reflexive, symmetric, transitive), and the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut}(K)|$ on that space.

background

Recognition gravity treats the path sum as a sum over admissible triangulations of a compact manifold with mesh bounded below by the substrate length $\ell_{\mathrm{sub}}$. The upstream UV-bound module frames that sum and its finiteness; this module supplies the finite, combinatorial state space on which those sums are written.

The model drops continuous metric data: edge length is fixed at the minimum mesh, so geometries are equilateral and combinatorial (CDT-style), mirroring a size-capped, metric-free version of a 3D Regge triangulation. Sibling structure introduces BoundedComplex, empty complex, finite coding (toCode/ofCode equivalence), Fintype instance, positive card, and the Relabel groupoid (refl/symm/trans).

The path-sum weight is the standard discrete-gravity symmetry factor $\mu(K)=1/|\mathrm{Aut} K|$, postulated here and later derived or stress-tested by gauge-counting and invariance modules.

proof idea

Definition and infrastructure module, not a single theorem. It packages the bounded complex type, coding equivalence to a finite type (hence Fintype and card positivity), and the relabeling equivalence relation with its groupoid laws. The measure $\mu=1/|\mathrm{Aut}|$ is introduced by definition as the scoped path-sum weight. Downstream proofs import these objects rather than re-deriving finiteness or incidence shape.

why it matters in Recognition Science

This is the shared configuration layer for the Seven-Gaps QG campaign. CampaignLedger records scoped increments against it. ClassPushforward uses the space for quotient bookkeeping of the path sum $Z$. ExactShellGaugePreflight derives $\mu=1/|\mathrm{Aut}|$ from pure gauge counting (this module only postulates it). ExactShellGaugeUV organizes quotient classes into exact complexity shells and proves Gaussian-UV convergence. MeasureInvarianceNoGo kills the claim that relabeling invariance alone forces $\mu=1/|\mathrm{Aut}|$, with explicit witnesses on this space. PathSumProbes and SimplicialClass attach honest probes and simplicial class structure. Without a finite, relabel-aware complex type, the path-sum UV and measure lanes have nowhere to land.

scope and limits

Does not derive μ=1/|Aut| from gauge counting; that is ExactShellGaugePreflight.
Does not prove UV convergence or shell resummation; ExactShellGaugeUV owns that.
Does not claim continuum or physical closure of any QG gap flag.
Does not include a dynamical metric field; complexes are equilateral and combinatorial only.
Does not assert that relabeling invariance uniquely fixes the measure.

used by (7)

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

IndisputableMonolith.Gravity.SevenGaps.CampaignLedger module_import
IndisputableMonolith.Gravity.SevenGaps.ClassPushforward module_import
IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugePreflight module_import
IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugeUV module_import
IndisputableMonolith.Gravity.SevenGaps.MeasureInvarianceNoGo module_import
IndisputableMonolith.Gravity.SevenGaps.PathSumProbes module_import
IndisputableMonolith.Gravity.SevenGaps.SimplicialClass module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.PathSumUVBound module_import

declarations in this module (56)

structure BoundedComplex L81
def emptyComplex L92
abbrev CodeType L115
def toCode L120
def ofCode L125
def codeEquiv L137
instance instFintypeBoundedComplex L146
theorem boundedComplex_card_pos L150
structure Relabel L157
def refl L171
def symm L179
def trans L193
theorem refl_vEquiv L203
theorem symm_vEquiv L205
theorem symm_eEquiv L207
theorem symm_tEquiv L209
theorem trans_vEquiv L212
theorem trans_eEquiv L215
theorem trans_tEquiv L218
def toEquivTriple L223
theorem toEquivTriple_injective L229
theorem ext L240
def Equivalent L251
def relabelSetoid L257
abbrev TriangulationClass L266
theorem triangulationClass_finite L270
theorem classCount_le_labeledCount L276
theorem labeledCount_eq_card L282
abbrev Aut L290
instance instFiniteAut L297
theorem autCard_pos L301
def mu L307
theorem mu_pos L311
theorem mu_le_one L318
theorem mu_congr L348
def Z L362
theorem Z_norm_le_muSum L367
theorem Z_norm_le_card L381
theorem Z_relabel_invariant L400
theorem summand_class_constant L415
def unitaryWeight L427
theorem unitaryWeight_norm L432
theorem zRS_scoped_wellDefined L444
def provedFamily L464
theorem provedFamily_growthBase_derived L473
theorem proved_count_le_structural_bound L479
structure GapStatus L493
def pathSumMeasureStatus L504
theorem status_count_finite L514
theorem status_quotient_finite L515
theorem status_measure_defined L516
theorem status_measure_positive L517
theorem status_modulus_bound L518
theorem status_relabel_invariance L519
theorem status_continuum_open L521
theorem status_substrate_measure_open L523