{"organ":"a11oy","git_sha":"d58122b1d11f91b643a8b3c54458a0ef41027dd3","doctrine_lock":{"doctrine":"v11","state":"LOCKED","declarations":749,"axioms":14,"sorries":163,"commit":"c7c0ba17","lambda":"Conjecture 1","lambda_note":"Λ-Aggregator Uniqueness — Conjecture 1, NOT a closed theorem.","locked_formula_count":8,"locked_formula_ids":["F1","F4","F7","F11","F12","F18","F19","F22"],"sorries_method":"lutar-lean .github/scripts/lean_numbers.py sorries_raw @ c7c0ba17 — word-boundary 'sorry' text occurrences in Lutar/**+Main.lean, including comments and docstrings; not a count of open proof obligations","sorries_noncomment":149,"sorries_noncomment_method":"same script and commit (lutar-lean .github/scripts/lean_numbers.py @ c7c0ba17) — drops only lines whose first non-blank characters are `--`; 'sorry' text inside /- -/ block comments, /-- -/ doc comments and trailing `--` comments after code is still counted; not a count of open proof obligations","locked_formula_source":"lutar-lean Lutar/Puriq/Formulas/ProvedFormulas.lean @ 3a886349 (checked 2026-09-25; file added 2026-06-04 e6de491, last changed 2026-06-10 5cfaf9a; not present at c7c0ba17; experimental scope, outside the 749/14/163 count)"},"locked_formula_count":8,"locked_formula_ids":["F1","F4","F7","F11","F12","F18","F19","F22"],"footer":"Doctrine v11 LOCKED 749/14/163 @ c7c0ba17 · Λ = Conjecture 1","huggingface_hub_version":"1.31.0","honest_labels":{"lambda":"Λ-Aggregator Uniqueness is Conjecture 1 — NOT a theorem.","khipu_signatures":"Chain integrity is SHA3-256 hash-chain verified; DSSE signature is a separately-labelled cosign concern.","persistence":"Khipu receipts persist via backend=sqlite (durable=True).","principle":"HONESTY OVER CHECKLIST."}}