ILGParams
plain-language theorem explainer
ILGParams packages the fine-structure constant alpha and lag coupling cLag as a global parameter record for the ILG scalar action. Workers on the covariant Lagrangian in Relativity.ILG.Action cite it to supply the two reals that scale the kinetic, mass, and coupling terms. The declaration is a bare structure definition equipped with an Inhabited instance and no proof obligations.
Claim. The structure ILGParams consists of two real numbers: alpha (the fine-structure constant) and cLag (the lag coupling constant), together with an Inhabited instance.
background
The Relativity.ILG.Action module re-exports geometry and field types to support construction of the ILG action. The sibling Index abbrev supplies symbolic natural-number tensor indices. Upstream, Constants.Alpha.alpha supplies the definition alpha := 1/alphaInv, while the PeriodicTable.Index structure records rail and block data for atomic indexing. The SimplicialLedger.ContinuumBridge.as structure identifies discrete Laplacian actions with continuum curvature terms.
proof idea
This is a structure definition with no proof body. The two fields are declared directly as real numbers and the Inhabited instance is derived automatically.
why it matters
ILGParams supplies the parameters consumed by bandsFromParams, L_coupling, L_cov, L_density, L_kin, L_mass, L_pot, and PsiActionP. It therefore anchors the toy Lagrangian L_density = (alpha^2)/2 - (cLag^2)/2 + cLag * alpha that appears in the covariant action S_cov = S_EH + integral L_cov. In the Recognition framework the bundle supports the ILG extension of the Einstein-Hilbert term downstream of the T0-T8 forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.