pith. machine review for the scientific record. sign in
def definition def or abbrev high

cpTransformTick

show as:
view Lean formalization →

cpTransformTick encodes the charge-parity map on the eight-tick cycle of Recognition Science. Cosmologists working on baryogenesis cite it to exhibit the phase asymmetry that supplies the observed matter excess. The definition is realized by a direct modular subtraction that sends each tick k to 8 minus k modulo 8.

claimThe CP transformation on the 8-tick cycle is the map $kmapsto(8-k)bmod8$ for $k=0,1,dots,7$.

background

Recognition Science organizes time into an eight-tick octave, the fundamental period fixed by the self-similar point phi. The constant tick is the unit time quantum tau_0=1 in RS-native units, with one octave equal to eight ticks. Module COS-007 derives the baryon-to-photon ratio eta approximately 6 times 10 to the minus 10 from an intrinsic CP asymmetry inside this cycle. Upstream lemmas establish that the J-cost of any recognition event is non-negative and that nuclear densities sit on discrete phi-tiers.

proof idea

The definition constructs the image tick by integer subtraction followed by reduction modulo 8, then packages the result as an element of Fin 8; the omega tactic discharges the membership obligation.

why it matters in Recognition Science

This definition supplies the concrete map required to state that CP fails to be a symmetry of the 8-tick cycle, which is the second Sakharov condition in the Recognition Science account of baryogenesis. It feeds the downstream claim that the resulting epsilon_CP equals the observed eta. The construction rests on the eight-tick octave (T7) and the J-uniqueness property (T5).

scope and limits

formal statement (Lean)

  94def cpTransformTick (k : Fin 8) : Fin 8 :=

proof body

Definition body.

  95  ⟨(8 - k.val) % 8, by omega⟩
  96
  97/-- **THEOREM**: CP is not a symmetry of the 8-tick cycle.
  98    Specifically, the J-cost is NOT invariant under CP for generic states. -/

depends on (14)

Lean names referenced from this declaration's body.