scale_perturbed_pos
plain-language theorem explainer
The declaration shows that any perturbation of a positive level sequence by multiplying entries above index j by exp(t) remains strictly positive for every real t. Researchers deriving hierarchical structures from zero-parameter ledgers cite it to keep perturbed sequences inside the positive domain required for ratio analysis. The term proof unfolds the piecewise definition and dispatches the two cases directly with the input positivity hypothesis together with the positivity of the exponential.
Claim. Let $(l_k)_{k∈ℕ}$ be a sequence of positive reals. For any $j,k∈ℕ$ and $t∈ℝ$, define the perturbed sequence by $˜l_k=l_k$ if $k≤j$ and $l_k⋅e^t$ otherwise. Then $˜l_k>0$.
background
The HierarchyForcing module closes Gap 2 of the axiom-closure plan by forcing nontrivial hierarchical structure from a zero-parameter ledger. ScalePerturbed is the explicit analytic tool that shifts every level above position j by the factor exp(t), changing only the ratio at j while leaving all other ratios and the positivity of every level unchanged for arbitrary real t. The module documentation states that this construction is supplied for continuous deformation studies that later derive uniform ratios via HierarchyRealization.realized_uniform_ratios.
proof idea
The proof is a one-line term wrapper. It unfolds ScalePerturbed, splits on the defining if-then-else, and applies the hypothesis that every original level is positive in the first branch; in the second branch it invokes the product-positivity lemma together with the fact that exp(t) is positive.
why it matters
The result underwrites the perturbation machinery described in the module documentation for analytic exploration of inter-level ratios. It guarantees that every member of the perturbed family stays positive, a prerequisite for later injectivity statements and for the canonical derivation of uniform scaling as the unique zero-parameter solution. Within the Recognition framework it supports the step from nontrivial ledger to self-similar hierarchy without introducing extra parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.