BridgeData
BridgeData supplies a minimal structure containing only the fundamental tick duration τ₀. ILG gravity calculations cite it when restricting inputs to the time unit alone. The declaration is a direct structure definition with no computational reduction or proof obligations.
claimA structure BridgeData with single field $τ_0 : ℝ$, where $τ_0$ is the fundamental tick duration in RS-native units.
background
Recognition Science supplies external constants via bridge data structures rather than axioms. The core BridgeData in DataCore contains G, ħ, c, τ₀ and ell₀. This ILG module version restricts to τ₀ alone, matching the upstream definition τ₀ := tick in Constants and the derived form sqrt(hbar_codata * G_codata / (π * c_codata³)) / c_codata in Derivation.
proof idea
The declaration is a direct structure definition. No lemmas or tactics are applied; it simply introduces the tau0 field.
why it matters in Recognition Science
It supplies the τ₀ anchor required by lambda_rec and Physical in DataCore, supporting the dimensionless identity (c³ λ_rec²) / (ħ G) = 1/π. Within the framework this connects the time unit to the eight-tick octave and RS-native constants.
scope and limits
- Does not include G, ħ or c.
- Does not enforce positivity on its field.
- Does not derive τ₀ from other constants.
- Does not contain the ell0 anchor of the core version.
formal statement (Lean)
12structure BridgeData where
13 tau0 : ℝ
14