31.4. The algebraic Remarks as kind-laws: digital transmission built by the kind algebra🔗

Several Part-13 definitions state a quantity's defining relation algebraically. The signal energy per binary digit is the product of carrier power and the bit period (13-19, E_bit = P_c·T_bit); the periods are reciprocals of the rates (13-12, 13-14). Each is specified as an R12 kind-law.

Theorem31.4.1

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Signal energy per bit is carrier power × bit period — a verified construction (item 13-19). A signal energy built as the product of a carrier power and a bit period carries its product certificate by construction, over the ℝ carrier. The companion signalEnergy_dim_from_power_period shows it is M·L²·T⁻² because it is a power times a time. Uses the quotient kind-law.

Lean code for Theorem31.4.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part13/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part13.DefiningRelations.signalEnergyOf_isProduct
  (p :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part13.carrierPower.kind
        LTMCTDimensionBase)
      ℝ)
  (t :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part13.periodOfBinaryDigits.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsProduct
    PropertyKindCalculus.Iso80000.Part13.DefiningRelations.signalEnergy_prod_power_period
    (PropertyKindCalculus.Iso80000.Part13.DefiningRelations.signalEnergyOf
      p t)
    p t

theorem PropertyKindCalculus.Iso80000.Part13.DefiningRelations.signalEnergyOf_isProduct
  (p :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part13.carrierPower.kind
        LTMCTDimensionBase)
      ℝ)
  (t :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part13.periodOfBinaryDigits.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsProduct
    PropertyKindCalculus.Iso80000.Part13.DefiningRelations.signalEnergy_prod_power_period
    (PropertyKindCalculus.Iso80000.Part13.DefiningRelations.signalEnergyOf
      p t)
    p t

The constructed signal energy satisfies the product certificate by construction.

Proof for Theorem 31.4.1

uses 0

signalEnergyOf p t := Quantity.mul signalEnergy_prod_power_period p t, and signalEnergyOf_isProduct is rfl. The reciprocal kind-laws periodOfDataElements_recip_transferRate and periodOfBinaryDigits_recip_binaryDigitRate give the periods, with periodOfDataElements_dim_from_transferRate the dimension. Axiom-free.