units_self_consistent
plain-language theorem explainer
The theorem establishes algebraic consistency among the fundamental tick duration τ₀, length ℓ₀, and arbitrary positive constants ℏ', G', c' when τ₀ is set to the scaled Planck time expression. Researchers deriving physical constants from Recognition Science primitives cite it to confirm that the unit definitions close without contradiction. The proof is a direct algebraic reduction that squares the given τ₀ relation, applies sq_sqrt and field_simp after non-negativity checks, then substitutes to recover the target expression for ℏ'.
Claim. For all real numbers ℏ', G', c' > 0, if τ₀ = √(ℏ' G' / (π c'³)) / c' and ℓ₀ = c' τ₀, then ℏ' = π c'⁵ τ₀² / G'.
background
The Constants.Derivation module derives physical constants from Recognition Science primitives using CODATA reference values for c, ℏ, and G. Here τ₀ is defined as sqrt(ℏ G / (π c³)) / c and ℓ₀ as c τ₀, matching the upstream tau0_planck_relation that equates τ₀ to the Planck time divided by √π. The local theoretical setting is the self-consistent unit system required before applying the mass formula on the phi-ladder and the alpha band bounds.
proof idea
The tactic proof introduces the three positive constants and the two defining equations. It first records c' ≠ 0, G' ≠ 0, π ≠ 0 and the non-negativity of the radicand. It then rewrites the given τ₀ equation via div_pow and sq_sqrt to obtain τ₀² = ℏ' G' / (π c'⁵), followed by field_simp. Substitution of this squared relation and a final field_simp step yields the target equality for ℏ'.
why it matters
The result is aggregated inside derivation_status, which lists units_self_consistent among the proven relations that close the constant derivation. It supplies the algebraic closure step that links the CODATA-based definitions to the Recognition Science tick duration, supporting the self-consistent units needed for the eight-tick octave and D = 3 spatial dimensions in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.