PositiveDimensionedQuantity
plain-language theorem explainer
PositiveDimensionedQuantity defines a dimensioned physical quantity whose real value is strictly positive, extending the base structure that pairs a real number with a length-time-mass exponent triple. Researchers deriving constants such as ħ or G from Recognition Science primitives would cite it to enforce positivity for energies and masses. The construction is a direct structure extension that adds only the single inequality constraint.
Claim. A positive dimensioned quantity is a pair $(v, [L^a, T^b, M^c])$ where $v > 0$ is real and the triple records integer exponents for length, time, and mass.
background
The module supplies a dimensional analysis framework whose fundamental units are the tick τ₀, the recognition length ℓ₀ = c τ₀, and the golden ratio φ. Each quantity is carried by DimensionedQuantity, which stores a real value together with an integer triple of exponents for length, time, and mass. Upstream structures such as PhiForcingDerived.of encode the J-cost function J(x) = (x + x^{-1})/2 - 1, while SpectralEmergence.of fixes the gauge content and three generations that must carry consistent dimensions.
proof idea
The declaration is a structure definition that extends DimensionedQuantity by adjoining the field value_pos : 0 < value. No lemmas or tactics are invoked; the proof body is simply the record extension.
why it matters
The definition supplies the positivity guard required when constants are extracted from the Recognition Science forcing chain (T5 J-uniqueness through T8 D = 3). It supports self-consistent derivation of ħ = φ^{-5}, G = φ^5 / π, and the fine-structure constant inside the interval (137.030, 137.039). No downstream theorems are recorded, so the structure remains a leaf definition in the constants layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.