predicted_ratio_rescale
plain-language theorem explainer
The lemma establishes that the predicted ratio for a scaling model is invariant under uniform positive rescaling of its three time parameters. Cosmologists calibrating suppression factors would cite it to confirm unit independence in MRD models. The proof reduces the scaled expression to the unscaled one by canceling the common multiplier in each ratio and applying the model's homogeneity axiom.
Claim. Let $M$ be a scaling model with exponent $gamma$ and homogeneous function $f$. For $c>0$ and real numbers $tau_{m1}, tau_{m2}, tau_f$, the predicted ratio satisfies predicted_ratio$(M, c tau_{m1}, c tau_{m2}, c tau_f)$ = predicted_ratio$(M, tau_{m1}, tau_{m2}, tau_f)$.
background
A ScalingModel is a structure containing a real exponent gamma, a binary function f from reals to reals, and the homogeneity axiom that f(c t1, c t2) equals f(t1, t2) for every c>0. The predicted ratio is defined as the product of (tau_m1 over tau_m2) raised to gamma and f applied to the two ratios against tau_f. This lemma sits inside the MRD scaling module, which supplies the scale-free properties required by the suppression ratio defined in the cosmology section.
proof idea
The proof unfolds the definition of predicted_ratio, then uses field_simp three times to show that each pairwise ratio of the scaled taus equals the corresponding unscaled ratio. It next invokes the homogeneity axiom f_hom0 (with the supplied one_mul lemma) to equate the f values on the scaled and unscaled ratio pairs, after which substitution yields equality.
why it matters
The result guarantees that the predicted ratio fed into Sigma8Suppression remains unchanged under choice of time units, closing a basic invariance step before calibration to observations. It directly supports the suppression factor computation by ensuring the MRD scaling expression is well-defined on ratios alone. No downstream theorems are recorded yet, leaving open its precise insertion point in the full cosmology pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.