ConfigProps
plain-language theorem explainer
ConfigProps cfg asserts that the time-epsilon parameter of cfg lies in the closed interval [0,1]. Gravity modelers cite it when proving nonnegativity and reference identities for the time kernel w_t. The declaration is a direct structure definition consisting of two field inequalities.
Claim. Let $cfg$ be a configuration with time parameter $eps_t$. Then ConfigProps($cfg$) holds if and only if $0 ≤ eps_t ≤ 1$.
background
In the Gravity.ILG module, Config is the structure holding five real parameters: upsilonStar, eps_r, eps_v, eps_t, eps_a. ConfigProps isolates the two inequalities that bound the time parameter eps_t. The upstream Config from Modal.Possibility describes a point in recognition state space, with a positive real value and a time coordinate in ticks.
proof idea
This is a structure definition with no proof body. It directly encodes the two inequalities eps_t_nonneg and eps_t_le_one as fields of the Prop.
why it matters
ConfigProps is required by defaultConfig_props, w_t_nonneg_with, and w_t_ref_with to establish nonnegativity and reference identities for the time kernel. It supplies the parameter constraint step inside the ILG gravity development and indirectly supports the eight-tick octave structure through the time-kernel construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.