form_factor_correction
plain-language theorem explainer
form_factor_correction defines the Recognition Science form factor correction as the algebraic expression 1 - 0.15 (Q/L)^2. Physicists addressing the proton radius puzzle cite it when inserting the standard dipole approximation into low-momentum calculations. The definition is a direct one-line expression with no further reduction steps.
Claim. The form factor correction is given by $1 - 0.15 (Q/L)^2$, where $Q$ is the momentum transfer and $L$ is a positive length scale.
background
The module derives the proton charge radius within Recognition Science, following the paper RS_Proton_Radius_Puzzle.tex. It supplies a quadratic correction drawn from the standard dipole form factor for use at small momentum transfers. Upstream Ledger definitions from Recognition and Cycle3 establish conserved debit-credit structures that underlie length scales appearing in the proton-radius formulas.
proof idea
The definition is a one-line algebraic expression implementing the standard dipole form factor correction.
why it matters
The definition is invoked by form_factor_near_one to bound the deviation from unity when (Q/L)^2 is at most 0.01. It supplies the explicit dipole term required by the proton-radius derivation in RS_Proton_Radius_Puzzle.tex. Within the Recognition framework the expression connects to length scales generated by the phi-ladder and J-cost structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.