IsInvariantSelector
plain-language theorem explainer
An invariant selector is a property of configurations that is blind to positive rescaling: it holds of a point exactly when it holds of every scaled copy. Anyone citing the amplitude-form scale-homogeneity no-go uses this predicate class as the hypothesis on the selection criterion. The body is a pure definitional biconditional under the positive-real scaling action on the carrier.
Claim. A selector $P$ on a scaled configuration space is invariant when, for every positive real $c>0$ and every configuration $x$, one has $P(c\cdot x)$ if and only if $P(x)$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton, stated in neutral vocabulary. The uniqueness chain (T-2 through T8) builds the skeleton without a preferred scale; this file proves abstractly why the chain cannot fix an absolute value on its own. The carrier $X$ is any type with a positive-real scaling action, and an amplitude $A$ of degree one may be attached.
A selector is simply a predicate $P:X\to\mathrm{Prop}$ that picks out admissible configurations. Invariance means $P$ cannot tell $x$ from $c\cdot x$ for any $c>0$. The module also treats a joint form (posted value against a scale-invariant target); the present definition is the single-predicate form used by the amplitude-form statement S5.
Two concrete witnesses (real pairs with squared ratio; eight-component complex vectors with a probability weight) instantiate the abstract hypotheses elsewhere in the file, so the no-go is a general fact about scale-blind selection rather than a quirk of one carrier.
proof idea
Pure definition: no tactics and no lemmas. The predicate unfolds to the single biconditional $\forall, c>0,, x,; P(c\cdot x)\leftrightarrow P(x)$, quantifying over the subtype of positive reals and the carrier of the scaled space.
why it matters
This is the hypothesis class for the paper's S5 amplitude-form boundary theorem. Downstream, selected_amplitudes_eq_zero_or_all_pos takes an invariant selector and concludes that the selected amplitude set is either contained in ${0}$ or contains every positive real. From that dichotomy, no_forced_positive_amplitude shows an invariant selector satisfied somewhere cannot force every selected configuration to carry one fixed positive amplitude. The positive-quadrant witness quadrantSelector_invariant is proved by direct cancellation under the scaling action, pinning the scale-invariant ratio $a/b=2$ while leaving amplitude free.
In the Recognition framework this marks the edge of the forcing chain (T0–T8): without at least one scale-bearing input, no scale-blind criterion can select a unique absolute amplitude. The ledger instantiation lives elsewhere as an instance of the class theorem proved here; the present definition is the public, type-agnostic interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.