defaultConfig_props
plain-language theorem explainer
The lemma verifies that the default configuration meets the non-negativity and unit upper bound on its time-error parameter eps_t. Modelers instantiating the ILG gravity framework for baseline calculations would cite this result to justify use of the preset values. The proof proceeds as a one-line wrapper applying norm_num to the two field inequalities.
Claim. The default configuration satisfies $0 ≤ ε_t ≤ 1$.
background
ConfigProps is the structure asserting that a configuration cfg has its eps_t parameter satisfying 0 ≤ eps_t and eps_t ≤ 1. The defaultConfig is defined with eps_t set to 0.01, along with other small error tolerances. This lemma sits in the Gravity.ILG module, which handles parameter configurations for the ILG model.
proof idea
The proof is a one-line wrapper that refines the goal into the two inequalities from ConfigProps and discharges them via norm_num.
why it matters
This result supports downstream lemmas such as w_t_nonneg and w_t_ref, which rely on the default configuration satisfying the bounds to establish non-negativity of w_t and its reference value of 1. It fills the role of verifying the preset parameters in the ILG gravity setup.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.