ScalePerturbed
plain-language theorem explainer
ScalePerturbed defines a level sequence in which entries above index j are multiplied by exp(t) while lower entries remain fixed. Researchers deriving uniform ratios from zero-parameter ledgers cite this construction to vary one inter-level ratio continuously. The definition implements the shift through a direct conditional that applies the exponential only to higher positions.
Claim. Define the perturbed level at index $k$ by $levels(k)$ when $k ≤ j$ and by $levels(k) · e^t$ otherwise.
background
The HierarchyForcing module develops the second gap in the axiom-closure plan: passage from a nontrivial zero-parameter ledger to a forced hierarchical structure. ScalePerturbed supplies the explicit perturbation operator that multiplies every level above a chosen index j by exp(t), thereby varying the ratio at j continuously while leaving all other ratios and the positivity of every level unchanged for any real t.
proof idea
The definition is a direct conditional expression. When k ≤ j it returns the original level; otherwise it multiplies by Real.exp t. No lemmas or tactics are invoked.
why it matters
ScalePerturbed supplies the concrete perturbation used by scale_perturbed_pos, scale_perturbed_low and scale_perturbed_family_injective. These three results feed realized_hierarchy_forces_phi, the end-to-end theorem that extracts the scale ratio φ from any realized hierarchy on a closed observable framework. The construction therefore closes the analytic step required for uniform scaling in Phase 3 of Gap 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.