24.3. The AC power family: distinguishing kinds by defining construction
IEC 80000-6 lists power (6-45) as a genus and the AC power quantities — active power
(6-56), apparent power (6-57), complex power (6-59), reactive power (6-60), and non-active
power (6-61) — as items of one dimension M·L²·T⁻³. The standard distinguishes them by
which component of the periodic process each isolates: active power is the time-averaged
real (resistive) component; reactive power the imaginary part of the complex power;
apparent power the product of RMS voltage and current; and so on. Tellingly, it spends
three different unit strings on this single dimension — the watt for active power, the
var for reactive power, the volt-ampere for apparent power — precisely to keep the kinds
apart in print. A dimension-only model sees one type, "a real number of watts", for all
of them.
This is requirement R2 again, now on the AC power quantities — the pattern Part 3 set on
the length family, Part 4 on the force family, and Part 5 on the thermodynamic potentials.
Item 6-45 is the broad genus; each AC quantity is a species of power, distinguished not
by fiat but by an explicit defining construction (Dybkær's examination principle, §7.5).
The species are then provably distinct kinds while remaining mutually comparable as
powers — comparable enough to combine into the complex power P + jQ.
A power species is a ratio-scale quantity-kind of dimension
M·L²·T⁻³ carrying an examination principle — this work's own
terse descriptor of the defining construction that distinguishes it (the time-averaged
real part, the RMS product, the complex sum P + jQ, the imaginary part, the residual
√(S² − P²)), never the standard's normative definition. Active, apparent, complex,
reactive, and non-active power are all species of the general power kind (item 6-45).
Lean code for Definition24.3.1●1 definition
Associated Lean declarations
-
defdefined in PropertyKindCalculus/Iso80000/Part6.leancomplete
def PropertyKindCalculus.Iso80000.Part6.powerSpecies (id : String) (p : PropertyKindCalculus.ExaminationPrinciple) : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
def PropertyKindCalculus.Iso80000.Part6.powerSpecies (id : String) (p : PropertyKindCalculus.ExaminationPrinciple) : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
An AC power species: dimension `M·L²·T⁻³`, ratio-scale, individuated by its defining construction (examination principle).
powerSpecies id p := { kind := { id, scale := .ratio, examPrinciple := some p.id },
dim := EDim.power }. The general power carries no examination principle; the
direct-parent edges of the family are collected in an Edge relation, each species an edge
to power (mirroring the standard's listing of the AC quantities beneath power).
Active and reactive power are distinct kinds — by defining construction, not by fiat.
They share dimension M·L²·T⁻³ and are both "powers", yet are different kinds because
they isolate different components of the periodic process (the time-averaged real part vs
the imaginary part of the complex power), proved through distinct_of_examPrinciple (§7.5).
This is the AC-power analogue of width ≠ distance, static ≠ kinetic friction force, and
Helmholtz ≠ Gibbs energy. Uses the examination principle.
Lean code for Theorem24.3.2●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part6.leancomplete
theorem PropertyKindCalculus.Iso80000.Part6.activePower_ne_reactivePower : PropertyKindCalculus.Iso80000.Part6.activePower.kind LTMCTDimensionBase ≠ PropertyKindCalculus.Iso80000.Part6.reactivePower.kind LTMCTDimensionBase
theorem PropertyKindCalculus.Iso80000.Part6.activePower_ne_reactivePower : PropertyKindCalculus.Iso80000.Part6.activePower.kind LTMCTDimensionBase ≠ PropertyKindCalculus.Iso80000.Part6.reactivePower.kind LTMCTDimensionBase
**Active power and reactive power are distinct kinds — by defining construction, not by fiat.** They have the same dimension `M·L²·T⁻³` and are both "powers", yet they are different kinds *because they isolate different components of the periodic process* (the time-averaged real part vs the imaginary part of the complex power), proved through `distinct_of_examPrinciple` (§7.5) rather than by appealing to their `id` strings. This is the AC-power analogue of width ≠ distance, static ≠ kinetic friction, and Helmholtz ≠ Gibbs energy.
activePower_ne_reactivePower : activePower.kind ≠ reactivePower.kind, from
KindOfProperty.distinct_of_examPrinciple applied to the differing principles
time-averaged-real and reactive-imaginary (a decide on the Option String links).
The companion apparentPower_ne_complexPower separates two further species, and
activePower_examinedBy checks the kind-to-principle link. Axiom-free.
Comparability is preserved. Active and reactive power, though distinct kinds, remain
mutually comparable — they share the super-kind power, so combining them (into the
complex power) is possible but only via an explicit up-cast, never silently. The companion
activePower_specializes_power records that active power specializes power. Uses
specialization.
Lean code for Theorem24.3.3●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part6.leancomplete
theorem PropertyKindCalculus.Iso80000.Part6.activePower_reactivePower_comparable : PropertyKindCalculus.MutuallyComparable PropertyKindCalculus.Iso80000.Part6.Edge (PropertyKindCalculus.Iso80000.Part6.activePower.kind LTMCTDimensionBase) (PropertyKindCalculus.Iso80000.Part6.reactivePower.kind LTMCTDimensionBase)
theorem PropertyKindCalculus.Iso80000.Part6.activePower_reactivePower_comparable : PropertyKindCalculus.MutuallyComparable PropertyKindCalculus.Iso80000.Part6.Edge (PropertyKindCalculus.Iso80000.Part6.activePower.kind LTMCTDimensionBase) (PropertyKindCalculus.Iso80000.Part6.reactivePower.kind LTMCTDimensionBase)
**Mutual comparability is preserved.** Active and reactive power, though distinct kinds, remain *mutually comparable* — they share the super-kind power, so combining them (into the complex power) is possible but only via an explicit up-cast, never silently.
activePower_reactivePower_comparable : MutuallyComparable Edge activePower.kind
reactivePower.kind, with witness power.kind, each species reaching it by one edge.
Axiom-free.