tau0_sq_eq
plain-language theorem explainer
The lemma equates the square of the fundamental tick duration to the product of the reduced Planck constant and Newton's gravitational constant divided by pi times the fifth power of the speed of light, using the adopted CODATA numerical values. Researchers deriving constants inside the Recognition Science framework cite this relation to close the consistency check between the tick scale and observed constants. The proof unfolds the tau0 definition, inserts non-zero checks on the denominators, and finishes with algebraic rewriting plus field_su
Claim. $τ_0^2 = ℏ_{codata} G_{codata} / (π c_{codata}^5)$ where $τ_0$ denotes the fundamental tick duration in RS-native units and the subscripted symbols are the CODATA reference values for the reduced Planck constant, Newton's constant, and the speed of light.
background
The module derives physical constants from Recognition Science primitives by importing the CODATA reference values c = 299792458, ℏ = 1.054571817×10^{-34}, G = 6.67430×10^{-11} and defining corresponding codata constants. tau0 is the fundamental time unit, the duration of one tick, taken from the upstream definition in IndisputableMonolith.Constants as the RS-native tick length. The lemma supplies the algebraic bridge that lets the tick scale reproduce the standard constants.
proof idea
Unfold tau0, then introduce four non-zero hypotheses (c_codata ≠ 0, π ≠ 0, and the relevant powers). Rewrite with div_pow and sq_sqrt inner_nonneg, then finish with field_simp.
why it matters
The lemma is the central algebraic identity used by G_relation_satisfied and planck_relation_satisfied to verify that the derived constants equal the CODATA inputs; it also appears in the derivation_status summary. It therefore completes the constants-derivation step inside the Recognition Science framework, confirming that the tick-based expressions for G and ℏ match experiment once the codata values are inserted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.