ScalePerturbed
plain-language theorem explainer
ScalePerturbed defines a level sequence modified by multiplying entries above index j by exp(t). Analysts of hierarchical emergence in Recognition Science cite it when constructing continuous deformations of ratio sequences. The definition uses a simple if-then branch on the index k relative to j.
Claim. For a sequence of levels $(levels_k)_{k∈ℕ}$, index $j$, parameter $t$, and index $k$, the perturbed value is $levels_k$ when $k≤j$, and $levels_k⋅e^t$ otherwise.
background
In HierarchyForcing, which addresses Gap 2 on forcing hierarchical structure from a zero-parameter ledger, the perturbation machinery allows analytic variation of ratios. ScalePerturbed shifts all levels above position j by the factor exp(t), changing the ratio at j to r_j ⋅ exp(t) while preserving positivity and other ratios for every t∈ℝ. This sits in Phase 3 of the axiom-closure plan alongside uniform_scaling_forced, which shows non-uniform inter-level ratios are incompatible with the zero-parameter condition. The canonical derivation of uniform ratios instead uses HierarchyRealization.realized_uniform_ratios from the ratio_self_similar field.
proof idea
The definition is implemented as a direct conditional: if k ≤ j then return levels k else return levels k * Real.exp t. No lemmas are applied; it is the base construction for subsequent properties.
why it matters
This definition supplies the perturbation tool required by scale_perturbed_family_injective, scale_perturbed_low, and scale_perturbed_pos. It supports the end-to-end theorem realized_hierarchy_forces_phi, which shows a realized hierarchy forces the scale ratio to be φ. It fills the analytic machinery in the module doc for Gap 2, enabling the proof that uniform ratios are forced without external hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.