24.5. The algebraic Remarks as kind-laws: electromagnetism built by the kind algebra🔗

Many Part-6 definitions state a quantity's defining relation algebraically — the constitutive laws of circuit theory. Resistance is voltage per current (Ohm's law, 6-46); conductance is 1/R (6-47); capacitance is charge per voltage (6-13); power is voltage times current (6-45); resistivity is 1/σ (6-44); admittance is 1/Z (6-52.1); permeance is 1/Rₘ (6-40); the power factor is active over apparent power (6-58). Electric current itself is charge per time (6-1), crossing to ISO 80000-3 for its time factor. Each is formalized as an R12 kind-law over the catalogued kinds.

Theorem24.5.1

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

Resistance is voltage / current — a verified construction (Ohm's law). A resistance built as the quotient of a voltage by an electric current carries its quotient certificate by construction, over the ℝ carrier, and canonicity makes the certificate determine the quantity. Uses the quotient kind-law.

Lean code for Theorem24.5.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part6/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part6.DefiningRelations.resistanceOf_isQuotient
  (u :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part6.voltage.kind
        LTMCTDimensionBase)
      ℝ)
  (i :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part6.electricCurrent.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsQuotient
    PropertyKindCalculus.Iso80000.Part6.DefiningRelations.resistance_quot_voltage_current
    (PropertyKindCalculus.Iso80000.Part6.DefiningRelations.resistanceOf
      u i)
    u i

theorem PropertyKindCalculus.Iso80000.Part6.DefiningRelations.resistanceOf_isQuotient
  (u :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part6.voltage.kind
        LTMCTDimensionBase)
      ℝ)
  (i :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part6.electricCurrent.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsQuotient
    PropertyKindCalculus.Iso80000.Part6.DefiningRelations.resistance_quot_voltage_current
    (PropertyKindCalculus.Iso80000.Part6.DefiningRelations.resistanceOf
      u i)
    u i

The constructed resistance satisfies the quotient certificate by construction.

Proof for Theorem 24.5.1

uses 0

resistanceOf u i := Quantity.div resistance_quot_voltage_current u i, and resistanceOf_isQuotient is rfl; resistance_certificate_canonical is eq_div_of_isQuotient. The kind-law resistance_quot_voltage_current : QuotientKind voltage.kind electricCurrent.kind resistance.kind is ⟨rfl, rfl, rfl⟩, and resistance_dim_from_voltage_current checks M·L²·T⁻¹·C⁻² follows from the relation. The same families give powerOf (= voltage × current, a ProductKind), conductanceOf (= 1/R), and the cross-part electricCurrent_quot_charge_duration (= charge / time, the time crossing to ISO 80000-3).

Theorem24.5.2

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

The power factor is dimension one because it is a ratio of two powers. From the relation λ = P/S, the powers cancel and the dimension is computed to be one — not stipulated, the electromagnetic analogue of the plane angle being a ratio of two lengths and the thermodynamic efficiency a ratio of two powers. Yet the power factor remains a distinct kind from every other dimension-one quantity (the collision capstone above). Uses the dimension map.

Lean code for Theorem24.5.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part6/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part6.DefiningRelations.powerFactor_dim_from_powers :
  PropertyKindCalculus.Iso80000.Part6.powerFactor.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Iso80000.Part6.activePower.dim
        LTMCTDimensionBase /
      PropertyKindCalculus.Iso80000.Part6.apparentPower.dim
        LTMCTDimensionBase

theorem PropertyKindCalculus.Iso80000.Part6.DefiningRelations.powerFactor_dim_from_powers :
  PropertyKindCalculus.Iso80000.Part6.powerFactor.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Iso80000.Part6.activePower.dim
        LTMCTDimensionBase /
      PropertyKindCalculus.Iso80000.Part6.apparentPower.dim
        LTMCTDimensionBase

**The power factor is dimension one because it is a ratio of two powers.** Active and
apparent power are both `M·L²·T⁻³`, so `λ = P/S` cancels the dimension — the power
factor's dimensionlessness is a *checked computation from its defining relation*, not a
stipulation. (It nonetheless remains a distinct kind from every other dimension-one
quantity; see `Part6.iec80000_6_dim_one_collision`.) This is the electromagnetic
analogue of the plane angle being a ratio of two lengths and the thermodynamic
efficiency being a ratio of two powers.

Proof for Theorem 24.5.2

uses 0

powerFactor_dim_from_powers : powerFactor.dim = activePower.dim / apparentPower.dim, by reducing both sides via div_self (a / a = 1). The kind-law powerFactor_quot_active_apparent is ⟨rfl, rfl, rfl⟩. The companion power_dim_from_voltage_current checks M·L²·T⁻³ follows from P = U·I (the charge generator cancelling between voltage and current).