29.3. Dimension does not classify; the measurement principle does🔗

Theorem29.3.1

Statement uses 2

Statement dependency previews

Preview

Definition 6.4.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallPriorityhighTagscapstoneproved

The dimension-one collision, on the standard — total, the widest in the series. There exist distinct ISO 80000-11 kinds with the same dimension one — the Reynolds and Euler numbers witness it, alongside all 113 others. No dimension-only type system can separate any two characteristic numbers; the kind layer, through the measurement principle (R2), holds the entire part apart. This is dimension does not classify the kind (R1) at its absolute limit. Uses the dimension map and the examination principle.

Lean code for Theorem29.3.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part11.lean

complete

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

theorem PropertyKindCalculus.Iso80000.Part11.iso80000_11_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, on the standard — total, the widest in the series.**
There exist distinct ISO 80000-11 kinds with the same dimension one — the Reynolds and
Euler numbers witness it, alongside *all* 113 others. The {dimension functor} collapses
the entire part to one point; the kind layer, through the measurement principle, keeps its
115 members apart.

Proof for Theorem 29.3.1

uses 0

iso80000_11_dim_one_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim ∧ a.dim = 1, witnessed by ⟨reynolds, euler, reynolds_ne_euler, rfl, rfl⟩. Axiom-free.