module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2LabelInsertionDynamics`

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.GaugeCountingInevitableReasons module_import
IndisputableMonolith.Gravity.SevenGaps.InsertionAsymmetryInevitableReasons module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2GluingLawStationarity module_import

declarations in this module (30)

structure ReasonStatus L65
def reasonTable L71
theorem reasonTable_length L82
structure BirthDeathRates L90
def DetailedBalance L97
theorem D01_balance_ratio L102
theorem D01_balance_of_scaled_death L110
def equalPerSlotRates L131
def constantWeight L140
theorem constantWeight_detailedBalance_equalPerSlot L142
theorem D02_equal_per_slot_balances_constant L148
theorem D03_equal_per_slot_fails_insertionStationarity L156
def sizeBlindBirthPerLabelDeath L170
theorem D04_asymmetric_rates_force_insertionStationarity L178
theorem D04_factorial_is_stationary L194
def bakedFromWeight L212
theorem bakedFromWeight_balances L224
theorem D06_baked_rates_are_not_a_derivation L234
theorem D05_geometry_inhabited L245
structure CorrectedFloorPlan L248
def correctedFloorPlans L254
theorem correctedFloorPlans_length L264
structure CorrectedInsertionDynamicsResidual L270
def assumedTargetStatus L280
def firstAttackBlock L282
theorem firstAttackBlock_length L285
def D04_asymmetric_rates_give_kernel L290
theorem D04_asymmetric_rates_give_gcp L297
theorem gap2_measure_derived_unmoved L306
theorem labelInsertionDynamics_certified L312