pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts

show as:
view Lean formalization →

The RichDomainCosts module equips the five strict domain realizations with explicit cost functions and proves their algebraic properties including zero-cost equivalence, decidability, associativity, and left identity. Researchers building admissible classes cite it to supply the concrete law-bearing instances for StrictLogicRealization. The argument proceeds by direct verification on the imported domain structures for music ratios, biological lineages, narrative events, ethical actions, and metaphysical invariants.

claimThe domain cost functions satisfy zero-cost equivalence ($c(x)=0$ iff $x$ is the identity element), decidability of zero cost, associativity under composition ($c(a∘(b∘c))=c((a∘b)∘c)$), and left identity for each of the five realizations (frequency ratios, lineage states, event sequences, action ranks, and metaphysical structures).

background

The module sits inside the strict Universal Forcing development and imports the five domain realizations. Music supplies positive frequency ratios with equality-based comparison. Biology uses a simple lineage-state structure. Narrative works over event states carrying act and beat coordinates. Ethics employs action states with agent and improvement-rank coordinates. Metaphysical supplies the structural, theology-neutral package. These realizations instantiate the composition and invariance laws as raw Props; the present module replaces the trivial True instances with explicit cost functions and their verified properties.

proof idea

The module first defines the cost functions (ratioCost on frequencies, lineageCost on states, eventCost on sequences, and analogs for ethics and metaphysics). It then proves the required properties by direct case analysis on the domain data: zero-cost iff identity, decidability via the underlying equality, associativity by unfolding the composition operation, and left identity by substitution of the unit element.

why it matters in Recognition Science

This module supplies the concrete associativity, decidability, and invariance properties required by the AdmissibleClass theorem, which quantifies Universal Forcing by carrying excluded_middle_law, composition_law, and invariance_law. It closes the gap between the domain definitions and the admissible-class instantiation, allowing the five realizations to serve as law-bearing models rather than mere placeholders.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (19)