DOCTRINE v11 · LOCKED · 749 decls · 14 axioms · 163 sorries · kernel c7c0ba17 · SLSA L1 (honest)
Λ Conjecture 1 — NOT a theorem. Depends on 163 open sorries including CAUCHY_ND (Uniqueness.lean:120). Operator authority is human-final; Λ score is conjecture-grade, not closed proof.

Fleet Status — 5 Peers

Loading fleet status…
Λ Status
Conjecture 1
NOT a theorem. Depends on open CAUCHY_ND sorry (Uniqueness.lean:120) + missing symmetry axiom. 163 sorries open. Human decision required for all operational verdicts.
Lean Kernel Commit
c7c0ba17
lutar-lean @ lutar-v18.0.0 · 749 declarations · 14 unique axioms · 163 tracked sorries · lake build clean.
Wire B: a11oy↔sentra immune — LIVE
Wire C: a11oy↔rosie receipts — LIVE
Wire D: W3C traceparent — PENDING
§889 — 5 excluded vendors: HuaweiZTEHytera HikvisionDahua

Receipt Chain

Loading receipts…