tau0_planck_relation
plain-language theorem explainer
The theorem proves that the fundamental tick duration τ₀ equals the Planck time divided by √π. Researchers checking numerical consistency between Recognition Science units and CODATA values would cite it when verifying that the discrete tick aligns with the continuous Planck scale. The tactic proof unfolds both sides, records positivity and non-zero facts for c, ℏ, G and π, equates the squares of the candidate expressions, and recovers equality by applying sqrt_sq to the non-negative results.
Claim. $τ_0 = t_P / √π$, where $τ_0$ is the fundamental tick duration and $t_P = √(ℏ G / c^5)$ is the Planck time expressed in the same units.
background
The Constants.Derivation module numerically checks relations among physical constants using CODATA reference values for c, ℏ and G. τ₀ is the duration of one recognition tick; planck_time is the standard expression √(ℏ G / c^5). Upstream definitions supply τ₀ as the tick duration and G in the form λ_rec² c³ / (π ℏ), together with the concrete codata constants c_codata, hbar_codata and G_codata and their positivity lemmas.
proof idea
Tactic proof that unfolds tau0 and planck_time, then introduces non-zero and positivity facts via c_codata_ne_zero, c_codata_pos, hbar_codata_pos, G_codata_pos and Real.pi_pos. It computes both candidate sides squared, shows each equals ℏG/(π c^5) by div_pow, sq_sqrt and field_simp, equates the squares, and finishes with sqrt_sq on the non-negative quantities to obtain the original equality.
why it matters
The result is recorded inside derivation_status as one of the completed checks that the constants derivation is self-consistent. It closes the link between the RS tick τ₀ and the Planck time, confirming that the forcing-chain time unit (T7) reproduces the expected Planck scale when CODATA values are inserted. No open scaffolding remains for this relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.