pairScaleAction
plain-language theorem explainer
Componentwise multiplication by a real factor equips the plane with a positive-real scaling action. Anyone assembling the real-pair witness for the scale-homogeneity no-go cites this instance. The two action laws are discharged by componentwise extensionality plus associativity of real multiplication.
Claim. The assignment $(c,(x,y))\mapsto(c\cdot x,\,c\cdot y)$ is a scaling action of $\mathbb{R}$ on $\mathbb{R}\times\mathbb{R}$: scaling by $1$ is the identity, and scaling by a product equals successive scalings.
background
The module proves a boundary theorem for the forced skeleton: after the uniqueness chain (T-2 through T8) has fixed the scale-free structure, no selection criterion blind to joint rescaling of a posted value and its carrier can pin an absolute value for a scale-invariant target. The carrier is any type with a positive-real scaling action; concrete witnesses (real pairs, eight-component complex vectors) instantiate the abstract no-go.
A ScaleAction on a type $X$ is a map $\mathrm{scale}:\mathbb{R}\to X\to X$ obeying $\mathrm{scale},1=\mathrm{id}$ and $\mathrm{scale}(cd)=\mathrm{scale},c\circ\mathrm{scale},d$. The laws are recorded so instances cannot smuggle state-dependent rescaling. The present definition supplies that structure on real pairs by acting the same factor on both coordinates.
proof idea
Definitional instance of the scaling-action structure. The action map is componentwise multiplication. The unit law is proved by ext then simp on each coordinate. The multiplicative law is the same, with mul_assoc discharging the real-multiplication reassociation on each component.
why it matters
This is the carrier action for the real-pair witness of the scale-homogeneity no-go. Downstream, pairRatio_scaleInvariant shows that the squared first-component share is invariant under the action, and pair_witness feeds both facts into the abstract selector theorem to conclude that no positivity-style joint selector can force the posted value to equal that ratio. The module is the canonical public form of the boundary theorem in "Recognition Composition and the Forced Skeleton": the uniqueness chain cannot fix absolute scales without at least one scale-bearing input. The ledger-level mass-genesis instance is a specialization of the same class result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.