28.3. The dimension-one family — the widest in the physical parts🔗

ISO 80000-10 carries the largest dimension-one family of the physical parts: the atomic, neutron, and nucleon numbers; the eight quantum numbers (10-13.1 … 10-13.8); the two g-factors; the relative mass excess and defect; the packing and binding fractions; the internal conversion and quality factors; the total ionization; and the reactor factors (resonance escape, fast fission, thermal utilization, non-leakage, multiplication). All share the dimension one; what tells them apart is the kind.

Theorem28.3.1

Group: The dimension-collision capstone, on standard quantities: the dimension map identifies absorbed dose with dose equivalent, while the kind layer keeps them apart, both as kinds and as units (the gray and the sievert). The becquerel collision ( T⁻¹ ) is the companion. (2)

Group member previews

Preview

Theorem 28.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 disambiguation, on the standard — the widest in the physical parts. There exist distinct ISO 80000-10 kinds with the same dimension one — the atomic and neutron numbers witness it, alongside the quantum numbers, the g-factors, and the reactor factors. Dimension cannot separate them; the kind layer does. Uses the dimension map.

Lean code for Theorem28.3.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part10.lean

complete

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

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

**The dimension-one disambiguation, on the standard — the widest in the physical
parts.** There exist distinct ISO 80000-10 kinds with the same dimension one — the atomic
and neutron numbers witness it, alongside the eight quantum numbers, the g-factors, the
relative mass excess and defect, the packing and binding fractions, the conversion and
quality factors, and the reactor factors. Dimension cannot separate them; the kind layer
does.

Proof for Theorem 28.3.1

uses 0

iso80000_10_dim_one_collision, witnessed by ⟨atomicNumber, neutronNumber, …⟩ with the kind distinction a decide and reflexivity. Axiom-free.