compose_assoc
plain-language theorem explainer
The theorem proves associativity of composition on positive frequency ratios under the strict music realization. Researchers establishing admissible realizations in the UniversalForcing framework cite it to verify that the music domain satisfies the required structural laws. The term proof reduces the claim to associativity of real multiplication via subtype extension and the ring tactic.
Claim. For all positive real numbers $a, b, c > 0$, if composition is defined by multiplication of the underlying values, then $(a b) c = a (b c)$.
background
The RichDomainCosts module supplies the concrete theorems that discharge the placeholder laws (composition_law, excluded_middle_law, invariance_law) in the five StrictLogicRealization instances for Music, Biology, Narrative, Ethics and Metaphysical. FrequencyRatio is the music carrier, the subtype of positive reals. strictMusicRealization sets compose to multiplication of these ratios, modeling octave stacking as the generator.
proof idea
One-line wrapper that applies Subtype.ext to equate the underlying real numbers, then invokes the ring tactic to obtain associativity of multiplication.
why it matters
It supplies the compose_assoc field demanded by the AdmissibleRealization structure, which requires associativity for a realization to count as admissible. The result is used directly in music_admissible to build the admissible instance for music and in richDomainCostsCert_holds to certify the full set of domain costs. It discharges the composition_law placeholder for the music domain, confirming that the strict realization carries non-trivial algebraic structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.