module module

`IndisputableMonolith.Foundation.CycleOperator`

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 (3)

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

IndisputableMonolith.Foundation.MassWeakBases module_import
IndisputableMonolith.StandardModel.CKMFromCube module_import
IndisputableMonolith.StandardModel.CPPhaseDerivation module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.EightTick module_import
IndisputableMonolith.Foundation.FaceWinding module_import
IndisputableMonolith.Foundation.GaugeFromCube module_import
IndisputableMonolith.Foundation.GrayCodeChirality module_import
IndisputableMonolith.Patterns.GrayCycle module_import

declarations in this module (20)

def grayOrder L57
def grayOrderInv L61
theorem grayOrderInv_left_inv L71
theorem grayOrderInv_right_inv L74
def cyclePerm L79
theorem cyclePerm_explicit L84
theorem cyclePerm_injective L90
theorem cyclePerm_period L95
theorem cyclePerm_not_identity_before_8 L99
def bitFlipOp L110
theorem bitFlipOp_involution L115
theorem cycle_step_is_bitflip L120
def omega8 L130
theorem omega8_pow_eight L133
def dft8Mode L152
def axisFlipCount L163
theorem generation_axis_coupling L170
theorem large_cabibbo_from_coupling_ratio L182
structure CycleOperatorCert L189
def cycleOpCert L197