dim_hbar
plain-language theorem explainer
The reduced Planck constant receives the dimensional signature with length exponent 2, time exponent minus 1, and mass exponent 1. Researchers performing dimensional analysis on constants derived from recognition primitives would reference this assignment. The definition is a direct record construction inside the Dimension structure.
Claim. The reduced Planck constant ħ carries the dimensional signature $[L^2 T^{-1} M^1]$.
background
Recognition Science assigns each physical quantity a dimensional signature [L^a T^b M^c] that tracks length, time, and mass exponents. The Dimension structure records these three integers and is used throughout the module to maintain consistency when constants are expressed in terms of the fundamental tick τ₀, recognition length ℓ₀ = c τ₀, and golden ratio φ. The module imports the same Dimension definition from Foundation.DimensionForcing and the Recognition structure M to ensure the signatures align with the forcing chain.
proof idea
One-line definition that applies the Dimension constructor to the integer triple (2, -1, 1).
why it matters
This supplies the required dimensional signature for ħ, which enters the mass formula and the self-consistent derivation of constants (ħ = φ^{-5} in native units). It supports the overall framework in which c = 1, ħ = φ^{-5}, G = φ^5 / π, and the eight-tick octave fixes D = 3. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.