quadrantPoint21_amplitude
plain-language theorem explainer
The positive-quadrant witness point (2,1) has amplitude exactly 2 under the first-coordinate amplitude map. Anyone citing the amplitude-form no-go (paper S5) or the quadrant witness needs this evaluation. The proof is pure definitional equality by reflexivity.
Claim. On the positive quadrant $\{(a,b)\in\mathbb{R}_{>0}\times\mathbb{R}_{>0}\}$ with amplitude $A(a,b)=a$, the witness point $(2,1)$ satisfies $A(2,1)=2$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton: after the uniqueness chain (T-2 through T8) builds a scale-free theory, no joint-scale-blind selector can pin an absolute value. The amplitude form restates paper S5: over a scaled configuration space (a positive-real action with a degree-one homogeneous amplitude), an invariant selector either forces amplitude 0 or accepts every positive amplitude.
The positive quadrant supplies the concrete carrier. Configurations are pairs $(a,b)$ with both coordinates positive; scaling multiplies both by $c>0$; amplitude is the first coordinate. The witness point is the subtype element $(2,1)$. The ratio $a/b=2$ is scale-invariant, while the amplitude itself is free under joint rescaling.
proof idea
One-line reflexivity. By definition of the quadrant scaled configuration space, amplitude is projection onto the first coordinate, and the witness is literally the pair $(2,1)$, so $A(2,1)=2$ holds by rfl.
why it matters
Feeds quadrant_witness, which packages the positive-quadrant instance of the amplitude-form no-go: the selector accepts $(2,1)$ with positive amplitude, yet does not force every selected amplitude to equal 2. That witness pins the scale-invariant ratio while leaving amplitude free, exactly the S5 statement in the paper "Recognition Composition and the Forced Skeleton".
In the broader RS chain this is the abstract reason the skeleton cannot fix absolute scales on its own: at least one scale-bearing input is required beyond T0–T8. The ledger-level instance lives elsewhere; this module is the type-agnostic public form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.