scaleInvarianceCert
plain-language theorem explainer
The scaleInvarianceCert assembles a record that certifies the J-cost obeys the Recognition Composition Law equality, a bound on the cost of scale changes, invariance under unit scaling, and symmetry under inversion. Pre-Big-Bang cosmologists would cite it to confirm that cost minimisation selects scale-invariant dynamics among candidate cost functions. The definition is a direct record constructor that wires four upstream lemmas into the ScaleInvarianceCert structure.
Claim. Let $J$ be the J-cost. The scale-invariance certificate asserts that for all $x,y>0$, $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, that $J(cx)≤2J(c)J(x)+2J(c)+2J(x)$ for all $c,x>0$, that $J(1·x)=J(x)$ for all $x>0$, and that $J(x)=J(x^{-1})$ for all $x>0$.
background
The module formalises the structural claim from pre-Big-Bang paper §5 that scale invariance is selected by cost minimisation. Among candidate cost functions only the form satisfying the Recognition Composition Law upper bound forces the unique solution $J(x)=(x+x^{-1})/2-1$. The certificate records four properties: the RCL equality, the scale-change bound, unit-scale freeness, and log-space symmetry under inversion. Jcost is the cost function whose explicit form is $J(x)=(x+x^{-1})/2-1$ (from JcostCore). Upstream lemmas establish each field separately: rcl_equality proves the equality by rewriting to squares and field simplification; scale_change_cost derives the inequality from rcl_equality plus non-negativity of Jcost; no_scale_change_is_free shows the unit case by direct simplification; Jcost_symm proves inversion symmetry by the same square rewriting.
proof idea
The definition is a one-line record constructor. It sets the rcl field to the theorem rcl_equality, the scale_cost_bound field to scale_change_cost, the free_at_unit field to no_scale_change_is_free, and the log_symmetric field to Jcost_symm. No additional tactics are required; the four lemmas already carry the required hypotheses on positivity.
why it matters
This definition supplies the complete certificate required by the Recognition framework to close the scale-invariance selection argument in Cosmology. It directly implements the cost-of-scale-change principle stated in the module doc-comment and thereby supports the claim that only the J-cost satisfies the compositional constraint while remaining bounded under rescaling. The certificate sits at the interface between the RCL (T5) and the forcing chain that selects D=3 and the eight-tick octave; it is the concrete object that would be invoked when deriving the phi-ladder mass formula or the alpha band from cost minimisation. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.