Admissible
plain-language theorem explainer
Admissible encodes the 45-gap experience gate for a given period and CQ alignment as the disjunction that the requirement predicate fails or an explicit experience flag holds. Modelers building ethical constraints into Recognition Science simulations or SAT encodings cite it when layering admissibility before cost-based preference. The definition is a direct one-line disjunction that imports the Gap45 rule without further reduction.
Claim. Let $n$ be a period in $ℕ$, $c$ a CQ alignment, and $e$ a proposition. The configuration is admissible when $¬R(c,n) ∨ e$, where $R$ is the experience-requirement predicate from the 45-gap rule (true precisely when 8 does not divide $n$).
background
The CostModel module defines ethical preference via lower cost being better and introduces CQ as an alignment threshold drawn from Measurement. Period is taken from the phi-ladder construction as $ϕ^k$. The requiresExperience predicate is imported from Gap45.Beat and implements the concrete gating rule that experience is required exactly when 8 does not divide the period.
proof idea
One-line definition that directly expands to the disjunction of the negation of requiresExperience c period or the supplied hasExperience proposition.
why it matters
Admissible supplies the first gate in PreferLex, which orders admissible plans ahead of cost comparison. It is referenced by BWD3Model to attach ethical constraints to linear SAT witnesses. The definition closes the Gap45 experience rule into the ethics layer, linking directly to the eight-tick octave where multiples of 8 relax the requirement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.