/* ===================================================================== SZL AGENT BODY v3 — ANATOMY DOCTRINE DATA MODEL Single source of truth for the 3D anatomy. Transcribed from: team/ANATOMY_DOCTRINE.md (founder's v3 8-image roadmap) team/_PROVEN_FORMULAS.md (lutar-lean PROVEN_FORMULAS.md, kernel c7c0ba17) team/PROVE_NEXT10_REPORT.md (Wave8, main @ 7885fd9) Honesty doctrine v11 LOCKED. No fabricated metrics, no AGI, no vendor model-codenames. Quechua organ names KEPT as architectural identity, always paired with plain-English FUNCTION. ===================================================================== */ (function (root) { 'use strict'; /* ---- Kernel posture (honest, from lutar-lean main) ---- */ const KERNEL = { locked_sha: 'c7c0ba17', locked_decls: 749, locked_axioms: 14, locked_sorries: 163, main_sha: '044eb098', // Wave11–18 all merged (CF-22..28 + CUT-1 fwd), CI-green, drift-clean wave910_sha: '66735bf', // Wave9 PR #199 merged here; Wave10 PR #200 branched from it experimental_decls: 1323, experimental_axioms: 23, experimental_axioms_unique: 22, experimental_sorries: 307, toolchain: 'Lean v4.13.0 (locked) / v4.18.0 (Mathlib pinned) · main @ 044eb098', locked_proven: ['F1', 'F4', 'F7', 'F11', 'F12', 'F18', 'F19', 'F22'], experimental_count_approx: 119, // waves 5–18 instilled card set (EXPERIMENTAL · CI-green, never folded into locked 8) waves_merged: 'Wave5–23 (CF-1..28 + CUT-1 fwd + CUT-2 + Wave23 conditional BFT safety)', // Wave15 CF-22, Wave16 CF-24/25/26, Wave17 CF-23/27/28, Wave18 CUT-1 forward fragment cut2: 'Wave12 CUT-2 lambda_unique_of_separable — Λ uniqueness PROVEN CONDITIONAL on slice-multiplicativity, axiom-free, kernel-clean. Unconditional Λ stays Conjecture 1.', bft_conditional: 'Wave23 khipu_quorum_safety_conditional — Khipu BFT safety (Conjecture 2) agreement / no-split-brain PROVEN CONDITIONAL on {n>=3f+1, honest non-equivocation}, axiom-clean (PR #214, merged main @ 43bcabb7). Unconditional BFT safety stays Conjecture 2 at the sharp boundary.', slsa: 'Static space: SLSA L1 honest · product images (a11oy, killinchu) L2 build-attested (container provenance, Sigstore keyless) · L3 roadmap', gpd: 'Governed Post-Determinism — SZL\u2019s own framework. The 5 organs ARE the participant-general model: the BRAIN reasons (divergent reasoning paths are OK), the HEART / YUYAY 13-axis gate certifies semantic admissibility (deny-by-default), the SKELETON / Khipu BFT quorum = Semantic Quorum Assurance (Wave23 conditional safety theorem; unconditional = Conjecture 2), and the CIRCULATORY / YAWAR append-only receipt bus = Epistemic State Replication + Verifiable Semantic Rollback (receipts/replay live; full ESR semantics = open R&D / roadmap). The unit of agreement shifts from identical output to certified semantic admissibility. Grounded entirely in SZL\u2019s prior DOI-stamped published work (Zenodo, Apr\u2013May 2026): The Loop Is the Product v1/v2 (10.5281/zenodo.19867281, .19934129), Lineage-Aware RAG v5 (.20020846), Sealed Constitutional Guardrails v6 (.20020845), Lutar Omega Formalism v4 (.20020841), SZL Doctrine v2 — 9 Canonical Axes (.20174600). Locked-proven = exactly 8 (locked_count_eight; F4/F7/F22 joined the original 5 on 2026-06-10); \u039b = Conjecture 1.' }; /* ---- Maturity → chip styling ---- */ const MATURITY = { LOCKED: { label: 'LOCKED · kernel-verified', color: '#ffd166', desc: 'Sorry-free, Lean-core axioms only [propext, Classical.choice, Quot.sound]. Frozen @ c7c0ba17.' }, EXPERIMENTAL: { label: 'EXPERIMENTAL · CI-green', color: '#5ad1ff', desc: 'Kernel-checked by CI on main @ 7885fd9. Additive — never folded into the locked 8.' }, AXIOM_GATED: { label: 'AXIOM-GATED (disclosed)', color: '#c9a0ff', desc: 'Sorry-free given one declared, cited idealization (axiom listed in #print axioms).' }, CONDITIONAL: { label: 'CONDITIONAL · axiom-free', color: '#9ef0c0', desc: 'A kernel-clean THEOREM proven CONDITIONAL on a stated stronger hypothesis (no new axiom). Honestly NOT an unconditional result.' }, CONJECTURE: { label: 'CONJECTURE 1', color: '#ff7eb6', desc: 'Not a theorem. Conditional only within strengthened classes; unconditional uniqueness machine-checked FALSE.' } }; /* ===================================================================== FORMULA LIBRARY — keyed by id. latex = ASCII-math the in-app renderer converts to Unicode glyphs. axioms = verbatim #print axioms line. ===================================================================== */ const FORMULAS = { /* ---------- LOCKED PROVEN (exactly 8) ---------- */ F1: { id:'F1', name:'Replay-Hash Determinism', maturity:'LOCKED', latex:'replay(s0, log) = trace => replay(s0, log) = trace (bit-identical)', plain:'Replaying the SAME recorded log from the same initial state yields a BIT-IDENTICAL trace — no drift. Underpins the Khipu replay-hash gate.', axioms:'f1_replay_fold_deterministic — [propext, Classical.choice, Quot.sound]', ref:'lutar-lean PuriqFormulaLean.lean @ c7c0ba17' }, F11:{ id:'F11', name:'Ayni Reciprocity Conservation', maturity:'LOCKED', latex:'fold(append_log) : Sigma_in = Sigma_out (tit-for-tat parity)', plain:'Fold-replay of an append-only reciprocity log conserves the balance invariant (Axelrod–Hamilton tit-for-tat parity).', axioms:'f11_ayni_reciprocity_conservation — [propext, Classical.choice, Quot.sound]', ref:'lutar-lean PuriqFormulaLean.lean @ c7c0ba17' }, F12:{ id:'F12', name:'Kuramoto Coupling Boundedness (additive fragment)', maturity:'LOCKED', latex:'| Sigma_i K_i(theta) | <= Sigma_i |K_i| (bounded, additive)', plain:'The discretised reciprocity coupling stays bounded under additive superposition. HONESTY CAVEAT: additive scaffolding ONLY — NOT the full nonlinear Kuramoto synchronization.', axioms:'f12_* — [propext, Classical.choice, Quot.sound]', ref:'lutar-lean @ c7c0ba17 · caveat in Lean docstring' }, F18:{ id:'F18', name:'Reed–Solomon RS(10,6) Recovery', maturity:'LOCKED', latex:'recoverable(shards) <=> |surviving| >= 6 of 10', plain:'Erasure tolerance: data is recoverable IFF at least 6 of 10 shards survive — the resilience arithmetic for the receipt/payload encoding.', axioms:'f18_* — [propext, Classical.choice, Quot.sound]', ref:'lutar-lean @ c7c0ba17' }, F19:{ id:'F19', name:'Bekenstein Additive Scaffolding', maturity:'LOCKED', latex:'Sigma_r S(region_r) <= S(total) (additive, monotone)', plain:'Entropy budget is additive and monotone over a region partition (per-region ≤ total). HONESTY CAVEAT: monotone scaffolding ONLY — NOT the full Bekenstein bound S ≤ 2πkRE/(ℏc).', axioms:'f19_* — [propext, Classical.choice, Quot.sound]', ref:'lutar-lean @ c7c0ba17 · caveat in Lean docstring' }, F4: { id:'F4', name:'Khipu DAG Acyclicity Preservation', maturity:'LOCKED', latex:'acyclic(G) => acyclic(append_fresh_node(G)) (no back-edge cycle)', plain:'Appending a fresh node to the Khipu receipt DAG preserves acyclicity — no receipt can ever cycle back on itself. Newly kernel-verified (joined the locked set 2026-06-10).', axioms:'f4_khipu_dag_acyclic_preserved / f4_khipu_no_cycle / f4_khipu_reach_decreases / f4_khipu_append_preserves — no axioms (genuine, non-vacuous)', ref:'lutar-lean ProvedFormulas.lean @ c7c0ba17 (lutar-lean #219 + platform #321)' }, F7: { id:'F7', name:'Chaski FIFO Reception Ordering', maturity:'LOCKED', latex:'drain(enqueue_batch(c, msgs)) = msgs (reception order = send order)', plain:'Messages drain from the Chaski channel in exactly the order sent — true FIFO, no reordering. Newly kernel-verified (joined the locked set 2026-06-10).', axioms:'f7_chaski_fifo_order / f7_chaski_fifo_positional / f7_chaski_drain_eq — no axioms (genuine, non-vacuous)', ref:'lutar-lean ProvedFormulas.lean @ c7c0ba17 (lutar-lean #219 + platform #321)' }, F22:{ id:'F22', name:'Khipu Emit Append-Only Monotonicity', maturity:'LOCKED', latex:'emit(ledger) => index(ledger\') > index(ledger) (strictly increasing)', plain:'Every Khipu emit strictly increases the ledger index — append-only, never rewrites history. Newly kernel-verified (joined the locked set 2026-06-10).', axioms:'f22_khipu_emit_monotone / f22_emit_appends_length / f22_emit_strictly_greater — no axioms', ref:'lutar-lean ProvedFormulas.lean @ c7c0ba17 (lutar-lean #219 + platform #321)' }, /* ---------- WAVE 8 (experimental, green on main @ 7885fd9) ---------- */ M2: { id:'M2', name:'Hash-Chain Tamper-Evidence', maturity:'EXPERIMENTAL', latex:'H injective , p_i != q_i => head(p) != head(q)', plain:'For an injective hash step H, if any payload entry differs then the resulting head-hash differs — append-only hash chains are tamper-evident. The formal core behind receipt/audit-trail integrity.', axioms:"Lutar.Wave8.HashChain.hashchain_tamper_evident — [propext]", ref:'PR #196 @ b1c840f · Wave8/HashChain.lean' }, CP1:{ id:'CP1', name:'Conformal Marginal Coverage', maturity:'EXPERIMENTAL', latex:'numer <= (n+1)*covCount < numer + (n+1)', plain:'Split-conformal coverage satisfies a two-sided ⌈·⌉ bound — finite-sample, distribution-free marginal-coverage guarantee for the trust intervals on Λ.', axioms:'Lutar.Wave8.Conformal.conformal_marginal_coverage — [propext, Quot.sound]', ref:'PR #196 @ b1c840f · Wave8/Conformal.lean' }, B1: { id:'B1', name:'Byzantine Impossibility (n=3, f=1)', maturity:'EXPERIMENTAL', latex:'3 <= 3*f => no decider agrees with all-false AND all-true', plain:'The classic 3-node / 1-fault Byzantine impossibility — the formal n ≥ 3f+1 lower bound. Justifies consensus/quorum sizing in the shared mesh and rejects under-provisioned fault tolerance.', axioms:'Lutar.Wave8.Byzantine.byzantine_impossibility_3_1 — does not depend on any axioms', ref:'PR #196 @ b1c840f · Wave8/Byzantine.lean' }, B2: { id:'B2', name:'Khipu BFT Safety (conditional)', maturity:'CONDITIONAL', latex:'n>=3f+1 && honest non-equivocation => two quorums certifying v1,v2 => v1 = v2', plain:'Conjecture 2 (Khipu BFT safety) — agreement / no-split-brain PROVEN axiom-free CONDITIONAL on n>=3f+1 and honest non-equivocation under signed votes. Byzantine organs MAY equivocate in the model and safety still holds. Unconditional BFT safety stays Conjecture 2 at the sharp boundary.', axioms:'Lutar.Wave23.QuorumSafety.khipu_quorum_safety_conditional — [propext, Classical.choice, Quot.sound]', ref:'PR #214 @ 43bcabb7 · Wave23/QuorumSafety.lean' }, S2: { id:'S2', name:'Simplex Safety Invariant', maturity:'EXPERIMENTAL', latex:'RC safe , (mon pass => AC safe) => forall t, state_t safe', plain:'Simplex/RTA run-time-assurance: a monitored switch to a verified recovery controller keeps the system in the safe set for ALL time. Backbone of fail-safe autonomy and the HUKLLA deadman reflex.', axioms:'Lutar.Wave8.Simplex.simplex_safety_invariant — [propext]', ref:'PR #196 @ b1c840f · Wave8/Simplex.lean' }, G1: { id:'G1', name:'CPA Minimality', maturity:'EXPERIMENTAL', latex:'cpaTime = argmin_t sep2(t) (unique minimizer)', plain:'The closest-point-of-approach time is the UNIQUE minimizer of squared separation. Formal anchor for killinchu collision / conflict-risk timing.', axioms:'Lutar.Wave8.CPA.cpa_unique — [propext, Classical.choice, Quot.sound]', ref:'PR #197 @ 7885fd9 · Wave8/CPA.lean' }, L2: { id:'L2', name:'Deny-by-Default Uniqueness', maturity:'EXPERIMENTAL', latex:'D monotone & diagonal & conservative => D == vmin (everywhere)', plain:'The min-gate vmin is the UNIQUE monotone, diagonal, conservative gate — the weakest-link trust gate is the ONLY policy satisfying the safety axioms; no permissive aggregator can sneak in. Backs the YUYAY deny-by-default conjunction.', axioms:'Lutar.Wave8.MinGate.deny_by_default_unique — [propext]', ref:'PR #196 @ b1c840f · Wave8/MinGate.lean' }, Q1: { id:'Q1', name:'Density-Matrix Mixture PSD', maturity:'EXPERIMENTAL', latex:'Sigma_i w_i rho_i PSD & unit-trace (w_i>=0, Sigma w_i = 1)', plain:'A convex combination of PSD, unit-trace matrices is again a valid density matrix — convexity of the mixed-state set. Underpins probabilistic ensemble reasoning in the YACHAY quantum-mind region.', axioms:'Lutar.Wave8.DensityMixture.density_matrix_mixture — [propext, Classical.choice, Quot.sound]', ref:'PR #197 @ 7885fd9 · Wave8/DensityMixture.lean' }, Q2: { id:'Q2', name:'Gershgorin Governance Non-Degeneracy (real)', maturity:'EXPERIMENTAL', latex:'Sigma_{j!=k} |W_kj| < |W_kk| => det W != 0 => W x = b unique', plain:'A strictly diagonally-dominant real governance weight matrix is invertible, so weighted aggregation has a unique solution — no zero-eigenvalue collapse of the governance operator. (ℂ variant left honestly as ROADMAP — shipped real-valued only, sorryAx-free.)', axioms:'Lutar.Wave8.Gershgorin.governance_nonsingular_real — [propext, Classical.choice, Quot.sound]', ref:'PR #197 @ 7885fd9 · Wave8/Gershgorin.lean' }, L3: { id:'L3', name:'Λ Strict Monotonicity', maturity:'EXPERIMENTAL', latex:'x_i > 0 , x <= y , x_k < y_k => Lambda(x) < Lambda(y)', plain:'The geometric-mean trust aggregator is per-component strictly monotone: improving any input strictly raises the fused trust. NO uniqueness of Λ asserted — Conjecture 1 untouched.', axioms:'Lutar.Wave8.LambdaMono.gmean_strict_mono — [propext, Classical.choice, Quot.sound]', ref:'PR #197 @ 7885fd9 · Wave8/LambdaMono.lean' }, Ph1:{ id:'Ph1', name:'Axiom-Disclosure Soundness', maturity:'EXPERIMENTAL', latex:'axiomsAllowed(S) => every a in S is a Lean kernel axiom', plain:'The axiom-disclosure gate is sound; locked_count_eight proves there are EXACTLY 8 locked entries with kernel-only axioms (= by decide, no axioms). Mechanically enforces "no hidden axioms".', axioms:'Lutar.Wave8.AxiomDisclosure.disclosure_sound — [propext, Quot.sound] · locked_count_eight — no axioms', ref:'PR #196 @ b1c840f · Wave8/AxiomDisclosure.lean' }, /* ---------- WAVE 9 + WAVE 10 (experimental, CI-green on main @ 66735bf) ---------- PR #199 (Wave9) merged @ 66735bf; Wave10 PR #200. EXPERIMENTAL · CI-green — kernel-verified, NEVER folded into the locked 8. Λ stays Conjecture 1. Live computation surfaces shipped in killinchu /api/killinchu/v1/wave910/*. */ W9_GERSH:{ id:'MA1', name:'Gershgorin Spectral Non-Degeneracy (incl. ℂ)', maturity:'EXPERIMENTAL', latex:'strict diag dominance => 0 in no Gershgorin disc => no zero eigenvalue => W nonsingular', plain:'Wave9 SPECTRAL Gershgorin: a strictly diagonally-dominant matrix (field-general, incl. ℂ) has no zero eigenvalue, hence is nonsingular and det is a unit. A cheap pre-flight gate on the governance/command-trust matrix BEFORE aggregation. DISTINCT from the Wave8 ℝ determinant-form card (Q2) — both kept.', axioms:'Lutar.Wave9.Gershgorin.no_zero_eigenvalue / nonsingular_of_strict_diag_dominant / isUnit_det_of_strict_diag_dominant — [propext, Classical.choice, Quot.sound]', ref:'PR #199 @ 66735bf · Wave9/Gershgorin.lean' }, W9_CI:{ id:'OE-2', name:'Covariance-Intersection PSD Convex Closure', maturity:'EXPERIMENTAL', latex:'P_ci^{-1} = w P_a^{-1} + (1-w) P_b^{-1} => P_ci PSD & conservative', plain:'Fuse two sensors that see the same target WITHOUT knowing their cross-covariance. The CI information matrix is PSD as a non-negative convex combination of PSD information matrices, so the fused covariance is always a valid, never-overconfident uncertainty. (Full inverted-covariance Loewner monotonicity left honestly as ROADMAP.)', axioms:'Lutar.Wave9.CovarianceIntersection.posSemidef_convex_comb / ci_information_psd — [propext, Classical.choice, Quot.sound]', ref:'PR #199 @ 66735bf · Wave9/CovarianceIntersection.lean' }, W9_MENGER:{ id:'L-Menger', name:'Menger Cut/Path Duality (mesh redundancy)', maturity:'EXPERIMENTAL', latex:'#edge-disjoint paths(s,t) <= minCut(s,t) ; cut blocks reachability', plain:'The number of edge-disjoint routes between two mesh nodes is bounded by the min-cut, and any cut blocks reachability. With k edge-disjoint paths the route survives any k-1 link failures — fail-safe routing, not a hope. (Full min-max Menger equality left honestly as ROADMAP.)', axioms:'Lutar.Wave9.Menger.cut_blocks_reachable — [] · disjoint_paths_le_cut — [propext, Classical.choice, Quot.sound]', ref:'PR #199 @ 66735bf · Wave9/Menger.lean' }, W9_MERKLE:{ id:'CP-1', name:'Merkle Transparency-Log Soundness', maturity:'AXIOM_GATED', latex:'Inj H => inclusion proof re-derives root ; append-only root binding', plain:'Every receipt is committed to a SHA-256 Merkle root; any single receipt\u2019s inclusion proof can be re-verified offline against that root, and the log is append-only. The transparency-log backbone for the YAWAR receipt bus. AXIOM-GATED: collision-resistance is an abstract HYPOTHESIS (Inj H) in Lean — SHA-256 is the concrete instance.', axioms:'Lutar.Wave9.Merkle.merkle_root_binding / merkle_inclusion_sound / merkle_append_only — [propext] (Inj H hypothesis disclosed)', ref:'PR #199 @ 66735bf · Wave9/Merkle.lean' }, W9_BDB:{ id:'C1', name:'Basilic Byzantine-BDB Threshold', maturity:'EXPERIMENTAL', latex:'safe <=> n > 3t + d + 2q (t Byzantine, d deceitful, q benign-faulty)', plain:'A SHARPER fault threshold than the classic n > 3t: with t Byzantine, d deceitful and q benign-faulty nodes, safety holds iff n > 3t + d + 2q. The mesh needs fewer nodes for the same guarantee (quorum-sizing efficiency). (Full protocol-level solvability left honestly as ROADMAP.)', axioms:'Lutar.Wave9.BasilicBDB.bdb_safe — [propext, Quot.sound] · bdb_threshold_dichotomy — [propext, Classical.choice, Quot.sound]', ref:'PR #199 @ 66735bf · Wave9/BasilicBDB.lean' }, W10_STL:{ id:'RA-1', name:'STL Robustness — two-sided Donzé–Maler', maturity:'EXPERIMENTAL', latex:'Sat => rho >= 0 ; rho > 0 => Sat ; rho < 0 => violation (NOT the iff Sat <=> rho>0)', plain:'A runtime monitor that not only says pass/fail but computes a signed robustness margin ρ — how far a signal is from violating a maritime/drone C2 rule. The PROVEN guarantee is TWO-SIDED, NOT the naive iff Sat ↔ ρ>0 (FALSE at the ρ=0 boundary). Strengthens the HUKLLA deadman reflex with a sound margin.', axioms:'Lutar.Wave10.STLRobustness.rho_sound / rho_pos_sound / rho_neg_violation — [propext, Quot.sound]', ref:'PR #200 (Wave10) · Wave10/STLRobustness.lean' }, W10_REPLAY:{ id:'AU-1', name:'Replay-Determinism + Tamper Localization', maturity:'EXPERIMENTAL', latex:'replay(log) == replay(log) ; first divergence => localizes tampered entry', plain:'Replaying the same ordered receipt log yields the same final state, and if one entry is altered the audit pinpoints exactly which one (first divergence). Together with Merkle inclusion: a re-verifiable, tamper-localizing audit trail on YAWAR. Axiom-free core.', axioms:'Lutar.Wave10.ReplayDeterminism.replay_deterministic — (none) · tamper_localized — (none) · replay_append — [propext, Quot.sound]', ref:'PR #200 (Wave10) · Wave10/ReplayDeterminism.lean' }, W10_QUORUM:{ id:'CN-1', name:'Quorum-Intersection (Flexible Paxos)', maturity:'EXPERIMENTAL', latex:'any two intersecting quorums => unique decision (no split-brain)', plain:'If any two quorums intersect, no two quorums can ever decide differently — no split-brain in C2 consensus. Majority quorums always intersect (Flexible Paxos sizing). The agreement/unique-decision core depends on NO axioms.', axioms:'Lutar.Wave10.QuorumIntersection.quorum_intersection_agreement / quorum_unique_decision — does not depend on any axioms · majority_quorums_intersect — [propext, Quot.sound]', ref:'PR #200 (Wave10) · Wave10/QuorumIntersection.lean' }, W10_REACH:{ id:'MR-1', name:'Reachability-Redundancy (route monotonicity)', maturity:'EXPERIMENTAL', latex:'add edge => reachability monotone ; edge-avoiding reach <= full reach', plain:'Adding links never removes reachability, and reachability that avoids a failed edge is bounded by full reachability — the monotonicity backbone that pairs with Menger to certify k-1 link-failure survival in the mesh. Axiom-free core.', axioms:'Lutar.Wave10.ReachabilityRedundancy.reach_mono — (none) · avoiding_reach_le_full — (none)', ref:'PR #200 (Wave10) · Wave10/ReachabilityRedundancy.lean' }, /* ---------- WAVE 11 (experimental, CI-green on main @ 044eb098) ---------- PR #201. EXPERIMENTAL · CI-green; #print axioms ⊆ {propext, Classical.choice, Quot.sound}. Never folded into the locked 8. */ CF1:{ id:'CF-1', name:'Graph Auto-Distance Invariance', maturity:'EXPERIMENTAL', latex:'phi graph automorphism => d(phi u, phi v) = d(u, v)', plain:'A graph automorphism preserves shortest-path distance — relabelling the mesh by a symmetry never changes routing distances. Structural invariant behind topology-aware routing.', axioms:'Lutar.Wave11.GraphAutoDist.* — [propext, Classical.choice, Quot.sound]', ref:'PR #201 @ 044eb098 · Wave11' }, CF5:{ id:'CF-5', name:'Immune Neyman–Pearson Optimality', maturity:'EXPERIMENTAL', latex:'likelihood-ratio test = most powerful at fixed false-alarm rate', plain:'The CHAPAQ-style egress detector that thresholds a likelihood ratio is the most powerful test at any fixed false-alarm rate (Neyman–Pearson). The optimality basis for the immune inspector.', axioms:'Lutar.Wave11.ImmuneNeymanPearson.* — [propext, Classical.choice, Quot.sound]', ref:'PR #201 @ 044eb098 · Wave11' }, /* ---------- WAVE 12 (experimental + CUT-2 conditional, CI-green on main @ 044eb098) ---------- PR #202. CUT-2 is a CONDITIONAL, axiom-free THEOREM — it gets Λ OFF bare conjecture (conditional only). Unconditional Λ uniqueness stays Conjecture 1 (machine-checked FALSE). */ CUT2:{ id:'CUT-2', name:'Λ Conditional Uniqueness (slice-multiplicativity)', maturity:'CONDITIONAL', latex:'Φ separable & per-axis multiplicative & monotone & A1A2A3A5 => Φ = Λ', plain:'Λ uniqueness is PROVEN as a theorem CONDITIONAL on slice-multiplicativity (separability) — axiom-free and kernel-clean. This gets Λ OFF bare conjecture honestly. UNCONDITIONAL Λ uniqueness under bare A1–A5 stays Conjecture 1 (provably FALSE — maxAgg/min counterexamples). NOT folded into the locked 8.', axioms:'Lutar.Round13.lambda_unique_of_separable — [propext, Classical.choice, Quot.sound] (NO new axiom)', ref:'PR #202 @ 044eb098 · Round13/LambdaSeparable.lean' }, CF13:{ id:'CF-13', name:'DEQ Input-Lipschitz Well-Posedness', maturity:'EXPERIMENTAL', latex:'dist(z*(x), z*(y)) <= Lx/(1-K) · dist(x, y)', plain:'A deep-equilibrium / fixed-point layer has a UNIQUE equilibrium that depends Lipschitz-continuously on its input with constant Lx/(1−K) — the model’s equilibrium reasoning is provably well-posed and stable to input perturbation. Margin badge for the code/forecast routing layer.', axioms:'Lutar.Innovations.Round5.InputLipschitz.equilibrium_dist_le / equilibrium_lipschitz — [propext, Classical.choice, Quot.sound]', ref:'PR #202 @ 044eb098 · round5/OuroLoopInputLipschitz.lean' }, CF17:{ id:'CF-17', name:'Floating-Point Summation Error Bound', maturity:'EXPERIMENTAL', latex:'|recSum(xs,δ) - Σxi| <= ((1+u)^(n-1) - 1) · Σ|xi|', plain:'Recursive floating-point summation under the standard rounding model fl(a+b)=(a+b)(1+δ), |δ|≤u has a provable forward error bound (Higham §2.2). Numeric-stability badge for any aggregation/scoring sum.', axioms:'Lutar.Khipu.NumericStability.recSum_error_le — [propext, Classical.choice, Quot.sound]', ref:'PR #202 @ 044eb098 · Khipu/NumericStability.lean' }, /* ---------- WAVE 13 (experimental, CI-green on main @ 044eb098) ---------- PR #203. PRNG completeness closed (−1 baseline sorry) + 2 experimental shadows. */ W13_REPLAY:{ id:'CF-RR', name:'Replay-Root Completeness', maturity:'EXPERIMENTAL', latex:'s ∈ candidates ∧ IsReplayRoot(s) => findReplayRoot(candidates).isSome', plain:'If a valid replay-root exists among the candidates, the search provably finds one — the PRNG replay-root lookup is complete. Closed a baseline sorry; axioms {propext, Quot.sound}.', axioms:'Lutar.PRNG.findReplayRoot_complete — [propext, Quot.sound]', ref:'PR #203 @ 044eb098 · PRNG/K10v2_ReplayRoot.lean' }, W13_QUORUM:{ id:'CF-QV', name:'Quorum Single-Valued Vote (non-Byzantine shadow)', maturity:'EXPERIMENTAL', latex:'n ≥ 3f+1 , two quorums (≥ n−f) , single-valued votes => v1 = v2', plain:'Under n ≥ 3f+1, any two large quorums of single-valued voters must agree — no split decision. HONEST SCOPE: this is the explicitly NON-Byzantine shadow (a faulty organ cannot equivocate here); it is NOT Khipu Conjecture 2, which stays OPEN.', axioms:'Lutar.Wave13.Sweep.quorum_agreement_single_valued_vote — [propext, Classical.choice, Quot.sound]', ref:'PR #203 @ 044eb098 · Wave13/Sweep.lean' }, W13_HM:{ id:'CF-HM', name:'HLP Harmonic-Mean Bottleneck', maturity:'EXPERIMENTAL', latex:'n / Σ(1/xi) < threshold => ∃ i, xi < threshold', plain:'If the harmonic mean of positive resources falls below a threshold, some single resource must be below it — a clean Hardy–Littlewood–Pólya bottleneck detector for the mesh. Clean inverse-form companion (no rpow).', axioms:'Lutar.Wave13.Sweep.hm_bottleneck_clean — [propext, Classical.choice, Quot.sound]', ref:'PR #203 @ 044eb098 · Wave13/Sweep.lean' }, /* ---------- WAVE 14 (experimental frontier pack, CI-green on main @ 044eb098) ---------- PR #204. 9 kernel-clean theorems; all #print axioms ⊆ {propext, Classical.choice, Quot.sound}. */ CF18:{ id:'CF-18', name:'Mādhava / Leibniz Alternating-Series Remainder', maturity:'EXPERIMENTAL', latex:'a antitone , Σ(-1)^i a_i -> L => |Σ_{i disagree on ≥ n−k+1 of n points', plain:'Two distinct degree- 0 <= Σ p·log(p/q)', plain:'The log-sum inequality and Gibbs’ inequality — the correctly-stated information-theory DPI core (Cover–Thomas Thm 2.7.1 / 2.6.3). HONEST: this does NOT repair the in-tree DPO klDivergence/pinsker, which stay FALSE-as-stated (no simplex hypothesis).', axioms:'Lutar.Wave14.log_sum_inequality / gibbs_inequality — [propext, Classical.choice, Quot.sound]', ref:'PR #204 @ 044eb098 · Wave14/LogSumInequality.lean' }, /* ---------- WAVE 15 (experimental + CUT-1 bridge, CI-green on main @ 044eb098) ---------- PR #205. CF-22 conditionally repairs the FALSE-as-stated DPO axiom (axiom-free, ON the simplex). All #print axioms ⊆ {propext, Classical.choice, Quot.sound}. The UNCONDITIONAL DPO axiom klDivergence_nonneg stays FALSE-as-stated (token untouched). */ CF22:{ id:'CF-22', name:'DPO KL-Divergence Nonneg on the Simplex (conditional repair)', maturity:'EXPERIMENTAL', latex:'p, q ∈ Δ => KL(p‖q) = Σ p·log(p/q) >= 0', plain:'CONDITIONALLY repairs the FALSE-as-stated in-tree DPO axiom: KL ≥ 0 holds once p,q are constrained to the probability simplex (Gibbs). Live demo KL(P‖Q)=0.0880 ≥ 0 (χ²=0.1917). HONEST: the UNCONDITIONAL DPO axiom klDivergence_nonneg stays FALSE-as-stated — only the simplex-restricted statement is the theorem. Independent confirmation: χPO (arXiv:2407.13399), f-DPO (arXiv:2309.16240).', axioms:'Lutar.Wave15.klDivergence_nonneg_simplex / dpo_klDivergence_nonneg_on_simplex — [propext, Classical.choice, Quot.sound]', ref:'PR #205 @ 044eb098 · Wave15/DPOKLSimplex.lean' }, /* ---------- WAVE 16 (experimental, CI-green on main @ 044eb098) ---------- PR #206. CF-24 geoBin satisfies FULL Aczél quasi-arithmetic axioms (real CUT-1 progress); CF-25 Λ scale-invariance; CF-26 abacus place-value. 13 theorems, axiom-clean. */ CF24:{ id:'CF-24', name:'geoBin Full Aczél Quasi-Arithmetic Axioms', maturity:'EXPERIMENTAL', latex:'geoBin: idempotent ∧ commutative ∧ homogeneous ∧ monotone (Aczél QAM axioms)', plain:'The geometric-binary mean satisfies the FULL Aczél quasi-arithmetic-mean axiom set (idempotency, commutativity, homogeneity, strict monotonicity) — real progress on the CUT-1 characterization route. Backs the per-axis generator form of the 13-axis Λ. Regularity-free QAM characterization (Burai–Kiss–Szokol, arXiv:2107.07391) shows bisymmetry yields continuity for free.', axioms:'Lutar.Wave16.geoBin_idem / geoBin_comm / geoBin_homog / geoBin_mono — [propext, Classical.choice, Quot.sound]', ref:'PR #206 @ 044eb098 · Wave16/GeoBinAczel.lean' }, CF25:{ id:'CF-25', name:'Λ Scale-Invariance (affine reparam of generator)', maturity:'EXPERIMENTAL', latex:'Λ(α·x + β) invariant under affine reparam of the generator (α>0)', plain:'Λ is invariant under affine reparametrization of its quasi-arithmetic generator and under axis normalization — rescaling the trust axes leaves the Λ verdict fixed. Convex-duality backing (Nielsen, arXiv:2301.10980): QAMs are gradient maps of Legendre-type convex functions, equivariant under affine duality.', axioms:'Lutar.Wave16.lambda_scale_axes / lambda_normalization_invariant — [propext, Classical.choice, Quot.sound]', ref:'PR #206 @ 044eb098 · Wave16/LambdaScaleInvariance.lean' }, CF26:{ id:'CF-26', name:'Abacus Place-Value Soundness', maturity:'EXPERIMENTAL', latex:'Σ digit_i · base^i = value (place-value encode/decode round-trip)', plain:'Place-value (abacus) encoding and decoding round-trip exactly — a clean positional-number-system soundness lemma underpinning deterministic integer serialization in receipts.', axioms:'Lutar.Wave16.abacus_place_value — [propext, Classical.choice, Quot.sound]', ref:'PR #206 @ 044eb098 · Wave16/Abacus.lean' }, /* ---------- WAVE 17 (experimental, CI-green on main @ 044eb098) ---------- PR #207. CF-23 FULL binary Pinsker (the long-sought headline); CF-27 monDEQ uniqueness; CF-28 recurrent-depth Lipschitz. 24 theorems, axiom-clean. */ CF23:{ id:'CF-23', name:'Full Binary Pinsker Inequality', maturity:'EXPERIMENTAL', latex:'2·(p − q)^2 <= KL(Bern p ‖ Bern q) (binary Pinsker)', plain:'The full binary Pinsker inequality — KL ≥ 2·TV² for Bernoulli distributions — the long-sought headline result (previously only a named Lean axiom). Live demo KL=0.0823 ≥ 2·TV²=0.0800. Gives a confidence-margin bound for any binary gate. HONEST: still experimental CI-green tier, NOT folded into the locked 8.', axioms:'Lutar.Wave17.binary_pinsker / binary_inv_sum_ge_four — [propext, Classical.choice, Quot.sound]', ref:'PR #207 @ 044eb098 · Wave17/BinaryPinsker.lean' }, CF27:{ id:'CF-27', name:'monDEQ Strong-Monotonicity ⇒ Unique Equilibrium', maturity:'EXPERIMENTAL', latex:'F strongly monotone => ∃! z*, F(z*) = z* (unique fixed-point)', plain:'A monotone deep-equilibrium operator that is strongly monotone has a UNIQUE equilibrium — the fixed-point reasoning layer is provably well-posed. Backs the uniqueness narrative for fusion fixed-points and tool-call resolution (Winston–Kolter monDEQ).', axioms:'Lutar.Wave17.monDEQ_unique_equilibrium — [propext, Classical.choice, Quot.sound]', ref:'PR #207 @ 044eb098 · Wave17/MonDEQUnique.lean' }, CF28:{ id:'CF-28', name:'Recurrent-Depth Kʳ-Lipschitz Contraction', maturity:'EXPERIMENTAL', latex:'r-fold recurrence with K-Lipschitz step => Kʳ-Lipschitz overall', plain:'An r-fold recurrent-depth block built from a K-Lipschitz step is Kʳ-Lipschitz overall — depth amplifies (K<1 ⇒ contraction; K>1 ⇒ honest blow-up bound). Stability budget for recurrent-depth estimators (mcleish7/retrofitting-recurrence, Apache-2.0).', axioms:'Lutar.Wave17.recurrent_depth_lipschitz — [propext, Classical.choice, Quot.sound]', ref:'PR #207 @ 044eb098 · Wave17/RecurrentDepthLipschitz.lean' }, /* ---------- WAVE 18 (CUT-1 FORWARD FRAGMENT — experimental + OPEN GAP, main @ 044eb098) ---------- 19 axiom-clean theorems toward the CUT-1 unconditional Λ characterization. STILL CONDITIONAL: the standing gap is `dyadic_image_dense` (the dense-domain step) — multi-week roadmap, NOT done. Λ unconditional uniqueness stays Conjecture 1 (machine-checked FALSE). */ CUT1:{ id:'CUT-1', name:'CUT-1 Forward Fragment (generator unique up to affine)', maturity:'CONDITIONAL', latex:'expMidpoint(x,y) = √(xy) ; generator unique up to affine ; cut1_conditional_lambda', plain:'The forward fragment of the CUT-1 unconditional-uniqueness program: the generator is unique up to affine reparam, the exponential midpoint equals the geometric mean √(xy), and Λ follows CONDITIONALLY (19 axiom-clean theorems). HONEST OPEN GAP: `dyadic_image_dense` (the dense-domain density step, n-adic recursive construction per Kiss–Shulman 2026) is NOT proven — multi-week roadmap. Λ unconditional uniqueness stays Conjecture 1. NOT folded into the locked 8.', axioms:'Lutar.Wave18.generator_unique_up_to_affine / expMidpoint_eq_geom / cut1_conditional_lambda — [propext, Classical.choice, Quot.sound] · GAP: dyadic_image_dense (open sorry, roadmap)', ref:'PR #208 @ 044eb098 · Wave18/CUT1Forward.lean' }, /* ---------- EARLIER EXPERIMENTAL (waves 5-7 / agentic) ---------- */ W5_1:{ id:'W5-1', name:'AM–GM No-Inflation', maturity:'EXPERIMENTAL', latex:'GM(x) <= AM(x) (Lambda never inflates trust)', plain:'Geometric mean ≤ arithmetic mean: the Λ aggregator can never inflate trust above the naive average.', axioms:'wave-5 — 0 new axioms (Mathlib-dep CI-green)', ref:'PR #186 @ b71114cf' }, W7_5:{ id:'W7-5', name:'PAC-Bayes Routing Envelope', maturity:'EXPERIMENTAL', latex:'R(rho) <= R_hat(rho) + sqrt( (KL(rho||pi)+ln(2/delta)) / 2m )', plain:'A PAC-Bayes generalization envelope bounds true routing risk by empirical risk plus a KL complexity term — confidence on model routing.', axioms:'wave-7 — 0 new axioms', ref:'PR #190 @ d6a232ba' }, P1: { id:'P1', name:'Receipt-Completeness', maturity:'EXPERIMENTAL', latex:'every hop => exactly one chained receipt (no drop/reorder)', plain:'Every hop in the governed loop leaves exactly one chained receipt — no silent drop or reorder.', axioms:'agentic-loop — axiom-free core', ref:'PR #188 @ 2ede47a2' }, P3: { id:'P3', name:'Non-Interference (Goguen–Meseguer)', maturity:'EXPERIMENTAL', latex:'poisoned retrieval =/=> flip(DENY -> ALLOW)', plain:'Poisoned / untrusted retrieval provably CANNOT flip a DENY to ALLOW (Cannonico bullseye).', axioms:'P3 — PROVEN, axiom-free core', ref:'PR #188 @ 2ede47a2' }, P4: { id:'P4', name:'Replay-Determinism (loop)', maturity:'EXPERIMENTAL', latex:'rerun(recorded) => byte-identical receipt chain', plain:'Re-running a recorded run reproduces a byte-identical receipt chain.', axioms:'P4 — PROVEN, axiom-free', ref:'PR #188 @ 2ede47a2' }, P5: { id:'P5', name:'Tamper-Evidence (loop)', maturity:'AXIOM_GATED', latex:'mutate(any receipt) => re-verify REJECTS', plain:'Any single-receipt mutation makes re-verify reject. AXIOM-GATED on hashFn_collision_resistant (NIST FIPS 180-4, disclosed).', axioms:'P5 — AXIOM-GATED [hashFn_collision_resistant]', ref:'PR #188 @ 2ede47a2' } }; /* ===================================================================== ORGANS — anatomical placement. pos = [x,y,z] in a single body's local frame (y up = head, y down = feet; chest ~ +0.6, head ~ +2.4). The two bodies are translated ±X in app.js. `system` keys into SYSTEMS. ===================================================================== */ // Region tags drive color: heart, blood, brain, nerve, skeleton, gate, audit, mesh const ORGANS = [ /* HEART — YUYAY (the beating Λ center, shared) */ { key:'yuyay', system:'heart', quechua:'YUYAY', fn:'13-axis CONJUNCTIVE truth gate', pos:[0,0.55,0.18], scale:0.42, color:'#ff5d8f', shared:true, beat:true, blurb:'Every proposal (thought · action · tool call) clears 13 axes CONJUNCTIVELY or is rejected and receipted. pass = all(score[i] >= floor[i]) — NOT a weighted average. 0.94 on moralGrounding FAILS even if all other 12 = 1.00. Emits the Λ-signed receipt. The beating Λ heart = geometric-mean trust over the axes.', formulas:['CUT2','CUT1','CF25','CF24','L3','L2','CP1','W5_1','CF21'], lambda_note:true, axes:'A01 moralGrounding≥0.95 · A02 measurabilityHonesty≥0.95 · A03 empiricalGrounding≥0.90 · A04 logicalConsistency≥0.90 · A05 sourceTransparency≥0.90 · A06 reproducibility≥0.90 · A07 licenseHygiene≥0.90 · A08 scopeDiscipline≥0.90 · A09 claimCalibration≥0.90 · A10 evalAwareness · A11 deceptionKeywords · A12 conflictingDirectives · A13 reversalDirective(STOP→halt)' }, /* BRAIN — YACHAY cortex (read-only reasoning cortex), at the head */ { key:'amaru', system:'brain', quechua:'YACHAY', fn:'read-only reasoning cortex (5 regions + quantum mind) · proposer', pos:[0,2.35,0.05], scale:0.5, color:'#7c5cff', blurb:'The cortex hangs off the bus by a SINGLE tether: it READS frozen snapshots, NEVER WRITES — the thinking layer cannot tamper with the record. 5 regions: PREFRONTAL (the 13-axis wisdom gate = the heart) · FRONTAL (proposer = RIMAY) · TEMPORAL (retrieval/RAG) · PARIETAL (K-candidate sim = MUSQUY) · OCCIPITAL (tool surface = MCP) · QUANTUM MIND (ρ 4×4, λ_min ≥ 0.225).', formulas:['Q1','Q2','W7_5','W9_CI','W9_GERSH','CF13','CF17','CF18','CF22','CF27','CF28'] }, /* CIRCULATORY / BLOOD — YAWAR (the vessel network spine), chest→abdomen */ { key:'yawar', system:'blood', quechua:'YAWAR', fn:'append-only SHA-256 receipt bus', pos:[0,-0.15,0.2], scale:0.34, color:'#ff3b5c', blurb:'h = sha256(json.dumps(packet, sort_keys=True)).hexdigest() → appended as [hash, packet]; never mutated, never deleted. Every component READS from YAWAR (snapshots frozen per layer). This is the audit-truth: you cannot rewrite history.', formulas:['M2','P1','F18','F1','W9_MERKLE','W10_REPLAY','CF19','W13_REPLAY','CF26'] }, { key:'ruway', system:'blood', quechua:'RUWAY', fn:'sole authorized write surface', pos:[-0.34,-0.05,0.16], scale:0.2, color:'#ff7a6b', blurb:'The ONLY authorized write surface. Every ceremonial write commits through RUWAY; all writes traverse CHAPAQ egress inspection. D-YAWAR-FLOW enforced.', formulas:['P4','F11'] }, { key:'sentra', system:'blood', quechua:'CHAPAQ', fn:'egress immune inspector', pos:[0.34,-0.05,0.16], scale:0.2, color:'#ff9e6b', blurb:'Egress immune inspector — 6 signatures + DoS guard (~18 SLOC). All writes traverse CHAPAQ before reaching the bus. The body\u2019s immune checkpoint at the vessel wall.', formulas:['P5','M2','CF5'] }, /* NERVOUS SYSTEM — span propagation + HUKLLA reflex */ { key:'huklla', system:'nerve', quechua:'HUKLLA', fn:'deadman tripwire (reflex arc)', pos:[0,1.5,-0.18], scale:0.18, color:'#5ad1ff', blurb:'DEADMAN REFLEX ARC: HUKLLA tripwire fires → span context frozen at pre-cycle value → halt signal into the HATUN root span → all child spans cancelled. The spinal reflex that halts the organism on anomaly.', formulas:['S2','B1','W10_STL','W9_MENGER','W10_REACH','W13_HM','CF23'] }, { key:'vsp', system:'nerve', quechua:'VSP / OTel', fn:'span lineage (efferent · afferent · proprioceptive)', pos:[0,1.0,-0.22], scale:0.2, color:'#5ad1ff', blurb:'W3C TraceContext: trace_id · span_id · parent_span_id propagate brain → every effector. Replay verifier checks child.parent_span_id == parent.span_id across a cycle. 3 nerve classes: EFFERENT (motor HATUN→YACHAY→YUYAY) · AFFERENT (sensory YAWAR→HATUN) · PROPRIOCEPTIVE (self-monitor R0513→HATUN).', formulas:['P4','F1'] }, /* GOVERNANCE / SKELETON anchors */ { key:'hatun', system:'skeleton', quechua:'HATUN', fn:'sovereign orchestrator + seal (the crown)', pos:[0,2.95,0], scale:0.26, color:'#ffd166', blurb:'Sovereign orchestrator (~199 SLOC): long-horizon multi-subagent dispatch, energy-gated (Butler–Volmer), doctrine-gated (YUYAY per cycle), cryptographic receipts on YAWAR. SOVEREIGN SEAL: identity-trace to a HUMAN PRINCIPAL · 10-tripwire egress · byte-deterministic commit · 5× replay verified. The seal also enforces the AXIOM-DISCLOSURE honesty gate (Ph1): exactly 8 locked-proven, no hidden axioms.', formulas:['Q2','P1','Ph1','W9_GERSH','W10_QUORUM','W9_BDB','CF20','W13_QUORUM','CF1'] }, { key:'overwatch', system:'audit', quechua:'R0513 / OVERWATCH', fn:'read-only 5-invariant audit', pos:[0,0.1,-0.24], scale:0.2, color:'#9ef0c0', blurb:'5 invariants, READ-ONLY: I1 KL drift · I2 joint margin · I3 TUKUY re-gate · I5 Maxwell rigidity · I6 continuum-hash chain. Event-log lines only; does NOT halt or gate; CRITICAL alerts notify the operator.', formulas:['M2','B1','CP1','W9_MERKLE','W10_REPLAY'] }, { key:'tukuy', system:'skeleton', quechua:'TUKUY', fn:'egress actuator', pos:[0.3,-1.6,0.05], scale:0.16, color:'#ffd166', blurb:'Egress actuator (~70 SLOC). The hand that acts on the world only after YUYAY passes and CHAPAQ clears — re-gated by R0513 invariant I3.', formulas:['S2','G1'] }, { key:'musquy', system:'brain', quechua:'MUSQUY', fn:'K-candidate simulation (parietal)', pos:[-0.28,1.95,0.0], scale:0.16, color:'#7c5cff', blurb:'K-candidate simulation (~219 SLOC) in the PARIETAL region — imagines K futures, scores each through the gate, never commits until YUYAY passes.', formulas:['Q1','W7_5'] } ]; /* ===================================================================== SYSTEMS legend (the five) + governance overlay ===================================================================== */ const SYSTEMS = [ { key:'heart', name:'HEART', organ:'YUYAY v3', fn:'13-axis conjunctive critique gate · emits Λ-signed receipt', color:'#ff5d8f' }, { key:'blood', name:'CIRCULATORY / BLOOD', organ:'YAWAR', fn:'append-only SHA-256 receipt bus · RUWAY sole write · CHAPAQ egress', color:'#ff3b5c' }, { key:'brain', name:'BRAIN', organ:'YACHAY cortex', fn:'read-only reasoning cortex · 5 regions + quantum mind · single tether, reads snapshots', color:'#7c5cff' }, { key:'nerve', name:'NERVOUS SYSTEM', organ:'OTel / VSP spans', fn:'efferent · afferent · proprioceptive · HUKLLA deadman reflex', color:'#5ad1ff' }, { key:'skeleton', name:'SKELETON', organ:'12 service repos', fn:'axial spine = doctrine+receipt chain · appendicular = capability bones', color:'#ffd166' } ]; /* ===================================================================== TWO BODIES — one circulatory + nervous mesh ===================================================================== */ const BODIES = [ { key:'a11oy', name:'a11oy', side:-1, color:'#3fe0c5', blurb:'governed-AI decision body — model routing, deny-by-default policy, human-on-the-loop actuation, signed-receipt Khipu DAG.' }, { key:'killinchu', name:'killinchu', side:1, color:'#ffb13f', blurb:'maritime / drone C2 body — track classification, ROE gate under human authority, detect·classify·defeat, DSSE receipt per interdiction, 3-of-4 BFT quorum.' } ]; /* The 12-bone axial spine + appendicular skeleton repos (skeleton legend) */ const SKELETON_REPOS = { axial: ['szl-yawar (receipt bus)', 'doctrine core (receipt chain)'], appendicular: ['szl-brain (YACHAY cortex+QM)','szl-overwatch (R0513)','szl-wires (YAWAR↔OTel)','szl-rimay (NL filter)','szl-sentra (egress)','szl-tupu-t7 (receipt-token)','szl-chakana (21-edge lattice)','szl-terra (BodyGraph)','szl-brand (assets)','szl-musquy (K-sim)'] }; /* ===================================================================== PUTNAM 2025 — honest doctrine-v11 kernel verdict (additive) Locked-8 {F1,F4,F7,F11,F12,F18,F19,F22} + Λ = Conjecture 1 are UNCHANGED by this block. Numbers match the CI kernel run on lutar-lean main exactly. ===================================================================== */ const PUTNAM_2025 = { competition:'86th William Lowell Putnam Mathematical Competition (Dec 6 2025)', source:'lutar-lean main', kernel_sha:'b7c3e382d56f6548945d93895c9d78c6411c40f8', kernel_sha_short:'b7c3e38', computed:'2026-06-09', doctrine:'v11', headline:'0 REAL / 11 DEMO / 1 OPEN', tally:{ REAL:0, DEMO:11, OPEN:1 }, labels:{ REAL:'Lean-kernel checked, no sorry, no extra axioms beyond declared', DEMO:'compiles but uses sorry/unproven lemmas', OPEN:'statement only' }, bridge:'We are not doing "drones solve Putnam." We are doing: Intelligence → Structure → Conjecture → Certificate. killinchu supplies intelligence (tracking, fusion, ROE decisions, signed receipts). We extract mathematical structure (graphs, constraints, optimization instances). We pose Putnam-grade + SZL-native problems. We ship certificates (Lean-verified REAL theorems, reproducible benchmarks, provenance).', problems:[ {id:'A1',file:'Lutar/Putnam/P_A1.lean',status:'DEMO',note:'formalized statement; proof uses sorry/unproven lemmas'}, {id:'A2',file:'Lutar/Putnam/P_A2.lean',status:'DEMO',note:'formalized statement; proof uses sorry/unproven lemmas'}, {id:'A3',file:'Lutar/Putnam/P_A3.lean',status:'OPEN',note:'statement only (True-shell); official answer withheld pending a real proof'}, {id:'A4',file:'Lutar/Putnam/P_A4.lean',status:'DEMO',note:'formalized statement; proof uses sorry/unproven lemmas'}, {id:'A5',file:'Lutar/Putnam/P_A5.lean',status:'DEMO',note:'formalized statement; proof uses sorry/unproven lemmas'}, {id:'A6',file:'Lutar/Putnam/P_A6.lean',status:'DEMO',note:'formalized statement; proof uses sorry/unproven lemmas'}, {id:'B1',file:'Lutar/Putnam/P_B1.lean',status:'DEMO',note:'formalized statement; proof uses sorry/unproven lemmas'}, {id:'B2',file:'Lutar/Putnam/P_B2.lean',status:'DEMO',note:'formalized statement; proof uses sorry/unproven lemmas'}, {id:'B3',file:'Lutar/Putnam/P_B3.lean',status:'DEMO',note:'formalized statement; proof uses sorry/unproven lemmas'}, {id:'B4',file:'Lutar/Putnam/P_B4.lean',status:'DEMO',note:'formalized statement; proof uses sorry/unproven lemmas'}, {id:'B5',file:'Lutar/Putnam/P_B5.lean',status:'DEMO',note:'formalized statement; proof uses sorry/unproven lemmas'}, {id:'B6',file:'Lutar/Putnam/P_B6.lean',status:'DEMO',note:'formalized statement; proof uses sorry/unproven lemmas'} ], szl_native:{ ids:['SZL-12A','SZL-12B'], status:'PENDING', note:'SZL-native originals — pending upstream kernel work; not yet on lutar-lean main' }, note:'A3 is OPEN (statement-only True-shell); the official 2025 A3 answer is intentionally withheld here until a REAL proof exists. No problem is currently REAL: each DEMO file formalizes the statement but discharges the proof with sorry or unproven lemmas.' }; /* ===================================================================== ============================ v5 QUANTUM-BIO LAYER ================= ADDITIVE. A self-contained, sovereign JS implementation of the FOUR tiny verified quantum-bio formulas (closed-form), mirroring the LIVE a11oy endpoints /api/a11oy/v1/qbio/{coherence,pmf,compass,lambda}. Labeled "verified model (mirrors a11oy /api/a11oy/v1/qbio)". 0 runtime CDN, 0 network: the math is embedded here so the layer is honest and self-contained even when the cross-origin endpoint is unreachable. HONESTY (doctrine v11) — never violated: • Lindblad coherence, Mitchell single-ion pmf, radical-pair compass, Becker/Nernst = [VERIFIED] (executed, peer-grounded physics). • Two-ion K⁺/H⁺ correction + Λ-v5 closure floor = [PROPOSED] SZL engineering constructs. Λ-v5 is an ENGINEERING gate, explicitly NOT the formal uniqueness Λ (which stays Conjecture 1, machine- checked FALSE unconditional). • Jack Kruse light/water/magnetism framing = [NARRATIVE] only. • Adds NO locked theorem — locked-proven stays exactly 8 {F1,F4,F7,F11,F12,F18,F19,F22}. Trust never 100%. ===================================================================== */ const QBIO = (function(){ 'use strict'; var R = 8.314, F = 96485.0, T = 310.0; /* 1. Lindblad / GKSL coherence decay (VERIFIED). C(t)=C0·e^(-t/τc). */ function coherenceAt(t, tau_c, C0){ tau_c = (tau_c==null) ? 6.05 : tau_c; C0 = (C0==null) ? 1.0 : C0; return C0 * Math.exp(-t / tau_c); } function coherenceSeries(tau_c, C0, tMax, n){ tau_c = (tau_c==null)?6.05:tau_c; C0=(C0==null)?1.0:C0; tMax = (tMax==null)?(tau_c*3):tMax; n=(n==null)?48:n; var out=[]; for(var i=0;i= lam_min (0.25), else RECHARGE/RE-TUNE. Mirrors the 3 Lean theorems: decohered (C=0) never closes; uncharged (charge=0) never closes; Λ monotone in coherence. */ function lambdaV5(C, charge){ return C * charge; } function closureGate(C, charge, lam_min){ lam_min=(lam_min==null)?0.25:lam_min; var v = lambdaV5(C, charge); return { value:v, lam_min:lam_min, execute:(v >= lam_min), verdict:(v >= lam_min ? 'EXECUTE' : 'RECHARGE / RE-TUNE') }; } /* canonical headline numbers (match a11oy /qbio/summary, verified) */ var CONST = { tau_c: 6.05, pmf_single_mV: 119.3, pmf_two_ion_mV: 121.5, // master payload §3/§10 headline (PROPOSED two-ion) compass_contrast_closed: 0.025, compass_contrast_full: 0.378, nernst_K_mV: -89.0, injury_current_uA: 70, lam_min: 0.25, lifecycle: '7 EXECUTE / 13 RECHARGE (balanced, self-regulating)' }; return { coherenceAt, coherenceSeries, pmf, pmfTwoIon, nernst, currentOfInjury, radicalPairYield, compassContrast, lambdaV5, closureGate, CONST, label:'verified model (mirrors a11oy /api/a11oy/v1/qbio)' }; })(); /* ---- Field leaders (VERIFIED load-bearing) + status doctrine ---- */ const QBIO_LEADERS = [ { name:'Peter Mitchell', work:'Chemiosmosis / proton-motive force (Nobel 1978)', status:'VERIFIED' }, { name:'Nick Lane', work:'Energy gradients precede genes (origin of life)', status:'VERIFIED' }, { name:'Douglas Wallace', work:'Bioenergetics ↔ mitochondrial genome', status:'VERIFIED' }, { name:'Klaus Schulten', work:'Radical-pair magnetoreception founder (cryptochrome)', status:'VERIFIED' }, { name:'Peter Hore', work:'Radical-pair spin dynamics (PNAS 2009)', status:'VERIFIED' }, { name:'Robert O. Becker', work:'DC current of injury → regeneration (classical)', status:'VERIFIED' }, { name:'Jack Kruse', work:'Light·Water·Magnetism framing (mitochondria as quantum engines)', status:'NARRATIVE' } ]; /* ---- Sources (arXiv / DOI / PMC) for the v5 layer ---- */ const QBIO_SOURCES = [ { label:'Mitchell pmf (Nobel)', url:'https://pmc.ncbi.nlm.nih.gov/articles/PMC2662253', status:'VERIFIED' }, { label:'Two-ion K⁺/H⁺ correction (Function zqac012)', url:'https://journals.physiology.org/doi/full/10.1093/function/zqac012', status:'PROPOSED' }, { label:'Lane — origin energy (arXiv:2104.08076)', url:'https://arxiv.org/abs/2104.08076', status:'VERIFIED' }, { label:'Wallace 2010 (PMC3245717)', url:'https://pmc.ncbi.nlm.nih.gov/articles/PMC3245717', status:'VERIFIED' }, { label:'Lindblad path integral (arXiv:2603.10839)', url:'https://arxiv.org/abs/2603.10839', status:'VERIFIED' }, { label:'Open quantum systems (arXiv:2202.05203)', url:'https://arxiv.org/abs/2202.05203', status:'VERIFIED' }, { label:'Radical pair (ora.ox.ac.uk uuid:d6b5f84e)', url:'https://ora.ox.ac.uk/', status:'VERIFIED' }, { label:'Schulten cryptochrome', url:'https://www.ks.uiuc.edu/Research/cryptochrome/', status:'VERIFIED' }, { label:'Hore PNAS 2009 (10.1073/pnas.0711968106)', url:'https://www.pnas.org/doi/10.1073/pnas.0711968106', status:'VERIFIED' }, { label:'Robert O. Becker (The Body Electric)', url:'https://en.wikipedia.org/wiki/Robert_O._Becker', status:'VERIFIED' }, { label:'AdS/CFT — holographic principle (Maldacena)', url:'https://en.wikipedia.org/wiki/Holographic_principle', status:'NARRATIVE' } ]; /* ---- 3 Lean closure theorems mirrored from the master payload §12 ---- */ const QBIO_THEOREMS = [ { id:'QB-T1', name:'Decohered never closes', status:'VERIFIED (Lean, no sorry)', lean:'theorem decohered_never_closes (h0:n.coherence=0)(hpos:lamMin>0): ¬ closureOk n lamMin', plain:'If coherence C=0 then lambdaV5 = 0 < lam_min, so the node can NEVER close — a fully decohered organ never executes.' }, { id:'QB-T2', name:'Uncharged never closes', status:'VERIFIED (Lean, no sorry)', lean:'theorem uncharged_never_closes (h0:n.charge=0)(hpos:lamMin>0): ¬ closureOk n lamMin', plain:'If charge=0 then lambdaV5 = 0 < lam_min, so an uncharged organ never executes — "no charge, no execute".' }, { id:'QB-T3', name:'Λ monotone in coherence', status:'VERIFIED (Lean, no sorry)', lean:'theorem lambda_mono_in_coherence (hq:q≥0)(h:c1≤c2): lambdaVal ⟨c1,q⟩ ≤ lambdaVal ⟨c2,q⟩', plain:'For charge q≥0, raising coherence never lowers lambdaV5 — the closure floor is monotone in coherence.' } ]; /* ===================================================================== PER-ORGAN v5 SEEDING (ADDITIVE — mutates each ORGAN object in place, adds new fields; NEVER removes/renames an existing field). Each value is COMPUTED from the verified formulas above using per-organ inputs derived deterministically from the organ index + name (so the same organ always shows the same physically-plausible state). The mV numbers are computed, not fabricated; the per-organ INPUTS are a labeled SAMPLE physiological assignment (organs have no measured pmf). ===================================================================== */ (function seedOrgansV5(){ // sample per-organ membrane inputs (labeled SAMPLE), within physiological ranges function hashStr(s){ var h=2166136261; for(var i=0;i>>0); } ORGANS.forEach(function(o, idx){ var hh = hashStr(o.key); // age along the coherence decay curve: 0..~2·τc (SAMPLE), deterministic per organ var age = ((hh % 1000)/1000) * (QBIO.CONST.tau_c * 1.6); var C = QBIO.coherenceAt(age, QBIO.CONST.tau_c, 1.0); // SAMPLE membrane inputs (physiological ranges): ΔΨ ~ 140..165 mV, // ΔpH ~ 0.28..0.61, ΔpK ~ 0.17..0.40 (deterministic per-organ, labeled SAMPLE) var d_psi = 140 + (hh % 26); // ~140..165 mV var d_pH = 0.28 + ((hh>>5) % 34)/100; // ~0.28..0.61 var d_pK = 0.17 + ((hh>>9) % 24)/100; // ~0.17..0.40 var dp_single = QBIO.pmf(d_psi, d_pH); // VERIFIED Mitchell var dp_two = QBIO.pmfTwoIon(d_psi, d_pH, d_pK); // PROPOSED two-ion var dp0 = QBIO.CONST.pmf_two_ion_mV; // reference Δp0 = 121.5 mV var charge = dp_two / dp0; // normalized charge ratio var gate = QBIO.closureGate(C, charge, QBIO.CONST.lam_min); o.qbio = { sample:true, // per-organ INPUTS are a labeled SAMPLE age_units: +age.toFixed(3), coherence: +C.toFixed(4), // C(age)=e^(-age/τc) [VERIFIED math] tau_c: QBIO.CONST.tau_c, d_psi_mV: d_psi, d_pH: +d_pH.toFixed(3), d_pK: +d_pK.toFixed(3), pmf_single_mV: +dp_single.toFixed(2), // [VERIFIED Mitchell] pmf_two_ion_mV: +dp_two.toFixed(2), // [PROPOSED two-ion K⁺/H⁺] charge: +charge.toFixed(4), // Δp_two / Δp0 lambdaV5: +gate.value.toFixed(4), // coherence · charge [PROPOSED gate] lam_min: QBIO.CONST.lam_min, execute: gate.execute, verdict: gate.verdict }; }); })(); /* ---- 5 v5 quantum-bio FORMULA CARDS (ADDITIVE to FORMULAS; honest tags). These are NOT locked theorems and are NEVER folded into the locked 8. maturity uses the existing MATURITY palette where it fits; the cards' plain text carries the explicit VERIFIED/PROPOSED/NARRATIVE status. ---- */ FORMULAS.QB_COH = { id:'QB-COH', name:'Lindblad Coherence Decay', maturity:'EXPERIMENTAL', latex:'C(t) = C0 \u00b7 e^(-t / tau_c) , tau_c \u2248 6.05', plain:'[VERIFIED math] Open-quantum-system (Lindblad/GKSL) coherence decays exponentially with time-constant \u03c4c\u22486.05. Steady state d\u03c1/dt=0 = proof of closure. This is a verified model mirroring a11oy /api/a11oy/v1/qbio/coherence \u2014 it adds NO locked theorem.', axioms:'verified model (mirrors a11oy /api/a11oy/v1/qbio/coherence) \u2014 not a Lean theorem', ref:'Lindblad path integral arXiv:2603.10839 \u00b7 open quantum systems arXiv:2202.05203' }; FORMULAS.QB_PMF = { id:'QB-PMF', name:'Mitchell Proton-Motive Force (+ two-ion)', maturity:'AXIOM_GATED', latex:'\u0394p = \u0394\u03a8 \u2212 (2.3 RT/F)\u00b7\u0394pH ; two-ion: 119.3 \u2192 121.5 mV', plain:'[VERIFIED] single-ion Mitchell pmf (chemiosmosis, Nobel). [PROPOSED] K\u207a/H\u207a two-ion correction (w\u22480.18) lifts 119.3\u2192121.5 mV. The bioenergetic "charge" of each organ = \u0394p/\u0394p0. Mirrors a11oy /api/a11oy/v1/qbio/pmf.', axioms:'verified model (mirrors a11oy /qbio/pmf); two-ion correction = PROPOSED SZL construct', ref:'Mitchell PMC2662253 \u00b7 two-ion Function zqac012 \u00b7 Wallace PMC3245717' }; FORMULAS.QB_COMPASS = { id:'QB-COMPASS', name:'Radical-Pair Magnetic Compass', maturity:'EXPERIMENTAL', latex:'\u03a6_S(\u03b8) angular singlet yield ; contrast \u2248 0.025 (closed) / 0.378 (full)', plain:'[VERIFIED math] Radical-pair spin dynamics give an angular singlet-yield contrast that biases execution direction (a magnetic compass). HONEST: the toy cos(\u03c9t) model FAILS (~0.003); single-nucleus closed form \u2248 0.025; only the full density-matrix model reaches \u2248 0.378. Mirrors a11oy /qbio/compass.', axioms:'verified model (mirrors a11oy /qbio/compass) \u2014 not a Lean theorem', ref:'Schulten cryptochrome (ks.uiuc.edu) \u00b7 Hore PNAS 2009 10.1073/pnas.0711968106' }; FORMULAS.QB_LAMBDA = { id:'QB-\u039bv5', name:'\u039b-v5 Closure Floor (engineering gate)', maturity:'CONJECTURE', latex:'lambdaV5 = coherence \u00b7 charge \u2265 lam_min (0.25) \u21d2 EXECUTE, else RECHARGE', plain:'[PROPOSED engineering gate] A node may execute iff it is coherent AND charged (lambdaV5 \u2265 0.25), else it RECHARGES / re-tunes. EXPLICITLY NOT the formal uniqueness \u039b \u2014 that stays Conjecture 1 (machine-checked FALSE unconditional). Mirrored by 3 Lean closure theorems (decohered/uncharged never close; \u039b monotone in coherence). Adds NO locked theorem; trust never 100%.', axioms:'PROPOSED engineering gate; Lean closure theorems QB-T1..T3 (no sorry); \u039b uniqueness = Conjecture 1 (FALSE)', ref:'master payload \u00a77/\u00a712 \u00b7 mirrors a11oy /api/a11oy/v1/qbio/lambda' }; FORMULAS.QB_BECKER = { id:'QB-BECKER', name:'Becker / Nernst Bioelectricity', maturity:'EXPERIMENTAL', latex:'E = (RT/zF) ln([ion]o/[ion]i) ; Nernst K\u207a = \u221289.0 mV ; I = V/R = 70 \u00b5A', plain:'[VERIFIED \u2014 classical electrophysiology] Nernst potential (K\u207a 5/140 mM = \u221289.0 mV) and Becker\u2019s DC "current of injury" (70 mV across 1 k\u03a9 = 70 \u00b5A) that directs growth/healing. The bioelectric drive behind the v5 layer; not a quantum claim.', axioms:'verified model (classical electrophysiology) \u2014 not a Lean theorem', ref:'Robert O. Becker, The Body Electric (1985) \u00b7 en.wikipedia.org/wiki/Robert_O._Becker' }; /* attach the 5 v5 cards to the relevant organs (ADDITIVE — push only) */ (function attachV5Cards(){ function pushUniq(o, ids){ if(!o) return; o.formulas = o.formulas || []; ids.forEach(function(id){ if(o.formulas.indexOf(id)<0) o.formulas.push(id); }); } var byKey={}; ORGANS.forEach(function(o){ byKey[o.key]=o; }); pushUniq(byKey['amaru'], ['QB_COH','QB_COMPASS']); // cortex / quantum mind pushUniq(byKey['yuyay'], ['QB_LAMBDA']); // Λ heart → Λ-v5 gate pushUniq(byKey['yawar'], ['QB_PMF']); // bioenergetic charge of the bus pushUniq(byKey['ruway'], ['QB_BECKER']); // write surface / bioelectric drive })(); root.SZL_ANATOMY = { KERNEL, MATURITY, FORMULAS, ORGANS, SYSTEMS, BODIES, SKELETON_REPOS, PUTNAM_2025, QBIO, QBIO_LEADERS, QBIO_SOURCES, QBIO_THEOREMS }; })(window);