{"doctrine":{"version":"v11","locked_kernel":"c7c0ba17","locked_proven":["F1","F4","F7","F11","F12","F18","F19","F22"],"locked_count":8,"experimental_kernel":"dc64dd80","lambda_status":"Conjecture 1 — NOT a theorem"},"honesty_badge":"EXPERIMENTAL · CI-green · NOT in locked-8 · kernel c7c0ba17 unchanged","experimental_scope":{"kernel_commit":"dc64dd80","lean":"v4.18.0","declarations":1401,"axioms_unique":25,"sorries":270,"theorems_ci_green_approx":"80+","wave_range":"Waves 5-24","notable_campaigns":["agentic_loop (P1-P6)","coder_formulas","PAC-Bayes routing envelope","stochastic processes / optional-stopping (Ville MC-4)","Theorem 9 (Khipu Merkle Functor)","Theorem U (conditional Λ uniqueness)","binary_pinsker (axiom-free)","Wave9: Gershgorin, Merkle, Ville, RobustDeclass, PAC-Bayes, CovarianceIntersection","Wave10: QuorumIntersection, DSSE-Token, NI-Composition, ReplayDeterminism, STL, ReachabilityRedundancy"],"note":"CI-green, kernel-verified (Waves 5-24 + agentic P1-P6 + airtight Λ + coder + Theorem 9); NEVER folded into the locked count of 8; Λ stays Conjecture 1"},"frontier_five":[{"id":"lambda_unique_of_factors","wave":"Waves 5-8 (Λ-uniqueness)","name":"Conditional Λ uniqueness","plain":"Λ is the unique aggregator GIVEN factorisation Φ x = ∏ xᵢ^αᵢ. The gap to unconditional uniqueness is exactly A6 bisymmetry (OPEN). Conjecture 1 remains OPEN unconditionally.","status":"EXPERIMENTAL · conditional-proven · CI-green on main","lean_file":"Lutar/Wave8/LambdaUnique.lean","note":"Λ = Conjecture 1; unconditional uniqueness machine-checked FALSE","honesty_badge":"EXPERIMENTAL · CI-green · NOT in locked-8 · kernel c7c0ba17 unchanged","founder_gated":false},{"id":"khipu_quorum_safety_conditional","wave":"Khipu BFT (Conjecture 2 surface)","name":"Conditional Khipu quorum safety","plain":"BFT safety under n≥3f+1 and honest non-equivocation. Conjecture 2 (unconditional) is still OPEN.","status":"EXPERIMENTAL · conditional-proven · CI-green on main","lean_file":"Lutar/Khipu/QuorumSafety.lean","note":"Khipu BFT safety = Conjecture 2 — unconditional liveness = Conjecture 3","honesty_badge":"EXPERIMENTAL · CI-green · NOT in locked-8 · kernel c7c0ba17 unchanged","founder_gated":false},{"id":"binary_pinsker","wave":"Waves 5-8 (information theory)","name":"Binary Pinsker inequality","plain":"2(p−q)² ≤ KL_bin(p,q). Axiom-free (no propext / choice needed).","status":"EXPERIMENTAL · axiom-free · CI-green on main","lean_file":"Lutar/Wave5/BinaryPinsker.lean","note":"Axiom-free; NOT in locked-8; NEVER adds to locked count","honesty_badge":"EXPERIMENTAL · CI-green · NOT in locked-8 · kernel c7c0ba17 unchanged","founder_gated":false},{"id":"khipuReceiptChains_compositionalClosure","wave":"Theorem 9 (Merkle Functor)","name":"Khipu receipt functor — Theorem 9","plain":"Khipu receipt chains form a valid CategoryTheory.Functor; receipt chains are compositionally closed (Theorem 9).","status":"EXPERIMENTAL · CI-green on main","lean_file":"Lutar/Wave9/KhipuFunctor.lean","note":"Category-theoretic backing for the receipt chain; NOT in locked-8","honesty_badge":"EXPERIMENTAL · CI-green · NOT in locked-8 · kernel c7c0ba17 unchanged","founder_gated":false},{"id":"monotone_additive_linear","wave":"Waves 5-8 (Cauchy / Aczél)","name":"Cauchy linearity via rational squeeze","plain":"Closes the Aczél 1966 obligation: monotone + additive ⇒ linear (proved via rational squeeze, no measure theory).","status":"EXPERIMENTAL · CI-green on main","lean_file":"Lutar/Wave6/MonotoneAdditive.lean","note":"Closes the Aczél obligation; NOT in locked-8","honesty_badge":"EXPERIMENTAL · CI-green · NOT in locked-8 · kernel c7c0ba17 unchanged","founder_gated":false}],"wave910":{"status":"live","count":12,"endpoint":"/api/a11oy/v1/proven/index","page":"/proven-formulas","cards":[{"id":"MA1","wave":"Wave9","name":"Gershgorin — strict diagonal dominance ⇒ nonsingular","plain":"If a trust-weight matrix is strictly diagonally dominant, every eigenvalue is bounded away from 0, so the matrix is non-degenerate (no zero-eigenvalue collapse).","status":"PROVEN","partial":false,"axioms":"'no_zero_eigenvalue' / 'nonsingular_of_strict_diag_dominant' / 'isUnit_det_of_strict_diag_dominant' depends on axioms: [propext, Classical.choice, Quot.sound]","source":"Gershgorin circle theorem (1931); Mathlib Matrix.Spectrum","source_url":"https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Matrix/Spectrum.html","lean_file":"Lutar/Wave9/Gershgorin.lean","tab":"governance gate — matrix-health pre-flight (RUN before aggregating)","benefit":"Real pre-aggregation safety gate: certifies the trust-weight matrix is invertible before a trust update, preventing a degenerate (collapsing) aggregation.","check":"/api/a11oy/v1/proven/gershgorin"},{"id":"CP-1","wave":"Wave9","name":"Merkle transparency-log soundness","plain":"Merkle root binding, inclusion-proof soundness, and append-only are proven by structural induction — an inclusion proof cannot lie about membership and the log cannot be silently rewritten.","status":"PROVEN","partial":false,"axioms":"'merkle_root_binding' / 'merkle_inclusion_sound' / 'merkle_append_only' depends on axioms: [propext]","source":"RFC 6962 (Certificate Transparency); arXiv:2303.04500","source_url":"https://arxiv.org/abs/2303.04500","lean_file":"Lutar/Wave9/Merkle.lean","tab":"receipts / audit — backs the inclusion-proof + tamper-evidence story","benefit":"Formal backing for the signed-receipt hash-chain: inclusion proofs are sound and the log is append-only, so receipts are tamper-evident.","check":null},{"id":"MC-4","wave":"Wave9","name":"Ville anytime-valid supermartingale bound","plain":"A nonnegative (super)martingale wealth process crosses 1/α with probability ≤ α at ANY time — so operators can stop/alarm at any moment with valid coverage, no fixed sample size required.","status":"PROVEN (fixed-time)","partial":true,"partial_note":"Fixed-time Ville is PROVEN; the full sup-over-all-time form is an explicitly-labeled in-file ROADMAP.","axioms":"'Supermartingale.expectation_le_one' / 'ville_markov_bound' / 'ville_fixed_time' depends on axioms: [propext, Classical.choice, Quot.sound]","source":"Ville (1939); arXiv:2009.03167","source_url":"https://arxiv.org/abs/2009.03167","lean_file":"Lutar/Wave9/Ville.lean","tab":"audit / trust-gate — live 'anytime alarm' (RUN the wealth path)","benefit":"Continuous monitoring with a time-uniform risk bound: alarm the instant evidence crosses threshold — more efficient and safer than fixed-n testing.","check":"/api/a11oy/v1/proven/ville"},{"id":"IF2","wave":"Wave9","name":"Robust declassification ⇒ non-interference","plain":"Controlled (governed) declassification preserves non-interference: an attacker cannot influence which secret bits get released through the policy channel.","status":"PROVEN","partial":false,"axioms":"'noninterference_of_robust' / 'released_facts_attacker_invariant' depends on axioms: [] ; 'robust_declass_sound' depends on axioms: [propext, Classical.choice, Quot.sound]","source":"Nonmalleable Information Flow, CCS 2017; arXiv:1708.08596","source_url":"https://arxiv.org/abs/1708.08596","lean_file":"Lutar/Wave9/RobustDeclass.lean","tab":"P3 / non-interference governance card","benefit":"Governance soundness: secrets are disclosed only via governed channels, never leaked by attacker influence — backs the controlled-release story.","check":null},{"id":"PB1","wave":"Wave9","name":"Time-uniform PAC-Bayes (routing envelope)","plain":"A time-uniform generalization (confidence) envelope for model routing, assembled from the proven Ville fixed-time corollary.","status":"PARTIAL-core","partial":true,"partial_note":"PARTIAL-core: the Ville-assembled confidence envelope is proven; the full Donsker–Varadhan variational identity + sup-over-time packaging are explicitly-labeled ROADMAP.","axioms":"'pac_bayes_confidence' / 'pac_bayes_risk_envelope' depends on axioms: [propext, Classical.choice, Quot.sound]","source":"Chugg–Wang–Ramdas, unified recipe for (time-uniform) PAC-Bayes; arXiv:2302.03421","source_url":"https://arxiv.org/abs/2302.03421","lean_file":"Lutar/Wave9/TimeUniformPACBayes.lean","tab":"routing-envelope card (governance gateway)","benefit":"An anytime generalization bound so model-routing trust gates stay sound under continual operation (ROADMAP parts labeled honestly).","check":null},{"id":"CN-1","wave":"Wave10","name":"Quorum-intersection ⇒ agreement (Flexible Paxos)","plain":"If every read quorum intersects every write quorum (read_q + write_q > n) then no two quorums decide differently — agreement safety with flexible quorum sizing.","status":"PROVEN","partial":false,"axioms":"'quorum_intersection_agreement' / 'quorum_unique_decision' does not depend on any axioms ; 'majority_quorums_intersect' depends on axioms: [propext, Quot.sound]","source":"Lamport, Part-Time Parliament (Paxos) 1998; Howard et al., Flexible Paxos, OPODIS 2016","source_url":"https://drops.dagstuhl.de/opus/volltexte/2017/7094/","lean_file":"Lutar/Wave10/QuorumIntersection.lean","tab":"mesh / consensus card (RUN the intersection check)","benefit":"Flexible quorum sizing: pick fast small read quorums + larger write quorums while keeping agreement safety — efficient consensus tuning.","check":"/api/a11oy/v1/proven/quorum"},{"id":"TE-3","wave":"Wave10","name":"DSSE search-token injectivity","plain":"Under a PRF-injective hypothesis, distinct keywords map to distinct search tokens — so an encrypted-search result set is sound w.r.t. the queried keyword.","status":"PROVEN","partial":false,"axioms":"'dsse_token_injective' / 'dsse_token_distinct' / 'dsse_search_sound' does not depend on any axioms","source":"Kamara & Papamanthou, Parallel and Dynamic Searchable Symmetric Encryption, CCS 2012/FC 2013","source_url":"https://doi.org/10.1007/978-3-642-39884-1_22","lean_file":"Lutar/Wave10/DSSEToken.lean","tab":"a11oy Code SBOM / search integrity card (RUN the injectivity check)","benefit":"Search integrity for the encrypted SBOM index: no token collisions ⇒ results are sound for the queried keyword.","check":"/api/a11oy/v1/proven/dsse"},{"id":"IF-3","wave":"Wave10","name":"Non-interference composition","plain":"Non-interference is preserved under identity, sequential composition, fold/iteration, chaining, and pairing — secure components compose into secure systems.","status":"PROVEN","partial":false,"axioms":"'ni_id' / 'ni_comp' does not depend on any axioms ; 'ni_foldl' / 'ni_chain' / 'ni_pair' depends on axioms: [propext]","source":"Goguen & Meseguer, IEEE S&P 1982; Mantel MAKS, IEEE S&P 2002","source_url":"https://doi.org/10.1109/SP.1982.10014","lean_file":"Lutar/Wave10/NonInterferenceComposition.lean","tab":"P3 / non-interference governance card","benefit":"Compositional governance soundness: chaining governed steps preserves non-interference, so the pipeline as a whole stays leak-free.","check":null},{"id":"AU-1","wave":"Wave10","name":"Replay-determinism + tamper localization","plain":"Replaying the same audit log yields the same final state (deterministic), and the first divergence pinpoints any altered entry — so audits are re-verifiable and tamper is localized.","status":"PROVEN","partial":false,"axioms":"'replay_deterministic' / 'replay_congr' / 'tamper_localized' does not depend on any axioms ; 'replay_append' depends on axioms: [propext, Quot.sound]","source":"Schneider, State Machine Approach, ACM CS 1990; Lamport, Time/Clocks, CACM 1978","source_url":"https://doi.org/10.1145/98163.98167","lean_file":"Lutar/Wave10/ReplayDeterminism.lean","tab":"audit / replay card (RUN deterministic replay + tamper-localize)","benefit":"Backs the 're-verifiable' claim: an auditor re-runs the log and gets the identical state; any single altered entry is pinpointed exactly.","check":"/api/a11oy/v1/proven/replay"},{"id":"RA-1","wave":"Wave10","name":"STL Robustness — two-sided Donzé–Maler bound","plain":"A runtime monitor that returns not just pass/fail but a signed margin ρ — how far the signal is from violating the rule. A satisfied trace guarantees ρ≥0, and ρ>0 guarantees satisfaction.","status":"PROVEN (two-sided)","partial":true,"partial_note":"Two-sided bound (Sat⇒ρ≥0, ρ>0⇒Sat, ρ<0⇒¬Sat) is PROVEN; the naive iff Sat↔ρ>0 is FALSE at the ρ=0 boundary and is NOT claimed.","axioms":"'STL.rho_sound' / 'STL.rho_pos_sound' / 'STL.rho_neg_violation' depends on axioms: [propext, Quot.sound]","source":"Donzé & Maler, Robust Satisfaction of Temporal Logic over Real-Valued Signals, FORMATS 2010","source_url":"https://doi.org/10.1007/978-3-642-15297-9_9","lean_file":"Lutar/Wave10/STLRobustness.lean","tab":"sensor-fusion / monitor card (RUN the robustness margin)","benefit":"Quantitative runtime monitoring: a signed margin tells operators how close a track/sensor signal is to breaching its bound — actionable headroom, not just a boolean.","check":"/api/a11oy/v1/proven/stl"},{"id":"OE-2","wave":"Wave9","name":"Covariance-Intersection — PSD convex closure","plain":"Fuse two sensors observing the same target even when you do NOT know how their errors are correlated. The fused covariance is always a valid, never-overconfident uncertainty ellipse.","status":"PROVEN","partial":true,"partial_note":"PROVEN core = PSD convex closure of the information form (ci_information_psd). Full inverted-covariance Loewner monotonicity is a labelled ROADMAP, not claimed.","axioms":"'posSemidef_convex_comb' / 'ci_information_psd' depends on axioms: [propext, Classical.choice, Quot.sound]","source":"Julier & Uhlmann, A Non-divergent Estimation Algorithm (Covariance Intersection), ACC 1997","source_url":"https://doi.org/10.1109/ACC.1997.609105","lean_file":"Lutar/Wave9/CovarianceIntersection.lean","tab":"sensor-fusion card (RUN the conservative fusion)","benefit":"Safe multi-sensor fusion with less bookkeeping: combine estimates with unknown cross-correlation and still get a provably valid, conservative track uncertainty.","check":"/api/a11oy/v1/proven/covariance"},{"id":"MR-1","wave":"Wave10","name":"Reachability-Redundancy + L-Menger cut/path duality","plain":"With k edge-disjoint routes between two nodes, the path survives ANY k−1 broken links — and the min-cut tells you exactly how many failures the mesh can take. Fail-safe routing, not a hope.","status":"PROVEN","partial":true,"partial_note":"MR-1 reachability halves + Menger's two directly-formalizable halves are PROVEN; the full min-max Menger equality is a labelled ROADMAP.","axioms":"'reach_mono' / 'cut_disconnects' / 'path_refutes_cut' depends on axioms: (none) ; 'disjoint_paths_le_cut' depends on axioms: [propext, Classical.choice, Quot.sound]","source":"Menger (1927); CLRS 3e Ch.26 (max-flow/min-cut); Mathlib SimpleGraph.Path","source_url":"https://en.wikipedia.org/wiki/Menger%27s_theorem","lean_file":"Lutar/Wave10/ReachabilityRedundancy.lean","tab":"mesh / tactical-routing card (RUN the survival proof)","benefit":"Provable mesh resilience: compute the redundancy k, then prove the route still connects after removing the worst k−1 links — fail-safe routing with a number behind it.","check":"/api/a11oy/v1/proven/mesh"}],"note":"Wave9 + Wave10 — 12 theorems, each carrying verbatim #print axioms and an EXPERIMENTAL · CI-green on main chip. LOCKED-proven = EXACTLY 8 {F1,F4,F7,F11,F12,F18,F19,F22}."},"founder_gated":[{"id":"PDDInjective_3_axioms","name":"PDDInjective.lean — 3 new axioms","plain":"Three new axioms (CrystalIsometryClass, PDDFingerprint, pdd) in PDDInjective.lean. Need founder approval and a reviewable PR to bump .github/data/lean_numbers.json (drift gate currently fails at HEAD per Doctrine v7 §3).","status":"FOUNDER-GATED · not yet approved","note":"DO NOT surface as proven or experimental-CI-green until founder approves","honesty_badge":"FOUNDER-GATED · awaiting review","founder_gated":true}],"software_labs":[{"id":"szl-typesafe-triage","name":"TypeSafe Triage","label":"EXPERIMENTAL","promotion_status":"HOLD","production_admitted":false,"locked_formula_member":false,"source_url":"https://github.com/szl-holdings/szl-typesafe-triage","space_url":"https://huggingface.co/spaces/SZLHOLDINGS/szl-typesafe-triage","demo_url":"https://szlholdings-szl-typesafe-triage.hf.space","readiness_url":"https://szlholdings-szl-typesafe-triage.hf.space/readyz","record_url":"https://a11oy.net/experiments/","runtime_contract":{"implementation":"Python deterministic triage","model_loaded":false},"runtime_observation":"NOT_PROBED","note":"Source-declared software lab. Open the demo to inspect its current runtime contract. No model inference or production promotion claim."}],"software_lab_count":1,"total_experimental_items":18,"live_pages":{"proven_formulas":"/proven-formulas","frontier_showcase":"/frontier"},"live_endpoints":{"wave910_index":"/api/a11oy/v1/proven/index","wave910_gershgorin":"/api/a11oy/v1/proven/gershgorin","wave910_ville":"/api/a11oy/v1/proven/ville","wave910_replay":"/api/a11oy/v1/proven/replay","wave910_quorum":"/api/a11oy/v1/proven/quorum","wave910_dsse":"/api/a11oy/v1/proven/dsse","wave910_stl":"/api/a11oy/v1/proven/stl","wave910_covariance":"/api/a11oy/v1/proven/covariance","wave910_mesh":"/api/a11oy/v1/proven/mesh","frontier_manifest":"/api/a11oy/v1/frontier/manifest","honest":"/api/a11oy/v1/honest"},"generated_at":"2026-10-13T10:53:29.544038+00:00"}