scale_perturbed_low
plain-language theorem explainer
The theorem shows that a level sequence perturbed by a factor exp(t) above index j agrees exactly with the original sequence at every position k at most j. Researchers analyzing stability of hierarchical ratios in zero-parameter ledgers cite this when isolating the effect of a single ratio change. The argument is a direct one-line expansion of the conditional definition followed by a rewrite on the ordering hypothesis.
Claim. Let $levels : ℕ → ℝ$ be a level sequence, $j ∈ ℕ$, $t ∈ ℝ$, and $k ∈ ℕ$ with $k ≤ j$. Then the perturbed value at position $k$ equals the original value $levels(k)$.
background
ScalePerturbed is the explicit construction that leaves every entry at or below index j unchanged while multiplying every later entry by exp(t). This changes only the ratio at position j while keeping all other ratios fixed and all values positive for any real t. The module places this construction inside the second gap of the axiom-closure plan, where a nontrivial zero-parameter ledger is shown to force hierarchical structure. The perturbation supplies an analytic device for continuously varying one ratio without leaving the positive reals.
proof idea
The proof is a one-line wrapper. It unfolds the definition of ScalePerturbed and rewrites the conditional using the hypothesis that k ≤ j, selecting the unperturbed branch.
why it matters
The result anchors the perturbation machinery listed in the module documentation for analytic use when deriving uniform scaling. It supports sibling statements on family injectivity and positivity by fixing the lower levels under the perturbation. In the Recognition framework it contributes to the step from zero-parameter ledgers to forced hierarchy by isolating how a single ratio variation affects the sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.