kernel_correction_positive
plain-language theorem explainer
The theorem shows that for any positive real numbers C, α and ratio the product C times ratio to the power α is strictly positive. Model builders examining power-law kernel corrections in modified gravity or causal closure at solar-system distances would invoke this to confirm the sign of the deviation term w-1. The proof is a direct one-line term application of the standard positivity rules for real multiplication and exponentiation.
Claim. Let $C,α,ratio>0$. Then $C·ratio^α>0$.
background
The result sits inside the CausalClosure section of the DIF papers. It concerns the extrapolated kernel correction w-1=C·(r/r₀)^α at solar-system scales. The statement assumes no ultraviolet cutoff and records that the power-law form carries no built-in suppression. No upstream lemmas from the Recognition Science core are invoked; the argument rests only on the ordered field properties of the reals.
proof idea
The proof is a one-line term-mode wrapper that applies mul_pos to the hypothesis hC together with the positivity of the real power supplied by Real.rpow_pos_of_pos on hratio and α.
why it matters
The declaration formalizes the solar-system tension identified in the paper: the power-law kernel correction remains positive for all positive ratios and therefore exceeds PPN bounds when extrapolated without regularization. It supplies a basic positivity fact inside the DIF causal-closure development but does not yet link to the J-uniqueness or phi-ladder steps of the main forcing chain. No downstream theorems currently depend on it in the rendered graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.