module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2PostingLayerFloor`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (2)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPosting module_import
IndisputableMonolith.Gravity.SevenGaps.GaugeCountingInevitableReasons module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2DynamicsKindRule module_import

declarations in this module (17)

class mass L28
theorem canonical_count_eq_complex_count L94
theorem state_factored_weight_is_complex_function L108
theorem canonical_state_fiber_constant L120
theorem invariant_enrichment_unique_gibbs L144
theorem equivariant_cost_contributes_no_factor L156
def twoIsoVerts L176
def twoIsoVertsSwap L188
def vertexIndexCost L198
theorem vertexIndexCost_not_equivariant L208
structure the L220
theorem label_asymmetric_structure_exists L225
theorem irreducible_input_is_orbit_stabilizer L235
theorem posting_layer_floor L260
structure Index L284
def index L292
theorem index_audit L311