Foundation Face Winding Axis Flip Asymmetry

The axis flip asymmetry

In the Recognition Science (RS) framework, the fundamental unit of change is an eight-step cycle, called a tick cycle, that moves through the eight corners of a three-dimensional cube. Each step of this cycle flips exactly one of the cube's three coordinates, which the framework calls an axis. The declaration axis_flip_asymmetry establishes a plain counting fact: within one full cycle, the number of steps that flip the first axis is not equal to the number of steps that flip the second axis. Specifically, the cycle flips the first axis four times, the second axis two times, and the third axis two times. This is a proved theorem in the framework's machine-checked library of formal theorems, and it is not a definition or a choice.

The counting fact matters because it breaks a symmetry. If the cycle were perfectly balanced, reversing its direction would produce a mirror-image cycle with the same axis-flip counts. The asymmetry means that a forward cycle and a backward cycle are structurally different objects. The framework uses this difference as the geometric origin of a physical phenomenon called CP violation, the observed asymmetry between matter and antimatter behavior. The winding number of the cycle around each face of the cube measures how the cycle wraps around that face, and a nonzero winding means the cycle distinguishes clockwise from counterclockwise traversal. The sum of these face windings, called the total chiral charge, is proved to be nonzero, which is the formal statement that the cycle has a built-in handedness.

The theorem is a statement about a specific, explicitly defined cycle on a cube. It is not a claim about all possible cycles, nor does it assert that the asymmetry is large or physically significant on its own. The framework's library also proves supporting facts: the cube has exactly six faces, each edge lies on exactly two faces, and the cycle's edge sequence is fully specified. These are the building blocks that make the asymmetry theorem precise. The theorem does not, by itself, derive the value of any physical constant or predict any experimental result. It establishes a structural property of the framework's fundamental cycle, and the connection from that property to observable physics is a separate, open question.

/-- The cycle traverses edges along all three axes. Specifically, 4 edges
    flip bit 0, 2 edges flip bit 1, and 2 edges flip bit 2.
    The 4:2:2 split breaks the S₃ axis-permutation symmetry. -/
theorem axis_flip_asymmetry :
    (List.ofFn flippedBit).count 0 ≠ (List.ofFn flippedBit).count 1 := by
  native_decide

/-- Bit 0 flips 4 times, bit 1 flips 2 times, bit 2 flips 2 times.
    This asymmetry (4 vs 2 vs 2) is the combinatorial origin of chirality. -/
theorem bit_flip_counts :
    (List.ofFn flippedBit).count 0 = 4 ∧
    (List.ofFn flippedBit).count 1 = 2 ∧
    (List.ofFn flippedBit).count 2 = 2 := by native_decide

/-- The total chiral charge: sum of absolute face windings.
    Measures the total asymmetry of the cycle's interaction with face boundaries.
    Nonzero means the cycle is chiral. -/
def totalChiralCharge : ℤ :=
  ∑ i : Fin 8, ∑ f ∈ allFaces.toFinset, (edgeFaceSign i f).natAbs

What this page does not claim

The theorem does not claim that the asymmetry is large or that it alone explains any measured physical quantity. The theorem does not claim that every cycle on a cube has this property; it holds for the framework's specific defined cycle. The theorem does not claim that the connection from this structural asymmetry to observable CP violation has been established; that bridge remains open.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/FaceWinding.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: