tau0
plain-language theorem explainer
The definition supplies the numerical value of the fundamental tick duration τ₀ by substituting CODATA constants into the expression √(ℏ G / (π c³)) / c. Bridge modules and unit certification routines cite it to anchor RS-native time to measured SI values. The body is a direct abbreviation with no reduction steps or lemmas applied.
Claim. τ₀ := √(ℏ_cod G_cod / (π c_cod³)) / c_cod, where ℏ_cod = 1.054571817×10^{-34}, G_cod = 6.67430×10^{-11}, and c_cod = 299792458 are the CODATA reference values for the reduced Planck constant, gravitational constant, and speed of light.
background
The Constants.Derivation module introduces physical constants as numerical definitions drawn from CODATA to anchor Recognition Science primitives to SI units. The referenced siblings c_codata, hbar_codata, and G_codata are the exact values 299792458, 1.054571817×10^{-34}, and 6.67430×10^{-11}. Upstream results supply the abstract tick from IndisputableMonolith.Constants.tick and the placeholder τ₀ in Compat.Constants.
proof idea
Direct definition that substitutes the three codata constants into the algebraic expression for τ₀. No lemmas are applied; the body is the closed-form expression itself.
why it matters
This definition provides the concrete numerical anchor for the fundamental tick duration τ₀ used throughout the framework. It feeds into BridgeData for external data structures and into UnitsKGateCert for ratio computations that certify unit consistency. In the Recognition Science chain it supplies the time unit that appears in the eight-tick octave and the mass ladder formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.