scale_perturbed_low
plain-language theorem explainer
The theorem shows that a level sequence perturbed above a cutoff index j remains unchanged at and below j. Researchers deriving hierarchical structures from zero-parameter conditions in Recognition Science cite this when controlling the support of a single-ratio perturbation. Its proof is a direct unfolding of the piecewise definition combined with rewriting on the index inequality.
Claim. Let $f : ℕ → ℝ$ be a sequence of levels, let $j ∈ ℕ$, $t ∈ ℝ$, and let $k ∈ ℕ$ satisfy $k ≤ j$. Define the perturbed sequence $f'$ by $f'(m) = f(m)$ for $m ≤ j$ and $f'(m) = f(m) exp(t)$ for $m > j$. Then $f'(k) = f(k)$.
background
The module develops Gap 2 of the axiom-closure plan: forcing hierarchical structure from a nontrivial zero-parameter ledger. It supplies an auxiliary perturbation that multiplies every level above index j by exp(t), changing only the ratio at j while preserving positivity for every real t and leaving all other ratios fixed. The local theoretical setting is analytic exploration of non-uniform scalings prior to proving that uniform ratios alone satisfy the zero-parameter condition.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the piecewise definition of the perturbed sequence and rewrites the conditional using the hypothesis that k ≤ j, selecting the unperturbed branch.
why it matters
This lemma secures the lower part of any perturbed sequence, enabling clean isolation of a single ratio change. It directly supports the injectivity argument for the family of perturbations listed in the module. In the Recognition framework it contributes to the derivation that uniform scaling is forced, by allowing controlled variation above j without disturbing the base of the hierarchy; it touches the self-similar fixed-point step in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.