Params
plain-language theorem explainer
The Params structure supplies a minimal record holding the fine-structure constant alpha and the ILG lag constant Clag for use in ILG modules outside the Relativity core. Researchers working on flight geometry or gravity models cite this record to instantiate parameters without pulling in the full Relativity subtree. The definition is a direct structure declaration with default values alpha set to 1 and Clag set to 0.
Claim. The structure Params consists of two real-valued fields: alpha : ℝ with default value 1 (the fine-structure constant α_EM) and Clag : ℝ with default value 0 (the lag parameter equal to φ^{-5}).
background
In the ILG.Params module the structure provides the minimal interface for ILG computations. The field alpha is the fine-structure constant drawn from Constants.Alpha.alpha, defined as 1/alphaInv. The field Clag is drawn from Constants.ILG.Clag and equals 1/φ^5 in RS-native units. A parallel but sealed structure appears in Relativity.ILG.Params; the present version is intended for modules outside that subtree. Upstream, UniversalForcingSelfReference.for supplies the meta-realization context while Gravity.ILG.Params and Spiral.SpiralField.Params supply the richer variants that downstream code may extend.
proof idea
The declaration is a direct structure definition that supplies the two fields together with their default values; no tactics or lemmas are applied.
why it matters
This record serves as the parameter interface for ILG computations feeding lemmas in Flight.Geometry (kappa_discreteness, perTurn_ratio, stepRatio_logSpiral_closed_form) and Gravity.ILG.ParamProps. It supplies the minimal alpha and Clag = φ^{-5} slot required by the phi-ladder and the alpha band (137.030, 137.039) while remaining outside the sealed Relativity subtree. The structure therefore closes the minimal-parameter gap between the forcing chain (T5 J-uniqueness, T6 phi fixed point) and concrete flight or gravity models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.