scale_change_cost
plain-language theorem explainer
The scale-change cost bound establishes that for positive reals c and x the J-cost of their product is at most twice the product of their J-costs plus twice each. Cosmologists studying scale-invariance selection in pre-Big-Bang models cite this when deriving cost bounds under rescaling. The proof is a direct application of the RCL equality combined with non-negativity of the J-cost of the ratio c/x.
Claim. For positive real numbers $c$ and $x$, the J-cost satisfies $J(c x) ≤ 2 J(c) J(x) + 2 J(c) + 2 J(x)$.
background
J-cost is the function $J(x) = ½(x + x^{-1}) - 1$ for $x > 0$, the unique solution satisfying the Recognition Composition Law under the forcing chain. The RCL equality states that $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ for positive $x,y$. This module addresses the pre-Big-Bang paper §5 claim that scale invariance is selected by minimizing the cost of scale changes, where the bound on $J(cx)$ controls deviations from invariance.
proof idea
The proof invokes the rcl_equality lemma to obtain the identity $J(c x) + J(c/x) = 2 J(c) J(x) + 2 J(c) + 2 J(x)$, then applies the non-negativity lemma Jcost_nonneg to the term $J(c/x)$ and concludes the inequality by linarith.
why it matters
This theorem provides the scale_cost_bound field in the ScaleInvarianceCert definition, which collects the certificates for scale-invariance selection. It fills the cost-of-scale-change principle in pre-Big-Bang paper §5 and connects to the Recognition Composition Law upper bound. The result supports the framework's claim that only the specific J form satisfies the compositional constraint with bounded scale costs, relating to the T5 J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.