1.2 Verification tiers

All 114 public theorems discharge under the following tiers, all green at commit 471e5d5 (see test/verification/CI/):

• Tier 0: lake build, 0 errors, 0 warnings, 0 sorry in ZPM/.

• Tier 1: #print axioms. 113 theorems use only propext, Classical.choice, Quot.sound; the 114th (challenge_bnd_subset_cyl) uses none.

• Tier 2: leanchecker –fresh per module (GitHub Actions workflow_dispatch).

• Tier 3: comparator + Landlock sandbox on GitLab CI; “Lean default kernel accepts the solution. Your solution is okay!” (pipeline #2463996501, duration 36 min).

Every statement in this blueprint carries a \lean{...} annotation linking to the Lean declaration; where the full proof is in the source, \leanok marks the entry as formally verified.