labScaleRatio
plain-language theorem explainer
This definition supplies the ratio of a typical laboratory rotation period to the fundamental recognition tick τ₀. Models applying the information-limited gravity weight kernel to rotating devices cite it to establish the scale separation of roughly 10^13. It is realized as a direct division of the two imported real constants typicalLabPeriod_seconds and tau0_seconds.
Claim. The ratio $T_ {dyn}/τ_0$, where $T_{dyn}$ denotes the typical laboratory rotation period (0.06 s) and $τ_0$ the recognition tick duration (7.3 fs).
background
The Flight.GravityBridge module connects the ILG weight kernel from Gravity.ILG to the Flight propulsion model. It formalizes the dynamical timescale $T_{dyn}$ for a rotating lab device and the resulting weight $w_t(T_{dyn},τ_0)=1+C_{lag}((T_{dyn}/τ_0)^α-1)$ with $α=(1-φ^{-1})/2≈0.191$.
proof idea
One-line definition that divides the constant typicalLabPeriod_seconds by tau0_seconds.
why it matters
The ratio quantifies the enormous separation between lab dynamical times and the recognition scale, confirming the null-result prediction $w≈1$ at laboratory scales. It supplies the concrete numerical input required by the ILG kernel in the Flight-Gravity bridge and links to the eight-tick octave underlying $τ_0=1/(8 ln φ)$. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.