File size: 647 Bytes
81b9e0e | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 | -- 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
|