ScalingModel
plain-language theorem explainer
ScalingModel packages a real exponent gamma with a two-argument function f obeying the homogeneity rule f(c t1, c t2) = f(t1, t2) for every c > 0. Workers on ratio predictions inside the MRD scaling layer cite this structure to parameterize homogeneous scaling. The declaration is a bare structure definition carrying no proof obligations or computational content.
Claim. A scaling model consists of a real number $gamma$ and a function $f : mathbb{R} to mathbb{R} to mathbb{R}$ satisfying $f(c t_1, c t_2) = f(t_1, t_2)$ for all $c > 0$.
background
The module TruthCore.MRD.Scaling supplies the carrier type for homogeneous scaling laws used in ratio calculations. Upstream gamma symbols appear as the Euler-Mascheroni constant in Constants.EulerMascheroni, as the fixed power-law exponent 3 in NetworkScience.SmallWorldFromSigma, and as the leading-order PPN parameter 1 in Relativity.ILG.PPN; the present structure treats gamma as an arbitrary real parameter. The homogeneity axiom on f is the only structural constraint and directly enables the scale-invariance property shown in the sibling rescale lemma.
proof idea
This is a structure definition with an empty proof body. The three fields are introduced directly: the real gamma, the function f, and the forall-quantified homogeneity condition f_hom0.
why it matters
ScalingModel serves as the input type for the downstream predicted_ratio definition, which assembles the ratio ((tau_m1 / tau_m2)^gamma) * f(tau_m1/tau_f, tau_m2/tau_f). The same structure supports the predicted_ratio_rescale lemma that propagates the homogeneity condition into invariance under uniform rescaling. Within the Recognition Science framework it supplies the interface for scaling exponents in the MRD component, sitting between the general forcing chain and concrete mass-ratio predictions on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.