IndisputableMonolith.Gravity.SevenGaps.GaugeCountingInevitableReasons

declarations in this module (78)

• structure ReasonStatus L101
• def reasonTable L107
• theorem reasonTable_length L127
• theorem R01_invariance_underdetermines L133
• theorem R02_gcp_iff_gaugeOrbitMass L139
• theorem R03_gaugeOrbitMass_satisfies L144
• theorem R04_uniform_fails L149
• theorem R05_pinned_count_is_complex L155
• theorem R06_pinned_weights_are_complex L160
• theorem R09_label_asymmetric_exists L167
• theorem R11_orbit_stabilizer L171
• theorem R07_invariant_enrichment_unique_gibbs L182
• theorem R08_equivariant_cost_no_factor L190
• theorem R10_indifference_family_underdetermines L202
• theorem R10_gcp_iff_unit_fugacity L211
• structure CorrectedFloorPlan L219
• def correctedFloorPlans L226
• theorem correctedFloorPlans_length L248
• structure CorrectedMeasurePremise L255
• def AssumedRequired L270
• def assumedTargetStatus L277
• def R01 L281
• def R02 L286
• def R03 L290
• def R04 L294
• def R05 L299
• def R06 L303
• def R07 L311
• def R08 L317
• def R09 L323
• def R10 L325
• def R11 L330
• def R12 L336
• def R13 L344
• def R14 L354
• def R15 L363
• def R16 L369
• def R17 L374
• def R18 L383
• theorem R01_reason L387
• theorem R02_reason L391
• theorem R03_reason L395
• theorem R04_reason L399
• theorem R05_reason L403
• theorem R06_reason L407
• theorem R07_reason L411
• theorem R08_reason L414
• theorem R09_reason L418
• theorem R10_reason L421
• theorem R11_reason L425
• theorem R12_refuted L429
• theorem R13_refuted L432
• theorem R14_refuted L436
• theorem R15_refuted L439
• theorem R16_refuted L442
• theorem R17_refuted L446
• theorem R18_rebooking_preserves_product L483
• def RebookingInvariant L507
• theorem R18_rebooking_invariant_admits_nonunit L516
• theorem R18_no_rebooking_invariant_selector L534
• def ProductVisible L553
• theorem R18_product_visible_is_rebooking_invariant L561
• theorem R18_no_product_visible_selector L580
• def R18Wall L593
• theorem R18_refuted L607
• theorem R18_vacuity_guard L618
• def R18Status L622
• def firstAttackBlock L626
• theorem firstAttackBlock_length L629
• def secondAttackBlock L640
• theorem secondAttackBlock_length L643
• def thirdAttackBlock L662
• theorem thirdAttackBlock_length L664
• def nextAttackBlock L668
• theorem nextAttackBlock_length L670
• theorem R18_block_certified L675
• def correctedFloorPlansStub L684
• theorem correctedFloorPlansStub_length L687