requiresExperience
plain-language theorem explainer
The definition requiresExperience encodes the Gap45 gating rule by declaring that experience is mandatory precisely when a plan's period is not a multiple of 8. Ethical cost modelers in the Recognition Science framework cite this predicate to enforce the 8-beat alignment policy from Source.txt. It is realized as a direct negation of the divisibility relation on natural numbers.
Claim. Let $c$ be a coherence quotient and $p$ a natural number. Then experience is required, written requiresExperience($c$, $p$), precisely when $8$ does not divide $p$.
background
In the Gap45.Beat module the gating rule is introduced to capture the Source.txt policy on 8-beat alignment. CQ is the coherence quotient structure imported from Measurement, carrying listensPerSec, opsPerSec and a coherence8 field bounded between 0 and 1. The predicate takes a CQ value (unused in the body) and a Nat period, returning the proposition that 8 does not divide the period. Upstream, the period function in PulsarEmissionRegimesFromRS defines period(k) := phi^k, while the Ethics.CostModel re-exports this predicate as an abbrev for ethical admissibility checks.
proof idea
The declaration is a one-line definition that directly negates the divisibility relation 8 | period.
why it matters
This predicate is the key input to the Admissible definition in Ethics.CostModel, which declares a plan admissible when either experience is not required or has been supplied. It encodes the eight-tick octave alignment (T7) that disables Gap45 gating, linking the local ethical rule to the broader Recognition Science forcing chain from T0 to T8. The definition closes a placeholder in the cost model by supplying the concrete Gap45 rule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.