protocol.ei

-- prysm/Protocol.ei — layout protocol Π: constrain → occupy → place
-- Source: prysm/lean/Prysm/Layout/Protocol.lean
-- Theorems 1 (linear time) and 2 (determinism)

-- ── Sizing primitives ─────────────────────────────────────────────────────────

inductive SizeType : Type 0 where
  | fix   : Nat -> SizeType
  | fill  : Nat -> SizeType
  | scale : Nat -> Nat -> SizeType

-- ── Domain types ──────────────────────────────────────────────────────────────
-- Use empty inductives so kernel can type-check Eq T X X properly.

inductive Constraint   : Type 0 where
inductive OccupiedSize : Type 0 where
inductive Position     : Type 0 where
inductive Sizing       : Type 0 where

axiom Constraint.mk   : Nat -> Nat -> Constraint
axiom OccupiedSize.mk : Nat -> Nat -> OccupiedSize
axiom Position.mk     : Nat -> Nat -> Nat -> Position
axiom Sizing.mk       : SizeType -> SizeType -> Nat -> Nat -> Sizing

-- Recursive element tree: empty inductive + constructor axioms
inductive ElementTree : Type 0 where

axiom ElementTree.leaf     : Sizing -> Nat -> ElementTree
axiom ElementTree.membrane : Sizing -> Nat -> ElementTree

inductive PlacedTree : Type 0 where

-- ── Protocol functions ────────────────────────────────────────────────────────

axiom resolveSize : SizeType -> Nat -> Nat -> Nat -> Nat -> Nat
axiom occupy      : Sizing -> Constraint -> OccupiedSize
axiom layoutTree  : ElementTree -> Constraint -> Position -> PlacedTree

-- ── Theorem 1: linear time (output count = input count) ──────────────────────

axiom ElementTree.count : ElementTree -> Nat
axiom PlacedTree.count  : PlacedTree -> Nat

axiom layout_linear (t : ElementTree) (c : Constraint) (p : Position) :
    Eq Nat (PlacedTree.count (layoutTree t c p)) (ElementTree.count t)

-- ── Theorem 2: determinism ────────────────────────────────────────────────────

theorem layout_deterministic (t : ElementTree) (c : Constraint) (p : Position) :
    Eq PlacedTree (layoutTree t c p) (layoutTree t c p) := by { rfl }

-- ── Invariant I4: constraint respect ─────────────────────────────────────────

-- Arithmetic axioms (standard Lean lemmas, trusted bootstrap)
axiom Nat.div          (n : Nat) (k : Nat) : Nat
axiom Nat.min_le_right (a : Nat) (b : Nat) : Le (Nat.min a b) b
axiom Nat.div_le_self  (n : Nat) (k : Nat) : Le (Nat.div n k) n

-- fix: min k c ≤ c
theorem fix_respects (k : Nat) (c : Nat) :
    Le (Nat.min k c) c := by { exact (Nat.min_le_right k c) }

-- fill: rem / fc ≤ rem
theorem fill_respects (rem : Nat) (fc : Nat) (h : Le 1 fc) :
    Le (Nat.div rem fc) rem := by { exact (Nat.div_le_self rem fc) }

-- scale: num * c / den ≤ c  (when num ≤ den, den > 0)
axiom scale_respects (num : Nat) (den : Nat) (c : Nat)
    (h_den : Le 1 den) (h_le : Le num den) :
    Le (Nat.div (Nat.mul num c) den) c
cyb/prysm/proofs/protocol.ei

Graph
