ScalePerturbed
ScalePerturbed defines a modified level sequence that multiplies every entry above index j by exp(t), leaving lower entries unchanged. Analysts proving that zero-parameter ledgers force uniform ratios cite this construction to vary one inter-level ratio continuously while preserving positivity. The definition is a direct conditional expression on the index comparison with no auxiliary lemmas.
claimFor a level sequence $(l_k)_{k∈ℕ}$, cutoff index $j∈ℕ$, real parameter $t∈ℝ$, and evaluation index $k∈ℕ$, the perturbed value equals $l_k$ when $k≤j$ and equals $l_k·exp(t)$ otherwise.
background
The HierarchyForcing module treats the second gap in the axiom-closure plan: deriving hierarchical structure from a nontrivial zero-parameter ledger. ScalePerturbed supplies the explicit perturbation tool that shifts all levels above a chosen position j by the factor exp(t), thereby varying the single ratio at j continuously while leaving all other ratios and positivity intact for any real t.
proof idea
The definition is a direct case distinction: if k ≤ j then return the original level value, else return the original value multiplied by Real.exp t. No lemmas or tactics are applied; the expression is written as a single if-then-else on the natural-number comparison.
why it matters in Recognition Science
The construction supplies the analytic device used by scale_perturbed_family_injective, scale_perturbed_pos and scale_perturbed_low, which together establish that different parameters produce distinct positive sequences. These results feed realized_hierarchy_forces_phi, the end-to-end theorem that a realized hierarchy on a closed observable framework forces the scale ratio to equal φ, the self-similar fixed point of the forcing chain (T6). The perturbation therefore closes part of the route from zero-parameter ledgers to the eight-tick octave without introducing external moduli.
scope and limits
- Does not prescribe any particular form for the unperturbed level sequence.
- Does not enforce or derive uniformity of ratios.
- Does not depend on ledger axioms beyond ordinary real arithmetic.
- Does not constrain the admissible values of the free parameter t.
formal statement (Lean)
44noncomputable def ScalePerturbed (levels : ℕ → ℝ) (j : ℕ) (t : ℝ) (k : ℕ) : ℝ :=
proof body
Definition body.
45 if k ≤ j then levels k else levels k * Real.exp t
46
47/-- Every perturbed level is positive. -/