predicted_ratio
plain-language theorem explainer
predicted_ratio defines the scaling formula for the ratio of two mass times under a model M. Cosmologists studying sigma8 suppression cite it when linking recognition strain to weak-lensing observations. The definition is a direct algebraic expression that multiplies the power-law term by the f-evaluated ratio of scaled times.
Claim. For a scaling model $M$ with exponent $M.gamma$ and homogeneous function $M.f$, the predicted ratio is $((tau_{m1}/tau_{m2})^{M.gamma}) * M.f(tau_{m1}/tau_f, tau_{m2}/tau_f)$.
background
ScalingModel is a structure consisting of a real exponent gamma, a function f from reals to reals, and the homogeneity property that f(ct1, ct2) equals f(t1, t2) whenever c is positive. This definition lives in the TruthCore.MRD.Scaling module, which supplies scaling relations for mass-ratio dynamics inside the Recognition Science framework. Upstream results include the Euler-Mascheroni gamma constant, the fixed gamma=3 from network science, the PPN gamma scaffold set to 1, and recognition structures M from the Recognition and Cycle3 modules.
proof idea
This is a direct definition that assembles the expression by raising the ratio of tau_m1 to tau_m2 to the model's gamma power and multiplying by the model's f applied to the arguments normalized by tau_f. No lemmas or tactics are invoked; the body is the primitive expression.
why it matters
This definition supplies the core expression used by predicted_equals_observed, sigma8_match, and Sigma8SuppressionCert in the Cosmology.Sigma8Suppression module. It realizes the scaling component of the eight-tick octave mechanism, allowing the model to accommodate the observed sigma8 tension via strain calibrated to J-cost bounds near 0.118. It leaves open the concrete calibration of f to match specific phi-ladder values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.