scale_perturbed_family_injective
plain-language theorem explainer
scale_perturbed_family_injective establishes that distinct real parameters t produce distinct perturbed level sequences when the base level at j+1 is positive. Analysts studying continuous deformations of hierarchies cite it to justify parameter variation without sequence collapse. The proof evaluates the equality at the single perturbed index, cancels the nonzero multiplier, and applies injectivity of the real exponential.
Claim. Let $(levels_k)_{k}$ be a sequence of reals with $levels_{j+1}>0$. Define the perturbed sequence by $levels'_k = levels_k$ for $k≤j$ and $levels'_k = levels_k·e^t$ for $k>j$. Then the map $t↦$ perturbed sequence is injective.
background
ScalePerturbed is the explicit map that multiplies every level index strictly above a chosen position j by the factor exp(t). This construction changes only the single ratio at j while keeping all other ratios fixed and preserving positivity for any real t. The module places the result inside Gap 2 of the axiom-closure plan, whose goal is to derive hierarchical structure from a zero-parameter ledger condition. The single upstream dependency is the definition of ScalePerturbed itself.
proof idea
Assume two parameters t1 and t2 produce identical perturbed sequences. Apply congr_fun to the equality at index j+1. Unfold the definition and rewrite the two if-conditions to false using omega. Cancel the nonzero factor levels(j+1) via mul_left_cancel₀ (justified by ne_of_gt on the positivity hypothesis). Conclude t1=t2 by Real.exp_injective.
why it matters
The theorem supplies the injectivity half of the perturbation machinery required for analytic arguments in the hierarchy-forcing development. It guarantees that continuous variation of t yields genuinely distinct sequences, a prerequisite for later contradictions that force uniform ratios. The result therefore supports the derivation of uniform_scaling_forced from the zero-parameter ledger condition and sits inside the phase-3 closure that extracts H1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.