requiresExperience
plain-language theorem explainer
requiresExperience(c, p) holds exactly when 8 does not divide p, for any coherence quotient c. Ethics and cost-model authors cite it to enforce the 45-gap experience gate. The declaration is a one-line abbreviation that imports the Gap45 definition verbatim.
Claim. For coherence quotient $c$ and natural number $p$, requiresExperience$(c,p)$ is the proposition $8$ does not divide $p$.
background
CQ is the coherence quotient structure from Measurement with fields listensPerSec, opsPerSec and coherence8 (bounded in [0,1]). The predicate originates in Gap45.Beat as the negation of 8 dividing the period, implementing the eight-tick octave gate. This abbreviation in Ethics.CostModel simply re-exports that definition for use in admissibility checks.
proof idea
One-line abbreviation that directly references Gap45.requiresExperience, inheriting its @[simp] reduction to ¬(8 ∣ period).
why it matters
The definition supplies the experience gate inside Admissible, which states a plan is admissible when either no experience is required or it is supplied. It encodes the 45-gap rule tied to the eight-tick octave (period 2^3) from the forcing chain. It closes the placeholder noted in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.