typicalLabPeriod_seconds
plain-language theorem explainer
A definition assigning the real number 0.06 to the typical laboratory rotation period in seconds. Researchers computing ILG weight kernels or lab-scale ratios in the Flight-Gravity Bridge would cite this constant when setting T_dyn for a rotating device at 1000 RPM. The declaration is a direct numerical assignment with no lemmas or reductions.
Claim. Define the typical laboratory rotation period by $T_ {lab} := 0.06$ seconds.
background
The Flight-Gravity Bridge module connects the ILG weight kernel $w_t(T_{dyn}, τ_0) = 1 + C_{lag} ((T_{dyn}/τ_0)^α - 1)$ from Gravity.ILG to the Flight model. Here τ_0 ≈ 7.3 fs is the recognition tick, α = (1 - φ^{-1})/2 ≈ 0.191, and T_dyn is identified with the rotation period T_rot of a lab device. The module addresses whether this kernel produces deviations from Newtonian w = 1 at laboratory scales where T_rot ≫ τ_0 by many orders of magnitude.
proof idea
Direct definition that assigns the constant 0.06 to typicalLabPeriod_seconds. No upstream lemmas are invoked; the value is supplied as a concrete parameter for downstream ratio and schedule calculations.
why it matters
Supplies the concrete T_dyn input used by labScaleRatio to form T_dyn/τ_0, by lab_schedule_well_separated to confirm the eight-tick schedule remains well-separated, and by rsLabPrediction to evaluate the predicted weight deviation w - 1. It instantiates the module's key question on whether ILG effects remain null at lab scales, relating to the eight-tick octave and the T0-T8 forcing chain. The downstream rsLabPrediction doc-comment notes that the resulting w ≈ 29 would constitute a falsifiable large effect if observed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.