requiresExperience
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not inspect the numerical value of the coherence quotient.
- Does not incorporate measurement error or uncertainty from the Measurement structure.
- Does not extend to periods measured in real numbers or fractional beats.
- Does not enforce any lower bound on the period size.
Lean usage
example (c : CQ) : requiresExperience c 9 := by simpformal statement (Lean)
10@[simp] def requiresExperience (_c : IndisputableMonolith.Measurement.CQ) (period : Nat) : Prop :=
proof body
Definition body.
11 ¬ (8 ∣ period)
12