Physical Dimension

@cite{bale-schwarz-2026} @cite{scontras-2014} @cite{zabbal-2005}

Per-entry feature taxonomy of physical measurement dimensions: the typed tag that classifies what a measure function measures (mass, volume, distance, time, cardinality, ...) and the corresponding quotient dimensions (density, speed, pressure) that ratios of simplex dimensions give rise to.

Scope

Dimension is the simplex feature: directly-measurable properties accessible to compositional semantics. QuotientDimension is the parallel taxonomy of derived ratios. Per @cite{bale-schwarz-2026}'s No Division Hypothesis (eq. (5), p. 135), the grammar does not compositionally produce values in quotient dimensions; references to them go through extra-grammatical "math speak".

DimensionType is the binary tag (simplex/quotient) used by paper-anchored studies that need to label values without committing to a specific dimension.

Consumers

• Theories/Semantics/Measurement/Basic.lean: MeasureFn carries Dimension
• Fragments/English/MeasurePhrases.lean: MeasureTermEntry carries Dimension
• Phenomena/Quantification/Studies/{BaleSchwarz2022, BaleSchwarz2026, Scontras2014}.lean
• Theories/Semantics/{Noun/Binominal, Gradability/Hierarchy, Verb/VerbEntry, Events/MeasurePhrases}.lean

inductive Features.Dimension.Dimension : Type

Physical dimensions that measure functions can target.

Simplex dimensions are directly measurable properties of entities and are accessible to compositional semantics. The cardinality constructor names the dimension of @cite{zabbal-2005}'s CARD (the Num-head behind cardinal numerals), aligned by @cite{scontras-2014} with measure terms.

• mass : Dimension
• volume : Dimension
• distance : Dimension
• time : Dimension
• cardinality : Dimension
• temperature : Dimension
• area : Dimension
• force : Dimension

def Features.Dimension.instReprDimension.repr : Dimension → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Features.Dimension.instReprDimension : Repr Dimension

Equations

• Features.Dimension.instReprDimension = { reprPrec := Features.Dimension.instReprDimension.repr }

@[implicit_reducible]

instance Features.Dimension.instDecidableEqDimension : DecidableEq Dimension

Equations

• Features.Dimension.instDecidableEqDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Features.Dimension.QuotientDimension : Type

Quotient dimensions: ratios of simplex dimensions.

These exist in the quantity calculus but are not compositionally derivable within the grammar (@cite{bale-schwarz-2026}'s No Division Hypothesis).

• density : QuotientDimension
• speed : QuotientDimension
• pressure : QuotientDimension

@[implicit_reducible]

instance Features.Dimension.instReprQuotientDimension : Repr QuotientDimension

Equations

• Features.Dimension.instReprQuotientDimension = { reprPrec := Features.Dimension.instReprQuotientDimension.repr }

def Features.Dimension.instReprQuotientDimension.repr : QuotientDimension → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Features.Dimension.instDecidableEqQuotientDimension : DecidableEq QuotientDimension

Equations

• Features.Dimension.instDecidableEqQuotientDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.Dimension.QuotientDimension.components : QuotientDimension → Dimension × Dimension

The simplex components of a quotient dimension.

Decomposition follows physical convention: density is mass per volume, speed is distance per time, pressure is force per area.

Equations

• Features.Dimension.QuotientDimension.density.components = (Features.Dimension.Dimension.mass, Features.Dimension.Dimension.volume)
• Features.Dimension.QuotientDimension.speed.components = (Features.Dimension.Dimension.distance, Features.Dimension.Dimension.time)
• Features.Dimension.QuotientDimension.pressure.components = (Features.Dimension.Dimension.force, Features.Dimension.Dimension.area)

inductive Features.Dimension.DimensionType : Type

Binary tag distinguishing the two dimension taxonomies.

All Dimension constructors are simplex by definition; QuotientDimension is always quotient. Studies that need to label values without committing to a specific dimension use this tag.

• simplex : DimensionType
• quotient : DimensionType

@[implicit_reducible]

instance Features.Dimension.instReprDimensionType : Repr DimensionType

Equations

• Features.Dimension.instReprDimensionType = { reprPrec := Features.Dimension.instReprDimensionType.repr }

def Features.Dimension.instReprDimensionType.repr : DimensionType → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Features.Dimension.instDecidableEqDimensionType : DecidableEq DimensionType

Equations

• Features.Dimension.instDecidableEqDimensionType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

theorem Features.Dimension.quotient_components_distinct (q : QuotientDimension) : q.components.fst ≠ q.components.snd

Every quotient dimension's components are distinct simplex dimensions.

There is no "self-ratio" quotient — mass/mass, time/time etc. would be dimensionless and don't appear in QuotientDimension.