Foundation Cycle Operator

The cycle operator

A Gray code is a way of listing the 8 vertices of a 3-dimensional cube so that consecutive vertices differ by flipping exactly one coordinate bit. One such Gray code path visits the vertices in the order 0, 1, 3, 2, 6, 7, 5, 4. The cycle operator is the rule that takes each vertex to the next one in this list, and the last vertex back to the first. It is a single directed loop around the cube, and it has a simple algebraic description as an 8 by 8 permutation matrix.

This operator has a clean periodicity: apply it eight times and every vertex returns to where it started, and no smaller number of steps does this. Each step flips exactly one bit, so the cycle is a Hamiltonian path on the cube graph. The operator is also invertible, meaning the loop can be run backward. These properties are proved in the framework's machine-checked library of formal theorems, which verifies that the cycle really has period eight, that it is minimal, and that it is injective.

The cycle operator's eigenvalues are the 8th roots of unity, and its eigenstates are the discrete Fourier transform modes on 8 points. These are the same modes used elsewhere in the framework for Born-rule forcing. The phase each eigenstate accumulates per tick encodes the generation structure of particles and determines the mixing angles. In plain language, the loop's geometry, which bits flip when, is not symmetric across the three axes: one axis flips four times per cycle, while the other two flip twice each. This asymmetry is what the framework connects to the Cabibbo angle, a measured quantity in particle physics.

The framework proves that the flip count on one axis is exactly twice the flip count on another, and this 2-to-1 ratio is the seed of the large Cabibbo angle. The operator itself is a definitional choice, a model of how recognition events step through an 8-state space. What is proved is the period, the minimality, the bit-flip structure, and the asymmetry of the flip counts. The physical bridge from this algebraic object to the measured CKM matrix is a hypothesis, not a theorem.

/-- The cycle permutation: maps vertex v to the next vertex in the cycle.
    If v is visited at tick t, the next vertex is the one visited at tick t+1. -/
def cyclePerm : Fin 8 → Fin 8 :=
  fun v => grayOrder (grayOrderInv v + 1)

/-- The cycle permutation has period exactly 8. -/
theorem cyclePerm_period : ∀ v, (cyclePerm^[8]) v = v := by
  intro v; fin_cases v <;> native_decide

/-- After fewer than 8 iterations, the permutation is NOT the identity. -/
theorem cyclePerm_not_identity_before_8 :
    ∀ k, 0 < k → k < 8 → ∃ v, (cyclePerm^[k]) v ≠ v := by
  intro k hk hk8
  interval_cases k <;> exact ⟨0, by native_decide⟩

/-- Each step of the cycle equals a single bit flip (the one identified by flippedBit). -/
theorem cycle_step_is_bitflip (t : Fin 8) :
    cyclePerm (grayOrder t) = bitFlipOp (flippedBit t) (grayOrder t) := by
  fin_cases t <;> native_decide

/-- ω⁸ = 1. -/
theorem omega8_pow_eight : omega8 ^ 8 = 1 := by
  -- This follows from exp(2πi/8)^8 = exp(2πi) = 1.
  -- The proof requires careful handling of ℂ-cast of ↑(8:ℕ) vs (8:ℂ).
  -- The key fact needed: Complex.exp_nat_mul and Complex.exp_two_pi_mul_I.
  -- Pre-existing issue: the rw path through exp_nat_mul cast doesn't resolve.
  -- Structural result not needed for baryogenesis chain; safe to defer.
  simp only [omega8]
  have : Complex.exp (2 * ↑Real.pi * Complex.I / 8) ^ 8 =
         Complex.exp (8 * (2 * ↑Real.pi * Complex.I / 8)) := by
    rw [← Complex.exp_nat_mul]
    norm_cast
  rw [this]
  have h : (8 : ℂ) * (2 * ↑Real.pi * Complex.I / 8) = 2 * ↑Real.pi * Complex.I := by
    norm_cast; ring
  rw [h]
  exact Complex.exp_two_pi_mul_I

/-- The generation-axis coupling strength is proportional to the flip count.
    Generation g (axis g) sees `bitFlipCount g` transitions per cycle. -/
theorem generation_axis_coupling :
    GrayCodeChirality.bitFlipCount 0 = 4 ∧
    GrayCodeChirality.bitFlipCount 1 = 2 ∧
    GrayCodeChirality.bitFlipCount 2 = 2 :=
  GrayCodeChirality.chiralityCert.flipCounts

/-- The generation coupling ratio 2:1 between axis 0 and axes 1,2
    is the kinematic origin of the large Cabibbo angle.

    Qualitative prediction: because generation 1's axis is driven twice
    as often, the overlap between mass and weak bases is large for the
    1-2 mixing (Cabibbo) and smaller for the 2-3 mixing. -/
theorem large_cabibbo_from_coupling_ratio :
    GrayCodeChirality.generationFlipCount 0 = 2 * GrayCodeChirality.generationFlipCount 1 :=
  GrayCodeChirality.generation_coupling_asymmetry.1

What this page does not claim

The cycle operator is not derived from the cost function; it is a definitional choice. The connection from the cycle operator to the measured CKM matrix is not proved, it is a hypothesis. The cycle operator does not by itself force three spatial dimensions.

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/CycleOperator.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: