module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2TailFiberShiftBridge`

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.Gap2AntipodalBalanceBridge module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2TailFiberShiftBridgeAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2EnrichedCarrierPhase module_import

declarations in this module (47)

structure TailFiberShift L62
lemma fin8_add_one_ne L74
theorem tickFiberMass_succ_of_tailFiberShift L84
theorem tickFiberMass_eq_zero_of_tailFiberShift L111
theorem eventuallyTickFiberMassBalanced_of_tailFiberShift L135
theorem oscillatoryTail_of_tailFiberShift L144
theorem oscillatoryTail_of_labeled_tailFiberShift L151
theorem tick_shift_excludes_fixed_point L160
theorem fixed_class_blocks_tick_shift L171
def endpointReversal L185
theorem endpointReversal_involutive L190
theorem endpointReversal_ge L195
def tetSlotRotation L217
theorem tetSlotRotation_ge L222
def endpointReversalThenTetSlotRotation L237
theorem endpointReversalThenTetSlotRotation_ge L241
def allLoopsComplex L252
theorem endpointReversal_fixes_allLoops L256
def constTetComplex L262
theorem tetSlotRotation_fixes_constTet L266
theorem endpointReversalThenTetSlotRotation_fixes_constTet L270
theorem endpointReversalThenTetSlotRotation_fixes_allLoops L281
theorem endpointReversal_fixes_isolated L292
theorem tetSlotRotation_fixes_isolated L299
theorem endpointReversalThenTetSlotRotation_fixes_isolated L305
def endpointReversalClass L314
theorem endpointReversalClass_mk L321
theorem endpointReversalClass_involutive L327
def endpointReversalClassEquiv L335
theorem endpointReversalClass_fixes_isolatedClass L342
def tetSlotRotationClass L349
def tetSlotRotationInv L357
theorem tetSlotRotation_left_inv L362
theorem tetSlotRotation_right_inv L373
theorem tetSlotRotationInv_ge L384
def tetSlotRotationClassEquiv L398
theorem tetSlotRotationClass_fixes_isolatedClass L420
def endpointReversalThenTetSlotRotationClass L427
def endpointReversalThenTetSlotRotationClassEquiv L431
theorem endpointReversalThenTetSlotRotationClass_eq_equiv L435
theorem endpointReversalThenTetSlotRotationClass_fixes_isolatedClass L441
theorem endpointReversal_no_tailFiberShift L453
theorem tetSlotRotation_no_tailFiberShift L466
theorem endpointReversalThenTetSlotRotation_no_tailFiberShift L479
structure Gap2TailFiberShiftBridgeStatus L494
def gap2TailFiberShiftBridgeStatus L502
theorem gap2TailFiberShiftBridgeStatus_flags L510