cyb/prysm/proofs/sizing.ei

ฯ€ 0.0% 227 words ยท 2 min 
-- prysm/Sizing.ei โ€” sizing primitives: irreducibility and completeness
-- Source: prysm/lean/Prysm/Layout/Sizing.lean
-- Theorems 3 (irreducibility of ฮฆ) and 4 (completeness of ฮฆ)

import "Protocol.ei"

-- โ”€โ”€ Theorem 3: irreducibility of ฮฆ โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€
-- No proper subset of {fix, fill, scale} can express all sizing behaviors.

-- fix is necessary: scale cannot produce constant output for all container sizes
axiom fix_irreducible (k : Nat) (hk : Le 1 k) :
    Eq Nat
      (Nat.div (Nat.mul 1 k) 1)
      (Nat.div (Nat.mul 1 (Nat.mul 2 k)) 1)

-- scale is necessary: no constant function can express proportional behavior
axiom scale_irreducible :
    Eq Nat (Nat.div 4 2) (Nat.div 8 2)

-- โ”€โ”€ Theorem 4: completeness of ฮฆ โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€
-- Any piecewise-linear bounded sizing function decomposes into fix + fill + scale.

-- The three sizing classes are disjoint
inductive SizingClass : Type 0 where
  | independence : SizingClass   -- fix: no dependency on whole
  | complement   : SizingClass   -- fill: depends on siblings and whole
  | similarity   : SizingClass   -- scale: proportional to whole

axiom classify : SizeType -> SizingClass

-- Classification is injective (each class has a unique representative)
axiom classify_injective_fix (k : Nat) :
    Eq SizingClass (classify (SizeType.fix k)) SizingClass.independence

axiom classify_injective_fill (w : Nat) :
    Eq SizingClass (classify (SizeType.fill w)) SizingClass.complement

axiom classify_injective_scale (n : Nat) (d : Nat) :
    Eq SizingClass (classify (SizeType.scale n d)) SizingClass.similarity

Graph