domainCost
plain-language theorem explainer
The domain cost of a composition ratio m/e equals the recognition cost J(m/e). Chemists deriving RS polymer phase-separation thresholds from Flory-Huggins cite this as the bridge from composition to J-cost. It is a one-line definitional wrapper around the standard J functional.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
The module develops polymer phase separation from RS J-cost on composition ratios. Classical Flory-Huggins has critical interaction parameter $\chi_c=1/2$ at composition $\varphi_c=0.5$; RS replaces this by $\chi_c=\sqrt{J(\varphi)}\approx 0.344$, predicting separation slightly above an RS quantum.
J-cost is the unique recognition cost $J(x)=\frac{x+x^{-1}}{2}-1$ forced by the Recognition Composition Law (T5 uniqueness). It vanishes only at ratio one and is nonnegative for positive arguments. Upstream modules (Cost, Cosmology.RefineTrigger, Gravity.CoherenceCollapse) all expose the same functional.
Domain cost simply evaluates that functional on the monomer-to-environment ratio $m/e$, giving the composition-dependent cost later compared to a canonical threshold.
proof idea
Definitional wrapper with no proof obligations: domain cost of $m$ and $e$ is defined to be $J(m/e)$. The body is a direct application of the imported Jcost functional.
why it matters
Supplies the composition-to-cost map used by the rest of the phase-separation development in this module (nonnegativity, equality-at-one, canonical threshold, and the PhaseSepCert certificate). It anchors the RS claim that phase separation occurs when the Flory parameter exceeds a J-derived quantum rather than the classical $1/2$. The construction sits directly on the T5 J-uniqueness landmark and the Recognition Composition Law, importing the same J used in cosmology and gravity coherence arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.