scaleHomogeneityNoGoCert
plain-language theorem explainer
Packages the scale-homogeneity boundary into a single certificate: no joint-scale-invariant selector can force an absolute posted value on a scale-invariant target, any forcing selector fails joint invariance, and the positivity selector witnesses a nonempty nonvacuous class. Cite it as the public form of the forced-skeleton boundary (paper S5 / class wall). The proof is a pure term wiring the doubling-decoy theorem, its admission export, and the positivity witness into the four certificate fields.
Claim. For every carrier $X$ with a positive-real scaling action, the scale-homogeneity no-go certificate holds: (i) if $S$ is joint-scale invariant and $f$ is scale invariant with $f(x_0)>0$ and $S(f(x_0),x_0)$, then $S$ does not force $a=f(x)$ on all accepted pairs; (ii) any selector that does force the value cannot be joint-scale invariant; (iii) the joint-scale-invariant class is nonempty; (iv) on any inhabited carrier the class is inhabited nonvacuously (positivity accepts the witness without fixing the value).
background
The module is the boundary theorem of the forced skeleton, stated type-agnostically. A ScaleAction on a carrier $X$ is a map $\mathbb{R}_{>0}\times X\to X$ obeying the unit and multiplicativity laws, so rescaling cannot hide state dependence. A target $f:X\to\mathbb{R}$ is scale invariant when $f(\mathrm{scale},c,x)=f(x)$; a selector $S\subseteq\mathbb{R}\times X$ is joint-scale invariant when acceptance is stable under simultaneous rescaling of the posted value and the carrier.
The uniqueness chain (T-2 through T8) builds the skeleton without fixing an absolute scale. This module records why the chain stops: any criterion blind to joint rescaling that accepts an intended witness also accepts a doubled decoy whose posted value misses the target. Hence at least one scale-bearing input is required. The statement is deliberately carrier-agnostic; concrete witnesses (real pairs with squared ratio, eight-component complex vectors with a probability weight) only instantiate the hypotheses.
Upstream, the main class theorem is the doubling decoy: from $S(f(x_0),x_0)$ joint invariance yields $S(2f(x_0),\mathrm{scale},2,x_0)$, while scale invariance of $f$ gives $f(\mathrm{scale},2,x_0)=f(x_0)\neq 2f(x_0)$. The admission export is the contrapositive: a forcing selector cannot be joint-scale invariant. The positivity selector $S(a,x)\iff a>0$ ignores the carrier and is therefore joint-scale invariant for every action.
proof idea
Pure term construction of the four certificate fields. class_wall is filled by direct application of no_scaleInvariantSelector_forces_value (the doubling-decoy argument). admission_export is filled by forcingSelector_not_jointScaleInvariant (the contrapositive admission gate). class_nonempty is the pair of the positivity selector with the lemma that it is joint-scale invariant for the given action. class_inhabited_nonvacuous builds an explicit witness on any inhabited carrier: positivity selector, constant posted value $1$, the given point $x_0$, joint invariance of positivity, the trivial forcing failure rfl on the constant-$1$ map, and the two positivity facts $1>0$. No new reasoning; the certificate is the packaging.
why it matters
This is the canonical public form of the boundary theorem used in the paper "Recognition Composition and the Forced Skeleton". The uniqueness chain forces the skeleton (J-cost uniqueness, $\varphi$ as self-similar fixed point, eight-tick octave, $D=3$) without a scale; the certificate states, once and abstractly, that the chain cannot fix absolute values by scale-blind selection alone. The ledger instantiation MassGenesis.T10JointScaleHomogeneityNoGo in the full library is an instance of this class theorem. The amplitude-form sibling restates the paper's S5 claim over a scaled configuration space with a degree-one homogeneous amplitude. No downstream dependents are recorded in the graph yet; the declaration exists as the reusable certificate interface for any later scale-fixing step that must import a scale-bearing input rather than derive one from joint-invariant selection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.