RichDomainCostsCert
plain-language theorem explainer
RichDomainCostsCert bundles associativity of composition and the zero-cost equivalence condition across the music, biology, narrative, and ethics strict realizations. Researchers extending the universal forcing chain to rich domains cite it to confirm that costs remain non-trivial and compositions behave as expected. The definition aggregates four domain-specific lemmas already proved in the sibling modules without additional reasoning steps.
Claim. A structure whose fields assert: composition of frequency ratios is associative and ratioCost$(a,b)=0$ iff $a=b$; reproduction of lineage states is associative and lineageCost$(a,b)=0$ iff $a=b$; event composition is associative and eventCost$(a,b)=0$ iff $a=b$; preference composition is associative and actionCost$(a,b)=0$ iff $a=b$.
background
The module supplies concrete theorems replacing the composition_law, excluded_middle_law, and invariance_law placeholders that appear in the five domain modules (Music, Biology, Narrative, Ethics, Metaphysical). Each domain carries its own cost: ratioCost is the scale-invariant comparison obtained by evaluating the comparison operator at the positive ratio $r/1$; lineageCost returns 0 precisely when two LineageState records (lineage label plus generation depth) coincide and otherwise 1, with reproduce adding the generation depths while preserving the label; actionCost and eventCost are defined analogously. Upstream, the ethics compose operation adds sigma changes and multiplies the jbar and gap multipliers while preserving positivity.
proof idea
The declaration is a bare structure definition. Its fields are populated directly by the already-proved lemmas MusicRich.compose_assoc, BiologyRich.reproduce_assoc, NarrativeRich.eventCompose_assoc, EthicsRich.preferenceCompose_assoc together with the four cost_zero_iff statements from the same modules. No tactics or reductions occur inside the definition itself.
why it matters
richDomainCostsCert_holds constructs an inhabitant of this structure by quoting the domain lemmas, thereby discharging the master certificate for the strict universal forcing. The certificate supplies the concrete content of the composition law (RCL) and the invariance law across rich domains, advancing the T5–T8 steps of the forcing chain by ensuring that J-costs and self-similar fixed points remain well-behaved when the carrier is expanded beyond the arithmetic core. It leaves the metaphysical domain and the triangle inequalities for later closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.