rcl_equality
plain-language theorem explainer
rcl_equality establishes the equality form of the Recognition Composition Law for positive reals x and y: J(xy) + J(x/y) equals 2 J(x) J(y) plus 2 J(x) plus 2 J(y). Cosmology arguments on scale-invariance selection cite it when bounding the cost of combining scales. The proof rewrites each J term via the squared-ratio identity, clears denominators under positivity, and reduces the polynomial identity by ring.
Claim. For all positive real numbers $x$ and $y$, the cost function satisfies $J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y)$, where $J(z) = (z-1)^2/(2z)$.
background
The module formalizes the pre-Big-Bang paper §5 claim that cost minimization selects scale-invariant laws. Jcost is the function J(z) = (z-1)^2/(2z) supplied by Jcost_eq_sq. Upstream, cost is the derived cost of a multiplicative recognizer comparator and the J-cost of any recognition event state. The Recognition Composition Law supplies the exact algebraic relation that bounds the cost of scale change without requiring naive invariance J(cx) = J(x).
proof idea
The term proof applies Jcost_eq_sq four times to replace each J term by its squared-ratio form under the positivity hypotheses. field_simp normalizes the resulting fractions using the supplied non-zero conditions, after which ring confirms the polynomial identity.
why it matters
This equality is the direct input to scale_change_cost, which obtains the inequality bound by dropping the non-negative J(c/x) term, and to scaleInvarianceCert, which packages the full certificate. It realizes the Recognition Composition Law in the framework, linking to T5 J-uniqueness and the phi fixed-point selection. The module uses it to show that the ratio J(cx)/J(x) remains controlled by J(c).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.