referenceTime
plain-language theorem explainer
The definition referenceTime fixes the base coronal timescale at unity in RS-native units, representing the Alfvén crossing time. Solar physicists modeling chaotic magnetic evolution and reconnection in the corona would cite this as the unit for scaling Lyapunov times across the phi-ladder. The definition is a direct constant assignment with no computation.
Claim. Let $τ_0 = 1$ denote the reference Alfvén-crossing timescale in RS-native units.
background
The module sets up the phi-ladder of coronal Lyapunov times, where rung 0 is the fastest coherent mode (Alfvén crossing, ~1 s at 1 R☉ with B ≈ 100 G). Reference timescale τ₀ is fixed at 1 so that higher rungs scale exactly by powers of phi, matching the self-similar structure seen in solar, stellar, and astrophysical timescales. Upstream rung definitions from mass and engineering modules supply analogous ladder constructions in other domains, though they are not invoked by this constant.
proof idea
Direct definition that assigns the constant value 1.
why it matters
This anchors the coronal timescale ladder and is used by the definition coronalTime(k) := referenceTime * phi^k together with the positivity result coronalTime_pos. It supplies the reference point for the phi-ladder described in the module doc, consistent with the Recognition framework's T6 phi fixed point and the eight-tick octave scaling. The module falsifier (adjacent timescales differing by a ratio outside (1.5, 1.8)) directly tests the scaling that begins from this unit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.