29.4. A characteristic number is a kind, not a constant🔗

The collapse to dimension one (the collision above) invites a tempting confusion: if every characteristic number is dimension one, isn't it just a number — the same sort of thing as π or e? It is not, and saying why is the clearest statement of the two-index architecture: a quantity is a kind carried over a numeric representation.

A mathematical constant such as π is a fixed magnitude in the carrier: it lives below the kind layer, in the numbers the magnitudes are drawn from, and it is the same value in every context. A characteristic number is the opposite in every respect: it is a kind of quantity, dimension one, living above the carrier; its value is variable — whatever the defining ratio produces in a given situation (ρvL/μ for the Reynolds number, flow speed over sound speed for the Mach number). The two never coincide:

	π (a constant)	Reynolds, Mach, … (characteristic numbers)
What it is	a fixed magnitude in the carrier	a kind of quantity (dimension one)
Layer	below the kind layer, in the representation	above the carrier, in the kind layer
Value	the same number in every context	variable — whatever `ρvL/μ`, `v/c`, … produce
How formed	shipped by the carrier	by the quotient calculus, the dimensions cancelling to 1
Identity	one value	each a distinct kind — Reynolds ≠ Mach, though both dimension one

This is why the function calculus supplies π as a carrier constant and e = exp 1 as a derived one (the only mathematical constant a numeric carrier need supply directly is π), while the Reynolds and Mach numbers are kinds in this part, never carrier constants. The kind layer keeps the two categories apart exactly where a dimension-only model — seeing "dimension one" for all of them — cannot.

Definition29.4.1

groupuses 1used by 0✓L∃∀N

A carrier constant is a fixed magnitude supplied by the numeric carrier — π, and the derived e = exp 1 — living below the kind layer, in the representation type. It is the same value in every context, and it is not a quantity-kind: it carries no kind index, no measurement principle, and is not formed from other quantities. This is the categorical opposite of a characteristic number.

Lean code for Definition29.4.1●1 definition

defdefined in PropertyKindCalculus/QuantityFunction.lean

complete

def PropertyKindCalculus.MathCarrier.e {R : Type}
  [PropertyKindCalculus.MathCarrier R] [One R] : R

def PropertyKindCalculus.MathCarrier.e
  {R : Type}
  [PropertyKindCalculus.MathCarrier R]
  [One R] : R

**Euler's number**, `e = exp 1`. Derived from `exp`, not a primitive carrier field
the way `pi` is — there is no reason to make every carrier re-supply it.

Proof for Definition 29.4.1

uses 0

In the function calculus (PropertyKindCalculus.QuantityFunction), the carrier capability MathCarrier carries pi as its only primitive constant — the one transcendental constant a numeric carrier ships directly (matching TorchLean's MathFunctions (George et al., 2026)Robert Joseph George, Jennifer Cruden, Will Adkisson, Xiangru Zhong, Huan Zhang, and Anima Anandkumar (2026). “TorchLean: Formalizing Neural Networks in Lean”. arXiv preprint arXiv:2602.22631 (cs.MS). .). Every other constant is derived: MathCarrier.e := MathCarrier.exp 1, and likewise ln 2, √2, …. Adding them as carrier fields would be redundant, since the operations already determine them.

Theorem29.4.2

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

The Reynolds and Mach numbers are distinct kinds, both dimension one — so neither is a carrier constant. Two characteristic numbers forget to the same dimension one yet are different kinds, formed by the quotient calculus from different physical ratios. Unlike π (a fixed magnitude in the carrier), each is a variable quantity whose value depends on the flow. Uses the dimension map.

Lean code for Theorem29.4.2●1 theorem

theoremdefined in PropertyKindCalculus/Function.lean

complete

theorem PropertyKindCalculus.reynolds_ne_mach_but_both_dimensionless :
  PropertyKindCalculus.reynoldsK.kind LTMCTDimensionBase ≠
      PropertyKindCalculus.machK.kind LTMCTDimensionBase ∧
    PropertyKindCalculus.reynoldsK.toDimension = 1 ∧
      PropertyKindCalculus.machK.toDimension = 1

theorem PropertyKindCalculus.reynolds_ne_mach_but_both_dimensionless :
  PropertyKindCalculus.reynoldsK.kind
        LTMCTDimensionBase ≠
      PropertyKindCalculus.machK.kind
        LTMCTDimensionBase ∧
    PropertyKindCalculus.reynoldsK.toDimension =
        1 ∧
      PropertyKindCalculus.machK.toDimension =
        1

**A characteristic number is a kind, not a constant.** Reynolds and Mach are
*distinct kinds* though both forget to dimension one — a dimension-only system identifies
them, the kind layer keeps them apart. Unlike `MathCarrier.pi` (a fixed magnitude in the
carrier), each is a variable quantity formed by the quotient calculus; the value of a
Reynolds number is whatever `ρvL/μ` produces in a given flow.

Proof for Theorem 29.4.2

uses 0

reynolds_ne_mach_but_both_dimensionless : reynoldsK.kind ≠ machK.kind ∧ reynoldsK.toDimension = 1 ∧ machK.toDimension = 1, the kind inequality by decide on the differing identities, the two dimensions by reflexivity. The kinds reynoldsK/machK are declared in the function-calculus layer (PropertyKindCalculus.Function) for this contrast; the catalogued reynolds/euler of this part carry the same point across all 115 members. Axiom-free.