31.2. Dimension one, three kind families, incommensurable special units (R13)🔗

IEC 80000-13's characteristic quantities all live at dimension one — and this is exactly the place the catalogue's thesis turns into a unit question. Three families share dimension one but carry different special units, and belong to different kinds:

Information content and entropy (13-24 …) in the shannon Sh, hartley Hart, or natural unit nat — alternative units of one kind, related by the logarithm base.
Traffic intensity (13-1 …) in the erlang E.
Storage capacity (13-9, 13-10) in the bit (or octet, or byte).

A dimension-only model sees one type, "a real number, dimension one", for all of them, and would let a bit of storage be silently read as an erlang of traffic. The shannon, erlang, and bit are scale-spanning units (R13), human-selected references for a dimensionless count — exactly like the candela (ISO 80000-7) and the mole (ISO 80000-9). The kind layer is what keeps them apart.

Theorem31.2.1

Group: The dimension-one collision capstone, on standard quantities: the dimension map identifies information content, traffic intensity, and storage capacity, while the kind layer keeps them apart, both as kinds and as units (the shannon, the erlang, the bit). (2)

Group member previews

Preview

Theorem 31.2.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagscapstoneproved

The shannon of information content and the erlang of traffic intensity are not commensurable, though both are dimension one (items 13-24, 13-1). Two human-selected dimensionless references for two different kinds — a bit of information is not an erlang of traffic. The companion shannon_bit_not_commensurable separates information from storage. This is the scale-spanning collision (R13) on information. Uses the metrological unit.

Lean code for Theorem31.2.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part13.lean

complete

theorem PropertyKindCalculus.Iso80000.Part13.shannon_erlang_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part13.shannon.Commensurable
      PropertyKindCalculus.Iso80000.Part13.erlang

theorem PropertyKindCalculus.Iso80000.Part13.shannon_erlang_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part13.shannon.Commensurable
      PropertyKindCalculus.Iso80000.Part13.erlang

**The shannon of information content and the erlang of traffic intensity are not
commensurable, though both are dimension one.** Two human-selected dimensionless references
for two different kinds — a bit of information is not an erlang of traffic. The
scale-spanning collision (R13) on information.

Proof for Theorem 31.2.1

uses 0

shannon_erlang_not_commensurable and shannon_bit_not_commensurable, each by decide after unfolding MetrologicalUnit.Commensurable on the dimension-one kinds. Axiom-free.

Theorem31.2.2

Group member previews

Preview

Theorem 31.2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

The dimension-1 collision, on the standard. There exist distinct IEC 80000-13 kinds with the same dimension one — information content and traffic intensity witness it, alongside storage capacity, the entropies, and the probabilities. With distinct special units (shannon, erlang, bit), the dimension cannot separate them; the kind layer does. Uses the dimension map.

Lean code for Theorem31.2.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part13.lean

complete

theorem PropertyKindCalculus.Iso80000.Part13.iec80000_13_dim_one_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase ∧
        a.dim LTMCTDimensionBase = 1

theorem PropertyKindCalculus.Iso80000.Part13.iec80000_13_dim_one_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠
        b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase =
          b.dim LTMCTDimensionBase ∧
        a.dim LTMCTDimensionBase = 1

**The dimension-one collision capstone, on the standard.** There exist distinct
IEC 80000-13 kinds with the same dimension one — information content and traffic intensity
witness it, alongside storage capacity, the entropies, and the probabilities. With distinct
special units (shannon, erlang, bit), the {dimension functor} cannot separate them; the
kind layer does.

Proof for Theorem 31.2.2

uses 0

iec80000_13_dim_one_collision, witnessed by ⟨informationContent, trafficIntensity, …⟩ with the kind distinction a decide and reflexivity. Axiom-free.