eps_t_le_one_default
plain-language theorem explainer
The lemma confirms that the default time-error tolerance in the ILG configuration satisfies the unit bound. Implementers of the Recognition Science gravity model cite it to certify the standard parameter set before invoking weight functions. The proof is a direct numerical check that evaluates the concrete inequality without further lemmas.
Claim. In the default configuration, the time-error tolerance satisfies $0.01 < 1$.
background
The ILG module supplies concrete configurations for the Recognition Science treatment of gravitational dynamics. Its defaultConfig fixes the time-error tolerance at 0.01 together with other small tolerances on position, velocity and acceleration. The tick is the fundamental RS time quantum, normalized to 1 in native units, and appears in the definition of the weight function w_t that calls the default configuration. The identity event from ObserverForcing supplies the zero-cost reference state used by the same weight function.
proof idea
The proof is a one-line wrapper that applies norm_num to compare the literal value 0.01 against 1.
why it matters
The result anchors the default configuration that is passed to w_t and related ILG routines. It guarantees the time tolerance lies inside the interval required by the eight-tick octave and the Recognition Composition Law. No downstream theorems are recorded yet, so the lemma functions as a local sanity check rather than a link in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.