eps_t_le_one_default
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.
claimIn 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of the tolerance from the forcing chain.
- Does not constrain non-default configurations.
- Does not address spatial or velocity tolerances.
- Does not invoke the J-cost or phi-ladder.
formal statement (Lean)
76lemma eps_t_le_one_default : defaultConfig.eps_t ≤ (1 : ℝ) := by
proof body
Term-mode proof.
77 norm_num
78
79/-- Reference identity under nonzero tick: w_t(τ0, τ0) = 1. -/