ScaleAction
plain-language theorem explainer
A monoid action of the multiplicative reals on an arbitrary carrier X: scaling by 1 is the identity, and scaling composes as multiplication of factors. Anyone stating the scale-homogeneity no-go cites this as the neutral interface for joint rescaling. It is a pure structure package; the two equational fields block state-dependent smuggling.
Claim. A scale action on a type $X$ is a map $\mathrm{scale}:\mathbb{R}\to X\to X$ such that $\mathrm{scale}(1,x)=x$ for all $x$, and $\mathrm{scale}(c\cdot d,x)=\mathrm{scale}(c,\mathrm{scale}(d,x))$ for all $c,d\in\mathbb{R}$ and $x\in X$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton in neutral vocabulary. The uniqueness chain (T-2 through T8) derives the skeleton without a scale; this file shows abstractly why the chain cannot fix an absolute value by itself: any selector blind to joint rescaling of a posted value and its carrier that accepts an intended witness also accepts a doubled decoy.
The carrier $X$ is deliberately type-agnostic. A scale action equips $X$ with a positive-real (in practice) monoid action written as a binary map $\mathbb{R}\times X\to X$. The two laws are the monoid-action axioms for $(\mathbb{R},\times)$: unit and associativity via multiplication of scale factors. Recording them in the structure prevents instances from inserting state-dependent or non-homomorphic rescaling.
Downstream the same interface is instantiated on real pairs (componentwise scaling) and on eight-component complex vectors (pointwise complex scaling), matching the paper's witnesses for squared ratios and probability weights.
proof idea
No proof body: this is a structure declaration. The fields are the action map together with the two equational axioms (identity at scale factor 1, and multiplicativity). Instances discharge the axioms by ext/funext and elementary algebra (simp, mul_assoc, ring).
why it matters
This is the carrier interface for the whole ScaleHomogeneityNoGo development. The certificate structure ScaleHomogeneityNoGoCert and the packaged theorem scaleHomogeneityNoGoCert quantify over an arbitrary ScaleAction; the class wall states that no jointly scale-invariant selector can force a scale-invariant target to a unique posted value.
Concrete instances pairScaleAction (componentwise on $\mathbb{R}\times\mathbb{R}$) and vecScaleAction (pointwise on $\mathrm{Fin},8\to\mathbb{C}$) feed the non-vacuity witnesses: squared first-component share and first-component probability weight, both invariant under joint scaling. Those witnesses pin the paper's S5 / amplitude form and the ledger instantiation MassGenesis.T10JointScaleHomogeneityNoGo.
In the Recognition framework this is the abstract reason the forcing chain stops short of an absolute scale: T5–T8 fix $J$, $\varphi$, the eight-tick octave, and $D=3$, but absolute units require at least one scale-bearing input. The structure keeps that boundary statement carrier-independent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.