module module

`IndisputableMonolith.Foundation.FaceWinding`

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.CycleOperator module_import
IndisputableMonolith.Foundation.GrayCodeChirality module_import
IndisputableMonolith.StandardModel.CPPhaseDerivation module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.GaugeFromCube module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.Patterns.GrayCycle module_import

declarations in this module (22)

structure CubeFace L46
def allFaces L52
theorem allFaces_length L57
theorem face_count_matches L60
structure DirectedEdge L70
def cycleEdges L78
def flippedBit L89
def vertexBit L110
def edgeOnFace L115
def freeAxes L135
def edgeFaceSign L143
def faceWinding L166
def allWindings L170
def totalChiralCharge L178
def netChiralCharge L184
theorem flippedBit_sequence L191
theorem bit_flip_counts L196
theorem face_pairs_have_three_axes L204
theorem each_edge_on_two_faces L210
theorem axis_flip_asymmetry L217
def reversedCycleEdges L222
theorem reversed_swaps_endpoints L233