Config
plain-language theorem explainer
The Config structure supplies the five real parameters that instantiate the ILG gravity model inside the Recognition Science cost-function framework. Workers on additive cost theorems and calibration structures cite it when they need concrete gravitational instances of the general Config type. The declaration is a plain structure definition with no proof obligations or hidden hypotheses.
Claim. An ILG configuration is a 5-tuple of real numbers consisting of a distinguished scale factor $υ^*$ together with four dimensionless parameters $ε_r$, $ε_v$, $ε_t$, $ε_a$ that control radial, velocity, temporal and acceleration contributions to the cost.
background
In the Recognition Science setting a configuration is a point in recognition state space, introduced in the Modal.Possibility module as a simplified stand-in for a full LedgerState with a positive real value and time coordinate. The Gravity.ILG module specializes this notion by supplying the concrete parameters needed to evaluate gravitational cost functions. These parameters are then imported into the CostFromDistinction module, where they appear as the type argument to CostFunction and Calibration structures.
proof idea
The declaration is a structure definition; it introduces the five fields directly with no tactics or lemmas applied.
why it matters
This definition supplies the concrete type on which the additive cost theorems (additive_emp_left, additive_emp_right, additive_three, additive_strict_of_both_inconsistent) and the Calibration structure are stated. It therefore sits at the interface between the general modal Config and the recognition-work constraint theorem, allowing the framework's forcing chain and recognition composition law to be instantiated for gravitational distinctions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.