24.2. Electric potential: one dimension, two scales🔗

IEC 80000-6 lists electric potential (6-11.1) and electric potential difference (6-11.2) as separate items of the same dimension V. But they are not the same kind of quantity. Electric potential is fixed only up to an arbitrary additive reference — the choice of where "zero potential" sits (the ground, infinity) is a gauge, so the standard notes the potential "is not unique". Only its differences are physically meaningful, so it is interval-scale: a ratio of two electric potentials is not a defined operation. Electric potential difference is a genuine difference, so it is ratio-scale. A dimension-only model sees one type, "a real number of volts", for both.

This is requirement R6 — the scale type fixes which operations are even defined — recurring on electromagnetism exactly as it appeared on thermodynamics. The gauge-dependent electric potential is electromagnetism's Celsius temperature: same dimension as its companion, separated from it neither by dimension nor by an examination principle, but by scale type alone.

Theorem24.2.1

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

Electric potential does not admit ×,÷. It is interval-scale (gauge freedom — fixed only up to an arbitrary additive reference), so a ratio of electric potentials is not a meaningful operation — the scale layer refuses it where the dimension would not. Electric potential difference, being ratio-scale, does admit it. Uses the scale type.

Lean code for Theorem24.2.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part6.lean

complete

theorem PropertyKindCalculus.Iso80000.Part6.electricPotential_not_allowsRatio :
  ¬(PropertyKindCalculus.Iso80000.Part6.electricPotential.kind
          LTMCTDimensionBase).scale.AllowsRatio

theorem PropertyKindCalculus.Iso80000.Part6.electricPotential_not_allowsRatio :
  ¬(PropertyKindCalculus.Iso80000.Part6.electricPotential.kind
          LTMCTDimensionBase).scale.AllowsRatio

**Electric potential does *not* admit `×`,`÷`.** It is interval-scale (fixed only up
to an arbitrary additive reference — gauge freedom), so a ratio of electric potentials is
not a meaningful operation — the kind layer refuses it where dimension would not.

Proof for Theorem 24.2.1

uses 0

electricPotential_not_allowsRatio : ¬ ScaleType.AllowsRatio electricPotential.kind.scale, with the companion electricPotentialDifference_allowsRatio for the ratio case. The volt of electric potential is nonetheless WellFormed (voltPotential_wellFormed, via the differential scale), and voltPotential_voltDifference_not_commensurable records that the two volts — same symbol, same dimension — are not commensurable, because the kinds differ in scale.

Theorem24.2.2

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

The scale disambiguation, on the standard. There exist distinct IEC 80000-6 kinds with the same dimension V that are separated by scale type alone — electric potential (interval, gauge-dependent) and electric potential difference (ratio) witness it. Neither the dimension nor an examination principle tells them apart; the scale layer does. This is requirement R6 on the standard, the electromagnetic counterpart of thermodynamic versus Celsius temperature. Uses the scale type.

Lean code for Theorem24.2.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part6.lean

complete

theorem PropertyKindCalculus.Iso80000.Part6.iec80000_6_scale_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase ∧
        (a.kind LTMCTDimensionBase).scale ≠
          (b.kind LTMCTDimensionBase).scale

theorem PropertyKindCalculus.Iso80000.Part6.iec80000_6_scale_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠
        b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase =
          b.dim LTMCTDimensionBase ∧
        (a.kind
              LTMCTDimensionBase).scale ≠
          (b.kind
              LTMCTDimensionBase).scale

**The scale disambiguation, on standard quantities.** There exist distinct
IEC 80000-6 kinds with the same dimension `M·L²·T⁻²·C⁻¹` that are separated by *scale
type* alone — electric potential (interval, gauge-dependent) and electric potential
difference (ratio) witness it. Neither the dimension nor an examination principle tells
them apart; the scale layer does. This is requirement R6 on the standard, the
electromagnetic counterpart of Part 5's thermodynamic/Celsius temperature.

Proof for Theorem 24.2.2

uses 0

iec80000_6_scale_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim ∧ a.kind.scale ≠ b.kind.scale, witnessed by ⟨electricPotential, electricPotentialDifference, …⟩ with reflexivity on the dimension and a decide on the differing scales. Axiom-free.