Birge ratio under an expansion factor: $R_B \mapsto R_B/f$

Disclosure - non-blind read-back. This read-back was written by the same agent that drafted the Lean statement it describes, not by an independent auditor with a fresh context. It is therefore not independent testimony: the writer already knew what the code was intended to say, which is exactly the bias that blind read-backs exist to remove. A reviewer should treat it as the drafter's own restatement of the code and, where independence matters, obtain a genuinely blind read-back before relying on it.

The statement quantifies over three real numbers, called here $\chi^2$, $\nu$ and $f$, and assumes $\chi^2 \ge 0$, $\nu > 0$ and $f > 0$. With $R_B(a,b) = \sqrt{a/b}$ (the real square root, which returns $0$ on negative arguments), the conclusion is

Here $\chi^2$ and $\nu$ are unconstrained real numbers subject only to the sign hypotheses - no connection to any matrix, data set or fit is asserted, and $\nu$ is a real number rather than an integer count. The claim is the elementary scaling law of the square root under division by $f^2$; the hypotheses $\chi^2\ge0$ and $\nu>0$ keep the radicand nonnegative so that no truncation of the square root occurs, and $f>0$ makes $\sqrt{f^2} = f$.