IndisputableMonolith.Gravity.SevenGaps.GaugeHistoryMeasure

declarations in this module (54)

• abbrev PostingAlphabet L81
• def balancedZeroState L85
• structure PostedBoundedHistory L98
• def vertexPost L107
• def edgePost L111
• def tetPost L115
• theorem vertexPost_injective L118
• theorem edgePost_injective L121
• theorem tetPost_injective L125
• def canonicalHistory L133
• structure CanonicalHistory L154
• abbrev toPosted L163
• def underlying L166
• def ofComplex L169
• theorem ext L173
• theorem toPosted_eq_canonicalHistory L178
• def classOf L183
• def fiber_unique L188
• def equivUnderlying L203
• instance instFinite L214
• theorem classOf_ofComplex L217
• theorem toPosted_ofComplex L221
• theorem underlying_ofComplex L225
• def postingAlphEquiv L234
• structure from L245
• structure HistoryRelabel L246
• def toRelabel L269
• def ofRelabel L279
• def historyRelabel_equiv_relabel L303
• def historyRelabel_equiv_relabel_canonical L317
• instance instFiniteHistoryRelabel L321
• def historyOrbitCardClass L329
• def historyPairCountClass L335
• structure GaugeHistoryEnrichment L342
• def nuBuild L348
• theorem nuBuild_def_history_only L356
• def history_class_equiv_mk L367
• def class_mk_equiv_orbit L379
• def history_class_equiv_orbit L394
• theorem historyOrbitCardClass_eq_orbitCardClass L399
• def history_pair_equiv_pair L417
• theorem historyPairCountClass_eq_pairCountClass L426
• theorem historyPairCountClass_pos L442
• theorem nuBuild_gaugeCounting L450
• theorem nuBuild_eq_gaugeOrbitMass L462
• theorem gap2_gauge_counting_from_history_discharged L474
• def TypedResidual_gap2_gauge_counting_from_history L483
• theorem typedResidual_gap2_gauge_counting_from_history_closed L490
• theorem TypedResidual_gap2_gauge_counting_from_history_closed L494
• def circularNu L504
• theorem circularNu_def_is_gaugeOrbitMass L508
• theorem circularNu_satisfies_gaugeCounting L514
• theorem decoy_uniformClassMass_not_gaugeCounting L520
• theorem gap2_history_measure_decoy_anchors L527