ScaledConfigSpace
plain-language theorem explainer
A scaled configuration space packages a carrier type with a multiplicative positive-real action and a nonnegative amplitude that scales linearly. It is the ambient setting for the amplitude-form boundary theorem: invariant selectors cannot pin a unique positive amplitude. Anyone citing the S5 no-go or the positive-quadrant witness uses this structure. The declaration is pure data (fields and axioms), not a proved statement.
Claim. A scaled configuration space consists of a carrier type $X$, a multiplicative action of $\mathbb{R}_{>0}$ on $X$ (identity at scale $1$, and $\mathrm{scale}(cd)=\mathrm{scale}(c)\circ\mathrm{scale}(d)$), together with a nonnegative amplitude $A:X\to\mathbb{R}$ that is homogeneous of degree one: $A(\mathrm{scale}(c)\,x)=c\,A(x)$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton, stated 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. Any selection criterion blind to joint rescaling that accepts an intended witness also accepts a doubled decoy whose posted value misses the target, so at least one scale-bearing input is required.
A scaled configuration space is the carrier for the amplitude form of that argument. The positive reals act multiplicatively on an arbitrary type $X$, and the amplitude $A$ is nonnegative and degree-one homogeneous under that action. The module is deliberately type-agnostic: ordinary witnesses (real pairs with a squared ratio; eight-component complex vectors with a probability weight) instantiate the same interface.
This is the public form used in "Recognition Composition and the Forced Skeleton". The ledger instantiation lives elsewhere as an instance of the class theorem proved here.
proof idea
No proof body: the declaration is a structure bundling a carrier, a positive-real scaling action with unital and multiplicative laws, and a nonnegative degree-one amplitude. Downstream constructions (for example the positive quadrant) fill the fields and discharge the field equations by direct computation with ext and simp.
why it matters
This structure is the ambient type for the paper's S5 amplitude-form no-go. Downstream, no_forced_positive_amplitude uses it to conclude that an invariant selector satisfied somewhere cannot force every selected configuration to share one fixed positive amplitude: the selected amplitude set is either ${0}$ or all of $\mathbb{R}_{>0}$. The positive-quadrant instance quadrantSpace supplies a concrete witness that pins a scale-invariant ratio while leaving amplitude free.
In the Recognition framework this marks the edge of the forcing chain (T0–T8): the skeleton is scale-free, and absolute scales (masses, couplings) require an external scale-bearing input. The module states the obstruction once, abstractly, before ledger-specific instantiations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.