music_admissible
plain-language theorem explainer
The definition constructs an AdmissibleRealization witness for the music strict realization on positive frequency ratios. It is referenced in certificates that confirm all four canonical domains meet the structural conditions for quantified universal forcing. The construction assembles the three fields directly from classical decidability, a pre-proven associativity lemma, and a norm_num identity check on the unit element.
Claim. For the music realization $R$ with carrier the positive reals under multiplication, cost equality is decidable, composition is associative, and $R.compose(R.one, R.one) = R.one$.
background
AdmissibleRealization augments a StrictLogicRealization with three properties: decidability of cost equality via excluded middle, associativity of composition, and the condition that the unit composes with itself to itself. The module uses this to certify the five domain realizations so that quantified universal forcing applies uniformly. The music case rests on the FrequencyRatio carrier from Strict.Music and draws its associativity witness from the RichDomainCosts module.
proof idea
This is a direct construction of the AdmissibleRealization structure. It supplies cost_decidable via Classical.dec, compose_assoc via RichDomainCosts.MusicRich.compose_assoc, and the compose_one_or_step disjunct by Subtype.ext followed by norm_num on the equality one times one equals one.
why it matters
The definition supplies the music_adm field of admissibleClassCert_holds and thereby supports four_canonical_domains_admissible. It confirms that the music frequency-ratio realization satisfies the extra structural laws needed for the quantified universal forcing theorem. In the framework this step ensures the equivalence of forced arithmetic surfaces holds across all admissible realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.