ScaleHomogeneityNoGoCert
plain-language theorem explainer
Certificate structure packaging the scale-homogeneity no-go on an arbitrary carrier with a positive-real scaling action: joint-scale-invariant selectors cannot force a unique absolute value of a scale-invariant target; the contrapositive admission form; and non-vacuity witnesses. Anyone assembling the boundary theorem of the forced skeleton cites this bundle. It is a pure Prop record with no proof body.
Claim. For a carrier $X$ equipped with a positive-real scaling action, the certificate asserts four properties: (i) every joint-scale-invariant selector $S$ that accepts a positive value of a scale-invariant target $f$ at some $x_0$ fails to force $a=f(x)$ for all accepted pairs; (ii) any selector that does force the target uniquely cannot be joint-scale-invariant; (iii) at least one joint-scale-invariant selector exists; (iv) if $X$ is nonempty, there exist a joint-scale-invariant selector, a scale-invariant target, and a positive accepted witness.
background
The module states the boundary theorem of the forced skeleton in neutral vocabulary. The uniqueness chain (T-2 through T8) derives the skeleton without a scale; this module shows abstractly why the chain cannot fix absolute values on its own. The carrier $X$ is any type with a positive-real scaling action ScaleAction: a map $\mathrm{scale}:\mathbb{R}\to X\to X$ obeying $\mathrm{scale}(1,x)=x$ and $\mathrm{scale}(cd,x)=\mathrm{scale}(c,\mathrm{scale}(d,x))$, so instances cannot smuggle state-dependent rescaling.
A selector $S:\mathbb{R}\to X\to\mathrm{Prop}$ is joint-scale-invariant when $S(a,x)\leftrightarrow S(ca,\mathrm{scale}(c,x))$ for all $c>0$. A target $f:X\to\mathbb{R}$ is scale-invariant when $f(\mathrm{scale}(c,x))=f(x)$ for $c>0$. The main class theorem (the doubling decoy) shows that no joint-scale-invariant selector accepting the intended witness can force the posted value onto the scale-invariant target: from $S(f(x_0),x_0)$ one gets $S(2f(x_0),\mathrm{scale}(2,x_0))$, while $f(\mathrm{scale}(2,x_0))=f(x_0)\neq 2f(x_0)$.
proof idea
No proof body: this is a structure (Prop bundle) whose four fields are the class wall, the admission export, existence of some joint-scale-invariant selector, and a non-vacuous inhabited witness when $X$ is nonempty. Downstream, scaleHomogeneityNoGoCert fills the fields by applying no_scaleInvariantSelector_forces_value and forcingSelector_not_jointScaleInvariant (plus the positivity-selector witnesses for non-vacuity).
why it matters
This is the canonical public certificate form of the boundary theorem used in the paper "Recognition Composition and the Forced Skeleton". It packages what the uniqueness chain cannot do alone: no selection criterion blind to joint rescaling of a posted value and its carrier can fix an absolute value for a scale-invariant target. Hence at least one scale-bearing input is required beyond T0–T8.
The sole direct consumer is scaleHomogeneityNoGoCert, which inhabits the structure for an arbitrary ScaleAction. The ledger instantiation (MassGenesis.T10JointScaleHomogeneityNoGo) in the full library is an instance of the class theorem recorded here. The module also carries an amplitude form matching the paper's S5 statement (invariant selectors over a scaled configuration space force the selected amplitude set into ${0}$ or all of $\mathbb{R}_{>0}$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.