module module moderate

`IndisputableMonolith.Foundation.ScaleHomogeneityNoGo`

Scale-homogeneity no-go for selectors on a positive-real scale action: any selector that is jointly scale-invariant cannot force a unique value, while the natural forcing selector fails joint scale invariance. Physicists citing uniqueness of the RS cost or fixed point use this to rule out pure scale-homogeneous selection. The module packages the action laws, invariance predicates, contrasting selectors, and a certificate recording the dichotomy.

claimOn a carrier $X$ with a positive-real scaling action $\lambda\cdot x$ obeying the usual action laws, no jointly scale-invariant selector forces a unique value; the forcing selector is not jointly scale-invariant, while the positivity selector is jointly scale-invariant yet does not force a value.

background

Recognition Science forces its cost and fixed point from structural axioms rather than free parameters. A recurring obstruction is pure scale homogeneity: if a selection rule is invariant under simultaneous rescaling of all positive-real data, it cannot pin down a unique numerical value.

This module formalizes a positive-real scaling action on a carrier $X$, with action laws written so instances cannot hide state-dependent rescaling. It defines scale invariance of a single map and joint scale invariance of a selector, then introduces two contrasting selectors: a forcing selector that would pick a unique value, and a positivity selector that only retains the positive cone.

The local setting is foundational (pre-physics): the no-go is combinatorial and algebraic, not dynamical. It sits upstream of uniqueness arguments for the $J$-cost and the self-similar fixed point $\varphi$ in the forcing chain.

proof idea

The module is theorem-bearing, not a pure definition dump. It first records the scale-action structure and the two invariance predicates. It then proves the dichotomy in two directions: (i) any jointly scale-invariant selector fails to force a unique value; (ii) the forcing selector is not jointly scale-invariant. A separate positivity selector is shown to be jointly scale-invariant yet non-forcing, supplying a concrete witness that invariance and forcing pull apart. A certificate structure packages the pair of facts for downstream consumption. Arguments are direct equational and quantifier manipulations on the action laws; no analytic estimates.

why it matters in Recognition Science

The no-go blocks a natural escape from the RS forcing chain: one cannot obtain unique constants (cost shape, $\varphi$, octave period, dimension) by a purely scale-homogeneous selection rule on positive data. Downstream uniqueness results for $J$ (T5) and the self-similar fixed point $\varphi$ (T6) rely on breaking pure scale symmetry, typically via the Recognition Composition Law or normalization conventions. The certificate gives a reusable interface so later modules can cite the dichotomy without replaying the selector algebra. In the broader framework it explains why RS must introduce a non-homogeneous structure (composition law, discrete tick, or defect) rather than scaling alone.

scope and limits

Does not construct the $J$-cost or prove its uniqueness (T5).
Does not force $\varphi$ or the eight-tick octave; only rules out pure scale selection.
Does not treat spacetime diffeomorphisms or dimensionful unit changes beyond $\mathbb{R}_{>0}$ scaling.
Does not claim every non-invariant selector forces a value.
Does not address measure-theoretic or probabilistic selectors.

declarations in this module (31)

structure ScaleAction L49
def IsJointScaleInvariantSelector L62
def IsScaleInvariant L67
theorem no_scaleInvariantSelector_forces_value L75
theorem forcingSelector_not_jointScaleInvariant L90
def PositivitySelector L100
theorem positivitySelector_jointScaleInvariant L102
theorem positivitySelector_does_not_force_value L112
structure ScaleHomogeneityNoGoCert L121
theorem scaleHomogeneityNoGoCert L138
def pairScaleAction L153
def pairRatio L159
theorem pairRatio_scaleInvariant L161
theorem pair_witness L170
def vecScaleAction L180
def probWeight L187
theorem probWeight_scaleInvariant L190
theorem vec_witness L204
structure ScaledConfigSpace L235
def IsInvariantSelector L251
theorem selected_amplitudes_eq_zero_or_all_pos L256
theorem no_forced_positive_amplitude L277
def quadrantSpace L294
def quadrantSelector L305
theorem quadrantSelector_invariant L307
def quadrantPoint21 L322
theorem quadrantPoint21_selected L325
theorem quadrantPoint21_amplitude L329
theorem quadrant_witness L331
theorem quadrant_ratio_pinned L343
theorem quadrant_ratio_scaleInvariant L350