labScaleRatio
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not evaluate the ILG weight kernel itself.
- Does not incorporate device geometry or material properties.
- Does not vary the assumed 0.06 s period across different rotation rates.
- Does not address corrections outside the ILG model.
formal statement (Lean)
65def labScaleRatio : ℝ := typicalLabPeriod_seconds / tau0_seconds
proof body
Definition body.
66
67/-- The ILG exponent α = (1 - φ⁻¹)/2 ≈ 0.191.
68 Using the RS constant φ = (1 + √5)/2. -/