isBalance
plain-language theorem explainer
isBalance marks phases 4-7 in the Fin 8 cycle as the BALANCE region for equilibration. Researchers testing the 8-tick periodicity hypothesis on recognition traces cite this predicate when partitioning observed dynamics into LOCK and BALANCE intervals. The definition is a direct threshold comparison on the phase index.
Claim. Let $p$ be an element of the finite set $0,1,2,3,4,5,6,7$. Then isBalance$(p)$ holds precisely when $p$ is at least 4.
background
The module states the 8-tick hypothesis that observed folding and recognition traces exhibit 8-phase periodicity, with phases 0-3 assigned to LOCK for structure formation and phases 4-7 assigned to BALANCE for equilibration. Phase is the abbrev Fin 8, the standard 8-element finite set drawn from the upstream ChurchTuringPhysicsStructure.Phase declaration that supplies the 8-tick phase space. The module documentation presents this segmentation as an explicit hypothesis about traces rather than a derived axiom.
proof idea
The declaration is a one-line definition that compares the phase value directly against the constant 4. No lemmas or tactics are invoked; it simply implements the BALANCE region test as a Boolean predicate.
why it matters
This predicate is invoked by the downstream theorems lock_balance_partition and lock_balance_disjoint, which together establish that LOCK and BALANCE form a partition of the eight phases. It realizes the explicit 8-tick hypothesis of the module, aligning with the T7 eight-tick octave step in the forcing chain. The LockPhasePrediction structure further depends on it to encode the claim that LOCK phases exhibit higher structural change than BALANCE phases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.