25.4. The algebraic Remarks as kind-laws: radiometry and photometry built by the kind algebra🔗

Many Part-7 definitions state a quantity's defining relation algebraically — the constitutive laws of radiometry and photometry. Radiant flux is the time-derivative of radiant energy (7-4.1); photon flux of photon number (7-20); irradiance is the area-density of radiant flux (7-7.1); radiant intensity its solid-angle-density (7-5.1); the luminous efficacy is luminous flux over radiant flux (7-11.1). Each is specified as an R12 kind-law, several crossing to ISO 80000-3 for time, area, and solid angle.

Theorem25.4.1

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Irradiance is radiant flux / area — a verified construction (item 7-7.1). An irradiance built as the quotient of a radiant flux by an area carries its quotient certificate by construction, over the ℝ carrier, and canonicity makes the certificate determine the quantity. The companion radiantIntensity_dim_from_flux_solidAngle shows radiant intensity keeps the dimension of flux because the solid angle it divides by is dimension one — the steradian dropping, as a checked computation. Uses the quotient kind-law.

Lean code for Theorem25.4.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part7/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part7.DefiningRelations.irradianceOf_isQuotient
  (φ :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part7.radiantFlux.kind
        LTMCTDimensionBase)
      ℝ)
  (a :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part3.area.kind LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsQuotient
    PropertyKindCalculus.Iso80000.Part7.DefiningRelations.irradiance_quot_flux_area
    (PropertyKindCalculus.Iso80000.Part7.DefiningRelations.irradianceOf
      φ a)
    φ a

theorem PropertyKindCalculus.Iso80000.Part7.DefiningRelations.irradianceOf_isQuotient
  (φ :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part7.radiantFlux.kind
        LTMCTDimensionBase)
      ℝ)
  (a :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part3.area.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsQuotient
    PropertyKindCalculus.Iso80000.Part7.DefiningRelations.irradiance_quot_flux_area
    (PropertyKindCalculus.Iso80000.Part7.DefiningRelations.irradianceOf
      φ a)
    φ a

The constructed irradiance satisfies the quotient certificate by construction.

Proof for Theorem 25.4.1

uses 0

irradianceOf φ a := Quantity.div irradiance_quot_flux_area φ a, and irradianceOf_isQuotient is rfl; irradiance_certificate_canonical is eq_div_of_isQuotient. The same family gives luminousEfficacyOf (= Φ_v/Φ_e), and the cross-part radiantFlux_quot_energy_duration (= radiant energy / time) and photonFlux_quot_number_duration (= photon number / time), the time crossing to ISO 80000-3.