costOfInhomogeneity
plain-language theorem explainer
costOfInhomogeneity assigns the J-cost of the ratio 1 + |δρ| to any density contrast δρ. Cosmologists working inside the Recognition Science treatment of the horizon problem cite it when showing that inhomogeneities raise total recognition cost. The body is a one-line wrapper around the Jcost operator imported from the multiplicative recognizer.
Claim. The cost of a density contrast δρ is given by J(1 + |δρ|), where J denotes the cost function induced by a multiplicative recognizer on positive ratios.
background
The module COS-004 treats the horizon problem as a synchronization question solved by the universal 8-tick clock rather than by causal contact. J-cost is the derived cost of a multiplicative recognizer's comparator applied to positive ratios; the cost of any recognition event equals its J-cost. Density itself is expressed on the phi-ladder as phi raised to an integer rung. Upstream results supply the recognizer cost definition and the non-negativity of recognition-event cost.
proof idea
The definition is a one-line wrapper that applies Jcost directly to the scaled density contrast 1 + abs δρ.
why it matters
This definition supplies the cost measure required by the downstream theorem homogeneous_minimizes_cost, which proves that the homogeneous case (δρ = 0) has strictly lower J-cost than any nonzero contrast. It fills the COS-004 step by linking 8-tick ledger synchronization to cost-driven relaxation toward uniformity, the same mechanism that appears in the Recognition Composition Law and the T5 J-uniqueness property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.