richDomainCostsCert_holds
plain-language theorem explainer
The declaration shows that RichDomainCostsCert is inhabited by the associativity of domain-specific composition operations together with the zero-cost equivalence to equality in music, biology, narrative, and ethics. Researchers verifying strict realizations of universal forcing cite it to confirm that each domain supplies non-placeholder algebraic laws for its cost functions. The proof is a direct term-mode record construction that populates every field from the corresponding domain lemma.
Claim. The structure certifying rich-domain cost laws holds: composition is associative for frequency ratios under multiplication, for lineage states under reproduction, for event states under addition, and for action states under preference composition; moreover each domain cost vanishes if and only if its arguments are identical.
background
The module supplies the concrete realizations of composition, excluded-middle, and invariance laws for the five domains inside the StrictLogicRealization framework. Each domain module begins with placeholder instances whose composition_law and invariance_law fields are set to True; the present theorems replace those placeholders with proved statements about the actual cost predicates and composition maps.
proof idea
The proof constructs the RichDomainCostsCert record by direct field assignment. It maps music_compose_assoc to the associativity lemma for frequency-ratio multiplication, biology_reproduce_assoc to the reproduction associativity lemma, narrative_eventCompose_assoc to the event-addition associativity lemma, and ethics_preferenceCompose_assoc to the preference-addition associativity lemma. The four cost-zero fields receive the corresponding zero-cost equivalence lemmas proved by case analysis on equality.
why it matters
The theorem supplies the first-class, non-placeholder statements that any claim of strict realization must cite. It completes the cost-law content for the four rich domains inside UniversalForcing.Strict, thereby supporting the assertion that the forcing chain can be realized without hidden hypotheses. No downstream uses are recorded yet; the result closes the placeholder gap described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.