{"state":"AVAILABLE","wired":[{"name":"pacbayes","citation":"thesis_v22.pdf §2","lean_theorem":"Lutar/PACBayes.lean::pacBayes_inequality_form (TH13)"},{"name":"welford","citation":"thesis_v22.pdf §2","lean_theorem":"FrontierWelfordVariance.lean::welford_mean_exact"},{"name":"quorum","citation":"thesis_v22.pdf §2","lean_theorem":"KhipuConsensus.lean::khipu_consensus_safety (Conjecture 2)"},{"name":"holevo","citation":"thesis_v22.pdf §2","lean_theorem":"QuantumHolevoReceipt.lean::holevo_chi_nonneg (PR #176 — PROPOSED, not yet in corpus)","tier":"experimental"},{"name":"bloom","citation":"thesis_v22.pdf §2","lean_theorem":"FrontierBloomCacheBypass.lean::query_after_insert"},{"name":"kalman","citation":"thesis_v22.pdf §2","lean_theorem":"FrontierKalmanGain.lean::posterior_le_prior"},{"name":"bls","citation":"thesis_v22.pdf §2","lean_theorem":"FrontierBLSAggregation.lean::aggregate_verify"},{"name":"reidemeister","citation":"thesis_v22.pdf §2","lean_theorem":"KnotCalculus (v15, scaffolding — PROPOSED obligation, not a locked theorem)","tier":"experimental"},{"name":"hnsw","citation":"thesis_v22.pdf §2","lean_theorem":"FrontierHNSWNavigability.lean::greedy_search_terminates"},{"name":"kl","citation":"Cover–Thomas Thm 2.6.3 (Gibbs); χPO arXiv:2407.13399; f-DPO arXiv:2309.16240","lean_theorem":"Wave15/DPOKLSimplex.lean::dpo_klDivergence_nonneg_on_simplex (CF-22)","tier":"experimental"},{"name":"pinsker","citation":"Pinsker 1964; binary Pinsker (CF-23, Wave17)","lean_theorem":"Wave17/BinaryPinsker.lean::binary_pinsker (CF-23)","tier":"experimental"},{"name":"aftershock","citation":"Reasenberg–Jones 1989; Gasperini–Lolli 2006 (α≈⅔b); USGS live feed","lean_theorem":"(seismic forecast — not a Lean theorem; generic-parameter R–J model)","tier":"live-data"},{"name":"allodial","citation":"Lutar/Allodial.lean (PR #229, merge 783a38d0)","lean_theorem":"Lutar/Allodial.lean::allodial_dominates_all / galois_preserves_allodial / ni_low_independent_of_high (EXPERIMENTAL — PROPOSED gate, not a locked theorem)","tier":"experimental"},{"name":"entanglement","citation":"Lutar/Entanglement.lean (PR #230, merge 3a7f222ed3bb)","lean_theorem":"Lutar/Entanglement.lean::capBound_antitone / entanglement_decays_under_bound (EXPERIMENTAL — PROPOSED gate, not a locked theorem)","tier":"experimental"},{"name":"sovereign","citation":"Lutar/Allodial.lean (PR #229, merge 783a38d0) — ni_low_independent_of_high","lean_theorem":"Lutar/Allodial.lean::ni_low_independent_of_high / allodial_iff_top (EXPERIMENTAL — PROPOSED gate, not a locked theorem)","tier":"experimental"}],"count":15,"doctrine":"v11","honesty":"Static runtime registry availability; not a live execution signal."}