compose_left_id
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the right-identity law for the same composition.
- Does not address invariance under relabeling.
- Does not treat the biology, narrative, ethics or metaphysical domains.
- Does not establish decidability or zero-cost equivalence.
formal statement (Lean)
62theorem compose_left_id (a : FrequencyRatio) :
63 strictMusicRealization.compose strictMusicRealization.one a = a := by
proof body
Term-mode proof.
64 show (⟨1 * a.1, _⟩ : FrequencyRatio) = a
65 apply Subtype.ext
66 simp
67
68end MusicRich
69
70/-! ## Biology -/
71
72namespace BiologyRich
73
74open Biology
75