balance_end
plain-language theorem explainer
The balance_end constant marks phase 7 as the termination of the BALANCE segment inside the 8-phase cycle. Researchers modeling discrete recognition traces cite it when partitioning observed folding dynamics into LOCK (0-3) and BALANCE (4-7) intervals. The definition is a direct numerical assignment inside the Fin 8 type with no further computation.
Claim. Let Phase := Fin 8. Define balance_end := 7, so that balance_end denotes the final phase of the BALANCE region (phases 4 through 7) in the 8-beat discretization.
background
The RRF.Hypotheses.EightTick module encodes the explicit hypothesis that recognition traces exhibit 8-phase periodicity, with phases 0-3 forming the LOCK interval for structure formation and phases 4-7 forming the BALANCE interval for equilibration. Phase is introduced as the abbreviation Fin 8, supplying a finite index set for the cycle. Upstream, Foundation.EightTick.phase supplies the concrete real-valued angles kπ/4 for each k in Fin 8, while ChurchTuringPhysicsStructure.Phase and RiemannHypothesis.Wedge.phase reuse the same Fin 8 indexing in information-theoretic and complex-analytic settings.
proof idea
The definition is a direct one-line assignment of the literal 7 to balance_end of type Phase. No lemmas or tactics are applied; the value simply selects the last element of the 8-element finite set.
why it matters
This definition supplies the concrete endpoint of the BALANCE half-cycle required by the 8-tick hypothesis in the module documentation. It completes the partition used by sibling predicates such as isBalance and lock_balance_partition. Within the Recognition framework it instantiates the T7 eight-tick octave, labeling the equilibration segment that follows the LOCK structure-formation segment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.