BridgeData
plain-language theorem explainer
BridgeData supplies the single external anchor τ₀ for ILG-specific computations in the Gravity module. It is referenced by display functions such as w_t_display and by downstream lemmas in Bridge.DataCore. The structure is introduced by a direct field declaration with no proof obligations or additional fields.
Claim. A structure consisting of the single field $τ_0 ∈ ℝ$, where $τ_0$ denotes the fundamental tick duration.
background
The module Gravity.ILG works with ILG display quantities and imports bridge anchors together with the tick duration. Upstream, BridgeData in DataCore supplies the full set of external anchors G, ħ, c, τ₀, ell₀ with no axioms. The constant τ₀ itself is defined in Constants as the duration of one recognition tick in RS-native units and re-exported via Compat and Derivation as sqrt(ħ G / (π c³))/c.
proof idea
Direct structure definition that declares the field tau0 : ℝ with no further computation or lemmas applied.
why it matters
The declaration feeds w_t_display in the same module and ILG_w_t_display in TruthCore.ILGDisplay. It supplies the τ₀ anchor required for ILG display functions that sit above the eight-tick octave (T7) and the recognition length λ_rec derived in DataCore. No open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.