quadrantSpace
plain-language theorem explainer
The open positive quadrant is packaged as a scaled configuration space: positive reals dilate both coordinates jointly, and amplitude is the first coordinate. Anyone citing the paper's S5 amplitude-form no-go, or the a=2b witness, uses this carrier. Structure obligations reduce to positivity and associativity of real multiplication (mul_pos, mul_assoc, rfl).
Claim. Let $X=\{(a,b)\in\mathbb{R}\times\mathbb{R}:a>0,\,b>0\}$. Define the action $c\cdot(a,b)=(ca,cb)$ for $c>0$ and the amplitude $A(a,b)=a$. Then $(X,\cdot,A)$ is a scaled configuration space: the action is unital and multiplicative, $A\ge 0$, and $A(c\cdot x)=c\,A(x)$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton: after the uniqueness chain (T-2 through T8) derives the theory without a scale, no selection criterion blind to joint rescaling of a posted value and its carrier can fix an absolute value for a scale-invariant target. The amplitude form restates paper S5 over a scaled configuration space.
A scaled configuration space is a carrier $X$ with a multiplicative $\mathbb{R}_{>0}$-action (unital and associative) and a nonnegative amplitude readout homogeneous of degree one. The positive quadrant is the ordinary mathematical witness used to pin a scale-invariant ratio while leaving amplitude free; a second witness (eight-component complex vectors) shows the no-go is carrier-agnostic.
proof idea
Field-by-field structure instance, not a deep proof. Carrier is the subtype of pairs with both coordinates positive. Scaling multiplies both coordinates by the positive factor; image positivity is mul_pos on each factor. Unitality and multiplicativity are discharged by subtype extensionality plus simp with mul_assoc. Amplitude is first-coordinate projection; nonnegativity is le_of_lt on the subtype witness; homogeneity is definitional (rfl).
why it matters
This is the paper's positive-quadrant witness carrier for the amplitude-form Scale Homogeneity No-Go (S5). Downstream it hosts quadrantSelector (the predicate $a=2b$), the point $(2,1)$, the pinning theorem that every selected configuration has ratio $a/b=2$, and the proof that the selector is invariant under joint scaling. Those facts instantiate the abstract dichotomy: an invariant selector's selected amplitude set is contained in ${0}$ or contains every positive real. The module is the canonical public form of the boundary theorem in "Recognition Composition and the Forced Skeleton," sitting after T-2--T8, which cannot fix a scale on their own.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.