domainCost
plain-language theorem explainer
Domain cost assigns the Recognition Science cost J to a mass-to-energy ratio m/e. Cosmologists deriving the baryon density fraction Omega_b from the phi-ladder cite it as the local cost of a mass domain relative to an energy scale. The body is a one-line abbreviation of the unique J-cost functional.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The module derives a structural value for the baryon density parameter Omega_b from the phi-ladder (Plan v7, 119th pass). Status is a structural theorem with no sorry and no axioms; the target comparison is Omega_b = 0.049 against the RS estimate J(phi)/2 ≈ 0.059.
The cost functional is the unique J forced by the Recognition Composition Law: J(x) = (x + x^{-1})/2 - 1, equivalently cosh(log x) - 1. Upstream copies of Jcost (Cost, RefineTrigger, CoherenceCollapse, EnergyProcessingBridge, SpiralField) all fix this same formula; EnergyProcessingBridge notes it is the unique cost forced by RCL, and RefineTrigger records that a genuine distinction (ratio not one) has strictly positive cost.
Domain cost simply specializes that functional to a mass-over-energy ratio, the natural dimensionless argument when a mass domain is scored against an energy scale in the cosmology layer.
proof idea
Pure definition: domainCost m e is defined to be Jcost (m / e). No tactics, no lemmas, no proof obligations. Downstream nonnegativity and evaluation lemmas (siblings such as domainCost_nonneg and domainCost_at_eq) inherit directly from the corresponding properties of J.
why it matters
This is the cost primitive for the OmegaBaryon4 development. The module aims at a structural match between observed Omega_b ≈ 0.049 and the RS combination J(phi)/2 ≈ 0.059, tying baryon fraction to the T5 J-uniqueness and T6 phi fixed-point landmarks. Sibling certificates (OmegaBaryon4Cert, cert, cert_inhabited) and the canonical threshold sit on top of this ratio cost; without a named domain cost the ladder comparison has no local scalar. No downstream edges are recorded yet, so the declaration is infrastructure inside the module rather than a widely reused lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.