ScaleInvarianceCert
plain-language theorem explainer
The ScaleInvarianceCert structure packages four properties of the Jcost function: the Recognition Composition Law equality, an upper bound on the cost of scale changes, invariance under unit scaling, and symmetry under inversion. Pre-Big-Bang cosmologists cite it when showing that cost minimization selects scale-invariant laws among candidate cost functions. It is introduced directly as a structure definition that collects the properties for later use.
Claim. A structure certifying that the cost function $J$ obeys the recognition composition law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ for all $x,y > 0$, the scale-change bound $J(cx) ≤ 2J(c)J(x) + 2J(c) + 2J(x)$ for all $c,x > 0$, the unit-scaling identity $J(1·x) = J(x)$ for all $x > 0$, and the inversion symmetry $J(x) = J(x^{-1})$ for all $x > 0$.
background
In Recognition Science the Jcost function quantifies the recognition cost of a positive real scale factor. The module formalizes the pre-Big-Bang paper §5 claim that cost minimization selects scale-invariant laws: while $J(cx) = J(x)$ does not hold in general, the ratio $J(cx)/J(x)$ remains bounded by $J(c)$ itself. The Recognition Composition Law supplies the key upper bound $J(xy) ≤ J(x) + J(y) + 2·J(x)·J(y)$.
proof idea
This is a structure definition that directly encodes the four properties as fields. No lemmas or tactics are invoked inside the declaration; the fields are populated downstream by the sibling lemmas rcl_equality, scale_change_cost, no_scale_change_is_free and Jcost_symm.
why it matters
The certificate supplies the structural fact required by scaleInvarianceCert, which assembles the properties into a single object. It realizes the paper §5 proposition that the Recognition Composition Law together with cost-minimization forces the unique J form, consistent with T5 J-uniqueness and the eight-tick octave. It leaves open how the pre-Big-Bang dynamics enforce the bound without presupposing the explicit hyperbolic expression for J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.