Params
plain-language theorem explainer
Minimal parameter record for ILG in the relativity subtree supplies default values alpha equal to one and Clag equal to zero. Flight geometry and gravity modules cite this record to fix the fine-structure constant and the phi-derived lag term when instantiating log-spiral and rotor calculations. The declaration is a direct structure definition that embeds the upstream constant defaults without additional constraints or proof steps.
Claim. A parameter structure consisting of the fine-structure constant field with default value 1 and the ILG lag constant field with default value 0.
background
The Relativity.ILG.Params module isolates a minimal parameter record for the sealed relativity subtree. It draws its alpha default from the fine-structure constant definition, documented as the fine-structure constant (α_EM), and its Clag default from the ILG constant module, given explicitly as one over phi to the fifth power. Parallel structures exist in the general ILG.Params module and the fuller Gravity.ILG.Params that adds fields A, r0 and p. The local setting supplies a lightweight interface for relativistic extensions of the ILG framework while inheriting constants from the phi-ladder.
proof idea
The declaration is a direct structure definition that assigns the two default values. It references the alpha definition from Constants.Alpha and the Clag definition from Constants.ILG to establish the embedded defaults.
why it matters
This record supplies the parameter type for thirty-seven downstream declarations, including kappa_discreteness, perTurn_ratio and stepRatio_logSpiral_closed_form in Flight.Geometry. Those lemmas establish discrete pitch families via integer shifts of kappa and closed-form step ratios on the log-spiral. In the Recognition framework it anchors the constants alpha and Clag that enter the phi-ladder mass formulas, the eight-tick octave scaling and the alpha band. It fills the minimal interface requirement for relativity ILG parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.