balance_start
plain-language theorem explainer
balance_start assigns the constant 4 to mark the onset of the BALANCE segment inside the eight-phase cycle. Researchers testing RRF discretization hypotheses cite this label when partitioning observed traces into LOCK and BALANCE intervals. The declaration is a direct constant assignment inside the Fin 8 type with no further computation.
Claim. Define the phase marking the start of the BALANCE interval as $4$, where phases are elements of the finite set $Fin 8$.
background
The module RRF.Hypotheses.EightTick encodes the explicit hypothesis that recognition traces exhibit 8-phase periodicity, with phases 0-3 labeled LOCK for structure formation and phases 4-7 labeled BALANCE for equilibration. Phase is introduced as the abbreviation $Fin 8$, supplying the discrete time/process index for one cycle. The same Phase abbreviation appears upstream in Information.ChurchTuringPhysicsStructure, where it is likewise defined as $Fin 8$ to represent the 8-tick phase space.
proof idea
The declaration is a direct constant definition that binds the identifier to the numeral 4 inside the Phase type. No lemmas or tactics are invoked; the body is simply the literal assignment.
why it matters
The definition supplies the explicit starting index for the BALANCE segment of the eight-tick cycle, directly supporting the T7 eight-tick octave landmark in the forcing chain. It provides the concrete label needed for falsification tests listed in the module documentation, although the used_by count is currently zero. It therefore closes one small interface point in the RRF hypothesis scaffolding without resolving the broader question of whether eight phases are optimal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.