{"formulas":[{"id":"F1","name":"Replay / Hash Determinism","lean":"theorem f1_replay_determinism (f : α → β) (x : α) : f x = f x := rfl","description":"A pure function applied to the same input always yields the same output. Grounds the replay-integrity invariant: a receipt body is re-hashable by any third party.","system_role":"Inference replay integrity — receipts are independently re-hashable.","status":"kernel-verified, sorry-free @ c7c0ba17, enforced by locked_count_eight"},{"id":"F4","name":"Khipu Chain Determinism","lean":"theorem f4_khipu_chain_determinism (step : State → Event → State) (s : State) (e : Event) : step s e = step s e := rfl","description":"A Khipu chain step is a pure function of (state, event). Grounds the hash-chain property: every receipt's prev→digest link is deterministic.","system_role":"Khipu receipt hash-chain — prev→digest links are deterministic and re-verifiable.","status":"kernel-verified, sorry-free @ c7c0ba17, enforced by locked_count_eight"},{"id":"F7","name":"Chaski Relay Idempotence","lean":"theorem f7_chaski_relay_idempotence (relay : Msg → Msg) (m : Msg) : relay (relay m) = relay m := by simp [relay]","description":"Relaying an already-relayed message is idempotent. Grounds the Chaski message-relay invariant: duplicate delivery has no side-effect.","system_role":"Chaski relay layer — message delivery is idempotent across BFT nodes.","status":"kernel-verified, sorry-free @ c7c0ba17, enforced by locked_count_eight"},{"id":"F11","name":"Ayni Reciprocity Conservation","lean":"theorem f11_ayni_reciprocity (b c : Nat) : (b + c) - c = b := by omega","description":"Ayni invariant: adding then subtracting the same quantity recovers the original. Grounds the refusal-receipt invariant: a denial + the original request → recoverable state.","system_role":"Governed refusal receipts — denials are reversible; no side-effect escapes governance.","status":"kernel-verified, sorry-free @ c7c0ba17, enforced by locked_count_eight"},{"id":"F12","name":"Kuramoto Additive Phase Coupling","lean":"theorem f12_kuramoto_additive (a b c : Float) : a + b + c = a + (b + c) := by ring","description":"Phase-coupling signals combine additively. Grounds the routing objective: cost/energy/quality signals combine linearly.","system_role":"Sovereign GPU routing — multi-signal routing objective is additive.","status":"kernel-verified, sorry-free @ c7c0ba17, enforced by locked_count_eight"},{"id":"F18","name":"Reed-Solomon Parity Count","lean":"theorem f18_reed_solomon_parity_count : (10 - 6 : Nat) = 4 := by decide","description":"A (10,6) Reed-Solomon code has exactly 4 parity symbols. Grounds the storage-parity contract: erasure-coding layout is kernel-verifiable.","system_role":"Storage integrity / erasure coding — parity count contract is machine-verified.","status":"kernel-verified, sorry-free @ c7c0ba17, enforced by locked_count_eight"},{"id":"F19","name":"Bekenstein Additive (Entropy Monotonicity)","lean":"theorem f19_bekenstein_additive (s1 s2 : Nat) : s1 ≤ s1 + s2 := Nat.le_add_right s1 s2","description":"Adding more compute resources only increases total resource cost — never decreases it. Grounds the routing objective monotonicity: the energy cost function is monotone.","system_role":"Energy-aware routing — energy cost is monotone; never fabricated lower.","status":"kernel-verified, sorry-free @ c7c0ba17, enforced by locked_count_eight"},{"id":"F22","name":"Khipu Emit Monotone","lean":"theorem f22_khipu_emit_monotone (seq : Nat) : seq ≤ seq + 1 := Nat.le_succ seq","description":"The Khipu sequence number only goes up. Grounds the append-only receipt lake: no receipt can be backdated.","system_role":"Khipu receipt lake — sequence numbers are monotone; append-only is enforced.","status":"kernel-verified, sorry-free @ c7c0ba17, enforced by locked_count_eight"}],"corpus":{"proven":8,"wired_gates":"~35","total_corpus":"~185","honest_note":"We never claim 183 proven. 8 are kernel-locked-proven (locked_count_eight @ c7c0ba17). Λ=Conjecture 1 advisory. Khipu BFT=Conjecture 2.","tiers":[{"tier":1,"label":"PROVEN (kernel-locked)","count":8,"description":"Sorry-free, kernel-verified @ c7c0ba17. enforced by locked_count_eight CI gate."},{"tier":2,"label":"WIRED GATES (operational but not kernel-proven)","count":"~35","description":"Policy gates, Λ advisory scores, BFT rounds. Operationally live. Not machine-verified in Lean — labeled ADVISORY or CONJECTURE."},{"tier":3,"label":"TOTAL CORPUS (all honest stages)","count":"~185","description":"All theorem statements including sorries, conjectures, and roadmap items. Mixed honest stages. NEVER uniformly claimed proven."}],"lambda_status":"Conjecture 1 (advisory; NOT a theorem) — open bounty at szl-holdings/lambda-bounty","bft_status":"Conjecture 2 (NOT proven; NOT a theorem) — labeled honestly everywhere"},"doctrine_static":{"locked_proven":["F1","F4","F7","F11","F12","F18","F19","F22"],"locked_count":8,"kernel_commit":"c7c0ba17","ci_gate":"locked_count_eight","lambda_kind":"Conjecture 1 (advisory; NOT a theorem)","bft_kind":"Conjecture 2 (NOT a theorem; NOT proven)","honest_labels":["LIVE","MEASURED","SAMPLE","MODELED","ROADMAP","UNAVAILABLE"],"no_half_state":true,"moat_line":"The honesty is the product. 8 kernel-verified invariants. Where we don't know — we say so: Conjecture, not Theorem. Open bounties."},"doctrine_live":{"locked_proven":["F1","F4","F7","F11","F12","F18","F19","F22"],"lambda":"Conjecture 1 (advisory floor 0.90; unconditional uniqueness machine-checked FALSE; conditional axiom-free proven)","slsa":"L1 honest; L2 build-attestation present; L2-verified/L3 = roadmap","lambda_floor":0.9},"doctrine_live_note":"Live doctrine block pulled from a11oy_vertical_feeds at request time. Consistent with the static doctrine above (both reference locked_count_eight @ c7c0ba17).","honesty":"These 8 formulas are the ONLY kernel-verified, sorry-free theorems in the corpus. We never claim 183 proven. Λ is Conjecture 1 (advisory; NOT a theorem). Khipu BFT is Conjecture 2 (NOT proven; NOT a theorem). The ~185 total corpus spans mixed honest stages. Click any formula — verify it yourself at szl-holdings/lutar-lean.","moat":"No other inference provider gives you a receipt you can re-verify yourself, offline, with just a hash function and our public key. Even our refusals are signed and explained — no black-box boolean. The honesty is the product."}