31.3. The information rates re-dimension to `T⁻¹`🔗

Per-character entropies are dimension one, but the per-second rates re-dimension to T⁻¹: the average information rate, the average transinformation rate, the channel (time) capacity, the bit and transfer rates, the call intensities. They collide there — distinct kinds, one dimension — just as the dimension-one quantities collide at the point one.

Theorem31.3.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.1

Loading preview

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

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

The bit rate is not the call intensity, though both are T⁻¹ (items 13-13, 13-7). There exist distinct IEC 80000-13 kinds with the same dimension T⁻¹ — the bit rate and the call intensity witness it, alongside the transfer and modulation rates and the information rates. Dimension cannot separate them; the kind layer does. Uses the dimension map.

Lean code for Theorem31.3.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part13.lean

complete

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

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

**The `T⁻¹` collision, on the standard.** There exist distinct IEC 80000-13 kinds with
the same dimension `T⁻¹` — the binary digit rate and the call intensity witness it, alongside
the transfer and modulation rates and the information rates. Dimension cannot separate them;
the kind layer does.

Proof for Theorem 31.3.1

uses 0

iec80000_13_dim_collision, witnessed by ⟨binaryDigitRate, callIntensity, …⟩. The shared dimension is binaryDigitRate_dim_eq_callIntensity_dim; the kind distinction is a decide. Axiom-free.

31.3. The information rates re-dimension to T⁻¹🔗

31.3. The information rates re-dimension to `T⁻¹`🔗