scale_change_cost
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that J(cx) equals the right-hand side for general c and x.
- Does not apply when c or x is non-positive.
- Does not quantify the bound for specific numerical values of c and x.
- Does not extend to non-multiplicative recognition structures.
Lean usage
lemma apply_scale_change_cost {c x : ℝ} (hc : 0 < c) (hx : 0 < x) : Jcost (c * x) ≤ 2 * Jcost c * Jcost x + 2 * Jcost c + 2 * Jcost x := scale_change_cost hc hxformal statement (Lean)
45theorem scale_change_cost {c x : ℝ} (hc : 0 < c) (hx : 0 < x) :
46 Jcost (c * x) ≤ 2 * Jcost c * Jcost x + 2 * Jcost c + 2 * Jcost x := by
proof body
Term-mode proof.
47 have h := rcl_equality hc hx
48 -- J(cx) + J(c/x) = 2J(c)J(x) + 2J(c) + 2J(x)
49 -- J(cx) ≤ 2J(c)J(x) + 2J(c) + 2J(x) since J(c/x) ≥ 0
50 linarith [Jcost_nonneg (div_pos hc hx)]
51
52/-- If c = 1 (no scale change), cost is zero. -/