defaultConfig
plain-language theorem explainer
defaultConfig supplies the five numerical defaults for the ILG Config record: upsilonStar at 1 and the four epsilons at 1e-12, 1e-12, 0.01 and 1e-12. Gravity-module authors cite it to instantiate the parameter structure for every downstream kernel and lemma. The definition is a direct record literal with no reduction steps or external lemmas.
Claim. Let Config be the structure with fields upsilonStar, eps_r, eps_v, eps_t, eps_a : ℝ. Then defaultConfig is the instance with upsilonStar = 1, eps_r = 10^{-12}, eps_v = 10^{-12}, eps_t = 0.01, eps_a = 10^{-12}.
background
Config is the five-field record structure that holds the reference scaling upsilonStar together with the four recognition tolerances eps_r, eps_v, eps_t, eps_a. The ILG module uses this record to parameterize the time kernel and related gravity functions. The upstream Modal.Possibility.Config supplies a simpler single-value configuration for modal logic, but the ILG version specializes the fields for concrete numerical tolerances.
proof idea
The definition is a direct record construction that assigns the five literal real numbers to the Config fields. No tactics, lemmas or reductions are invoked.
why it matters
defaultConfig fixes the concrete tolerances that every w_t variant and its supporting lemmas (defaultConfig_props, eps_t_le_one_default, w_t_ge_one, w_t_nonneg) rely on. It therefore anchors the numerical layer of the ILG gravity model inside the Recognition framework, ensuring the time-kernel inequalities remain well-defined for the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.