module module

`IndisputableMonolith.Gravity.SevenGaps.InsertionAsymmetryInevitableReasons`

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

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2DynamicsKindRule module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2GaugeVolume module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2GluingLawStationarity module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2LabelInsertionDynamics module_import
IndisputableMonolith.Gravity.SevenGaps.MeasureInvarianceNoGo module_import

declarations in this module (114)

def CountingEquivalentRates L97
def RecognitionRateAsymmetry L104
def AssumedRequired L114
def D01 L119
def D02 L125
def D03 L129
def D04 L135
def D05 L141
def D06 L144
def D07 L151
def D08 L160
def D09 L167
def D10 L173
def D11 L176
structure PostingRatedWorld L182
def RatedWorldReachable L187
def RespectsPresentDynamics L194
def D12 L203
structure D13_CarrierEnlargingRateSensitiveDynamics L215
structure ReasonStatus L227
def reasonTable L233
theorem reasonTable_length L252
theorem D01_theorem L257
theorem D02_theorem L261
theorem D03_refuted L264
theorem D04_theorem L267
theorem D05_theorem L271
theorem D06_refuted L274
theorem D07_refuted L277
theorem D08_refuted L280
theorem D09_refuted L283
theorem equalPerSlotRates_not_namedLaw L291
theorem equalPerSlotRates_not_countingEquivalent L300
theorem factorialWorld_weight_pos L307
theorem factorialWorld_weight_ratio L313
theorem bakedFromWeight_factorial_satisfies_counting_law L328
theorem sizeBlindBirthPerLabelDeath_named_law L341
theorem sizeBlind_satisfies_counting_law L349
theorem sizeBlindBirthPerLabelDeath_ne_bakedFromWeight L356
theorem recognitionRateAsymmetry_derived L368
theorem D10_theorem L372
theorem countingLaw_balances_factorialWorld L380
theorem D11_theorem L399
theorem ratedWorldReachable_blind_to_rates L420
theorem D12_refuted L434
theorem recognition_presently_typed_cannot_select_asymmetry L443
def carrierStepWeight L484
def FactorsThroughKernel L491
def kernelUpObs L495
theorem kernelUpObs_factors L498
theorem kernelUpObs_selects_counting L502
theorem kernelUpObs_rejects_equalPerSlot L510
def D13_bare_admits_hand_placed L519
theorem D13_sharpened_holds L528
def D13_theorem L539
theorem D13_theorem_provenance_holds L546
theorem kernel_sees_what_posting_cannot L553
structure D14_LedgerScheduleProvenance L566
def D14_bare_admits_rate_readoff L579
def tickCarrier L620
def postingMove L625
def settlementMoves L629
def ledgerMoves L633
def ledgerMoveCount L638
theorem postingMove_card L641
theorem settlementMove_card L645
theorem settlementMoves_card L651
theorem ledgerMoveCount_up L657
theorem ledgerMoveCount_down L670
theorem ledgerMoveCount_off L685
theorem ledgerMoveCount_eq_kernel L703
def D14_theorem L725
theorem D14_theorem_provenance_holds L734
theorem unpinned_up_moves_at_least_two L740
structure D15_CanonicalHistoryPinning L755
def D15_bare_admits_hand_pinning L765
def tickSchedule L800
def canonicalRun L805
def carrierLedger L809
theorem canonicalRun_succ L814

… and 34 more