scale_perturbed_pos
The result shows that if every entry in a real sequence is positive then the sequence obtained by multiplying all terms after index j by exp(t) remains positive for any real t. Analysts of continuous deformations in hierarchical forcing would invoke it to guarantee that perturbed level sequences stay in the positive cone. The argument unfolds the piecewise definition and splits into the two cases k ≤ j and k > j, applying the input positivity hypothesis or multiplying it by the positivity of the exponential.
claimLet $(l_k)_{k=0}^∞$ be a sequence of positive reals. Fix $j∈ℕ$ and $t∈ℝ$. Define the perturbed sequence $l'_k$ by $l'_k=l_k$ when $k≤j$ and $l'_k=l_k⋅e^t$ otherwise. Then $l'_k>0$ for every $k$.
background
The module HierarchyForcing develops the second gap in the axiom-closure plan: passage from a nontrivial zero-parameter ledger to a forced hierarchical structure (H1). Within this setting the auxiliary definition ScalePerturbed supplies an explicit one-parameter family of deformations: it leaves levels 0 through j unchanged and multiplies every subsequent level by the positive factor exp(t). This construction changes only the single ratio at position j while preserving positivity for all real t, exactly the property needed for later injectivity statements on the family of perturbations.
proof idea
The proof is a direct term-mode case split. It unfolds the definition of ScalePerturbed, then branches on whether the index k satisfies k ≤ j. The first branch returns the hypothesis that the original sequence is positive at k; the second branch multiplies that same hypothesis by the fact that exp(t) > 0.
why it matters in Recognition Science
The theorem closes the positivity requirement for the perturbation machinery introduced in the module doc-comment. It therefore supports the analytic study of non-uniform scalings that is contrasted with the canonical uniform-ratio derivation (via HierarchyRealization.realized_uniform_ratios and no_moduli_forces_uniform_ratios). In the broader Recognition Science chain it belongs to the forcing steps that prepare the ground for the self-similar fixed point phi and the eight-tick octave structure.
scope and limits
- Does not assert preservation of any ratio or arithmetic relation beyond positivity.
- Does not restrict the perturbation parameter t to any interval.
- Does not address sequences that fail to be strictly positive at the outset.
- Does not claim uniqueness or minimality of the perturbed sequence.
formal statement (Lean)
48theorem scale_perturbed_pos (levels : ℕ → ℝ) (j : ℕ)
49 (h_pos : ∀ k, 0 < levels k) (t : ℝ) (k : ℕ) :
50 0 < ScalePerturbed levels j t k := by
proof body
Term-mode proof.
51 unfold ScalePerturbed
52 split
53 · exact h_pos k
54 · exact mul_pos (h_pos k) (Real.exp_pos t)
55
56/-- The perturbation fixes all levels at or below position `j`. -/