BridgeData
plain-language theorem explainer
BridgeData packages the five external constants G, ħ, c, τ₀ and ℓ₀ into a single record for reuse in bridge lemmas. Analysts deriving the recognition length λ_rec cite it to supply anchors without introducing axioms. The declaration is a bare structure definition carrying no proof obligations or computational content.
Claim. A record whose fields are five real numbers: the gravitational constant $G$, reduced Planck constant $ħ$, speed of light $c$, fundamental tick duration $τ_0$, and fundamental length $ℓ_0$.
background
The module isolates the minimal bridge-anchor data so that the certified import closure remains small and avoids pulling in the full Core subsystem. BridgeData supplies the constants that appear in the recognition-length formula $λ_rec = √(ħ G / (π c³))$. Upstream constants are taken from IndisputableMonolith.Constants, where ħ is defined as cLagLock · τ₀ and G is expressed as λ_rec² c³ / (π ħ) in RS-native units.
proof idea
The declaration is a plain structure definition; no lemmas or tactics are invoked.
why it matters
BridgeData supplies the anchors required by lambda_rec and the dimensionless identity (c³ λ_rec²) / (ħ G) = 1/π proved in lambda_rec_dimensionless_id. It is used directly by the ILG gravity module and by Physical, which packages the positivity hypotheses needed for downstream lemmas. The structure therefore closes the certified bridge between RS-native constants and classical physics while keeping the import closure minimal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.