-- Strata.lean — Stratum boundary verification
-- Non-recursive. WORM-sealed.

import Mathlib

/-- Stratum levels -/
inductive Stratum where
  | zero : Stratum
  | succ : Stratum → Stratum
  | boundary : Stratum → Stratum

/-- Stratum verification -/
def verifyStratum (s : Stratum) : Bool :=
  match s with
  | Stratum.zero => true
  | Stratum.succ inner => verifyStratum inner
  | Stratum.boundary inner => verifyStratum inner && true

/-- Stratum depth -/
def stratumDepth : Stratum → Nat
  | Stratum.zero => 0
  | Stratum.succ inner => 1 + stratumDepth inner
  | Stratum.boundary inner => 1 + stratumDepth inner