tau0_seconds
plain-language theorem explainer
The declaration supplies the numerical value of the fundamental recognition tick τ₀ at 7.3 × 10^{-15} seconds. Researchers computing ILG weight deviations for rotating lab devices cite this constant to normalize dynamical timescales against the eight-tick octave. It is introduced as a direct numerical definition matching the RS-native expression 1/(8 ln φ).
Claim. Let τ₀ denote the recognition tick in seconds, defined by τ₀ := 7.3 × 10^{-15}.
background
The Flight-Gravity Bridge module connects the ILG weight kernel w_t(T_dyn, τ₀) = 1 + C_lag ⋅ ((T_dyn/τ₀)^α - 1) to flight models. Here τ₀ anchors the reference timescale for lab device periods, with α = (1 - φ^{-1})/2 and T_dyn identified with the rotation period. The module asks whether w remains 1 at lab scales where T_rot exceeds τ₀ by 10-15 orders of magnitude.
proof idea
Direct numerical assignment of the constant 7.3e-15 drawn from the upstream tau0_seconds definition in QFT.Decoherence. No lemmas or tactics are invoked beyond the literal value.
why it matters
This constant is used by labScaleRatio, lab_schedule_well_separated, and rsLabPrediction to evaluate the ILG prediction at laboratory scales. It realizes the T7 eight-tick octave landmark by supplying the period 2^3 in seconds and supports the module's null-result claim that w ≈ 1 for typical lab devices. The downstream rsLabPrediction doc-comment notes that any measured deviation would falsify the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.