form_factor_near_one
plain-language theorem explainer
The theorem bounds the deviation of the Recognition Science dipole correction from unity by 0.0015 whenever the squared momentum transfer satisfies (Q/L)^2 ≤ 0.01 with L positive. Low-energy scattering analyses in the proton-radius program would invoke this estimate to control the error incurred by the standard dipole form factor. The proof substitutes the explicit algebraic definition of the correction and closes the inequality with nonnegativity, absolute-value identities, and linear arithmetic.
Claim. Let $Q,L$ be real numbers with $L>0$ and $(Q/L)^2≤0.01$. Then $|f(Q,L)-1|≤0.0015$, where the RS form-factor correction is the function $f(Q,L)=1-0.15(Q/L)^2$.
background
The module develops the proton charge radius inside Recognition Science, following the paper RS_Proton_Radius_Puzzle.tex. The key auxiliary definition is the form-factor correction $f(Q,L)=1-0.15(Q/L)^2$, which modifies the standard dipole ansatz by a quadratic term in momentum transfer. The length scale $L$ is taken positive and is compared with the momentum scale $Q$ to delineate the regime of validity. Upstream, the PrimitiveDistinction.from theorem supplies the structural conditions under which the Recognition framework operates, while the Ledger L objects in Recognition and Cycle3 supply the debit-credit bookkeeping used elsewhere in the monolith.
proof idea
The tactic proof first unfolds the definition of form_factor_correction, yielding the explicit expression 1-0.15(Q/L)^2. A positivity lemma establishes that 0.15(Q/L)^2 is nonnegative. Two ring and abs rewrites convert the absolute deviation into the nonnegative quantity 0.15(Q/L)^2. The final nlinarith step closes the bound using the hypothesis (Q/L)^2≤0.01.
why it matters
The result supplies a concrete numerical control on the dipole approximation inside the proton-radius calculation of the Recognition Science paper. It therefore supports the downstream estimates of the proton radius that appear as sibling declarations in the same module. Within the broader framework the bound illustrates how the Recognition Composition Law and the phi-ladder constrain low-energy electromagnetic observables once the length scale L is identified with a recognition yardstick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.