instill Wave23 conditional Khipu BFT safety (Conjecture 2 conditional) into doctrine panel + B2 node

data.js

@@ -21,8 +21,9 @@
     toolchain: 'Lean v4.13.0 (locked) / v4.18.0 (Mathlib pinned) · main @ 044eb098',
     locked_proven: ['F1', 'F11', 'F12', 'F18', 'F19'],
     experimental_count_approx: 119,  // waves 5–18 instilled card set (EXPERIMENTAL · CI-green, never folded into locked 5)
-    waves_merged: 'Wave5–18 (CF-1..28 + CUT-1 fwd + CUT-2)',  // Wave15 CF-22, Wave16 CF-24/25/26, Wave17 CF-23/27/28, Wave18 CUT-1 forward fragment
+    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: 'Build L1 honest · L2 roadmap (not claimed as earned)'
   };
 
@@ -83,6 +84,11 @@
       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.',