Repository navigation

Lean certificate check - #26

Merged

Mister-Meeseeks merged 7 commits into

CrocSwap:mainfrom

princezuda:lean-certificate-check

Oct 8, 2026

Merged

Lean certificate check#26
Mister-Meeseeks merged 7 commits into
CrocSwap:mainfrom
princezuda:lean-certificate-check

Commits on Oct 8, 2026
- Add a Lean check of the kappa = 83/10^12 certificate arithmetic
  
  princezuda
  and
  claude
  committed
  0132439
- Pair every Lean declaration with the lines it formalizes
  claude
  committed
  e963f21
- Check in the scoped-ceiling negative control as a theorem
  claude
  committed
  f99d715
- Prove the guard note's depth recursion in Lean
  claude
  committed
  75b7881
- Check the R = 509194 circuit independently; prove frame and movement algebra
  claude
  committed
  b0d5105
- Prove the compact-control layout's row arithmetic in Lean
  claude
  committed
  90457d2
- Add Lean checks of the open PRs #3-#12 certificate arithmetic
  claude
  committed
  f764fb9