compose_left_id
plain-language theorem explainer
The theorem establishes left-identity for composition in the strict music realization over positive frequency ratios. Researchers verifying algebraic laws for StrictLogicRealization instances in Recognition Science would cite it when confirming that the music domain satisfies the required identity axiom. The proof reduces the claim to an equality of subtype carriers via direct multiplication by the unit, then applies extensionality and simplification.
Claim. Let $F = {x : ℝ | x > 0}$ be the carrier of positive frequency ratios. Let $∘$ denote the composition in the strict music realization, given by $a ∘ b = ⟨a_1 · b_1, …⟩$ with unit element $1$. Then $∀ a ∈ F$, $1 ∘ a = a$.
background
The Rich Domain Cost Theorems module supplies first-class proofs of composition, decidability, and invariance for the five domain realizations (Music, Biology, Narrative, Ethics, Metaphysical). For Music, FrequencyRatio is the subtype of positive reals and strictMusicRealization defines composition by multiplication of the underlying values together with the positivity witness. This left-identity statement is one of the six required laws listed in the module documentation for each domain. Upstream, the compose definition in VirtueComposition supplies an analogous additive-multiplicative structure for ethics effects, while the one elements from IntegersFromLogic and RationalsFromLogic supply the unit used in the music carrier.
proof idea
The term proof first rewrites the left-hand side as the subtype element whose underlying real is 1 multiplied by a.1. It then applies Subtype.ext to reduce the equality to an equality of reals and finishes with simp to discharge the multiplication identity.
why it matters
The result supplies the left-identity law for the music domain inside the RichDomainCosts module, whose theorems are the statements to cite for non-trivial law-bearing in each strict realization. It directly supports the composition law required by the Recognition Composition Law and the forcing-chain steps T5–T7. No downstream uses are recorded yet, and the module reports zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.