Spaces:
Running
Running
| import{r as u,k as t}from"./index-BVfpSx5Q.js";import{L as S}from"./layout-NiehYZnq.js";import{P as $,C as p,S as b}from"./ui-DGkmnhL-.js";import{a as d,S as V}from"./cookbookContent-DI9NJhNa.js";function E(e){if(!(e.empiricalRisk>=0&&e.empiricalRisk<=1))throw new Error(`empiricalRisk must be in [0, 1], got ${e.empiricalRisk}`);if(!(e.klDivergence>=0))throw new Error(`klDivergence must be ≥ 0, got ${e.klDivergence}`);if(!Number.isInteger(e.sampleSize)||e.sampleSize<1)throw new Error(`sampleSize must be a positive integer, got ${e.sampleSize}`);if(!(e.delta>0&&e.delta<1))throw new Error(`delta must be in (0, 1), got ${e.delta}`)}function R(e){E(e);const{empiricalRisk:o,klDivergence:s,sampleSize:r,delta:a}=e,n=s+Math.log(2*Math.sqrt(r)/a),c=Math.sqrt(n/(2*r)),i=o+c;return{slack:c,upperBound:i,nonVacuous:i<1}}function y(e){let o=3421674724,s=2216829733;for(let a=0;a<e.length;a++){const n=e.charCodeAt(a);s^=n;const c=s*435+o*0,i=o*435+s*16777216;s=c>>>0,o=i+(Math.floor(s/4294967296)|0)>>>0,s=s>>>0}return((o>>>0).toString(16).padStart(8,"0")+(s>>>0).toString(16).padStart(8,"0")).repeat(4).slice(0,64)}function C(e,o,s){if(!Number.isInteger(o)||o<0)throw new Error(`buildDecision: value must be non-negative integer, got ${o}`);const r=JSON.stringify({decisionId:e,value:o,payload:null});return{kind:"decision",decisionId:e,value:o,hash:y(r),payload:s}}function H(e,o){const s=o.reduce((n,c)=>n+c.value,0),r=[...o.map(n=>n.hash)].sort(),a=y(`${e}|${r.join(",")}|${s}`);return{kind:"organ",organId:e,decisions:o,pendantValue:s,pendantHash:a}}function T(e,o,s){const r=o.reduce((c,i)=>c+i.pendantValue,0),a=[...o.map(c=>c.pendantHash)].sort(),n=y(`${e}|${a.join(",")}|${r}`);return{kind:"root",receiptId:e,organs:o,rootValue:r,rootHash:n,dualAttestation:s}}function k(e){for(const s of e.organs){const r=s.decisions.reduce((a,n)=>a+n.value,0);if(r!==s.pendantValue)return{ok:!1,reason:`organ "${s.organId}" pendantValue mismatch: stored=${s.pendantValue}, computed=${r}`}}const o=e.organs.reduce((s,r)=>s+r.pendantValue,0);return o!==e.rootValue?{ok:!1,reason:`root "${e.receiptId}" rootValue mismatch: stored=${e.rootValue}, computed=${o}`}:{ok:!0}}function A(e){const o=[...e.organs.map(s=>`${s.organId}:${s.decisions.length}`)].sort().join(";");return y(`knot|${o}|${e.rootValue}`).slice(0,16)}function B(e,o=0,s=1){const r=e.organs.map((a,n)=>n===o?{...a,pendantValue:a.pendantValue+s}:a);return{...e,organs:r}}function w(){const e=["a11oy","sentra","amaru"].map((o,s)=>H(o,Array.from({length:5},(r,a)=>C(`${o}-d${a}`,(s+1)*100+a*7))));return T("demo-root",e)}function M(){const[e,o]=u.useState(d.pacBayesWorkedExample.sampleSize),[s,r]=u.useState(d.pacBayesWorkedExample.klDivergence),[a,n]=u.useState(d.pacBayesWorkedExample.delta),[c,i]=u.useState(d.pacBayesWorkedExample.empiricalRisk),h=u.useMemo(()=>{try{return R({empiricalRisk:c,klDivergence:s,sampleSize:e,delta:a})}catch(l){return{slack:NaN,upperBound:NaN,nonVacuous:!1,error:String(l)}}},[e,s,a,c]),m=u.useMemo(()=>w(),[]),f=u.useMemo(()=>B(m,0,1),[m]),g=k(m),x=k(f),j=A(m),v=l=>Number.isFinite(l)?l.toFixed(6):"—";return t.jsxs(S,{children:[t.jsx($,{label:"COOKBOOK · knot-calculus-v1",title:"Knot Calculus — PAC-Bayes + Khipu TH11 (live)",subtitle:`Sealed ${d.sealed}. ${d.frame}.`,status:"LIVE"}),t.jsxs(p,{children:[t.jsx("div",{className:"text-xs font-semibold mb-1",style:{color:"#c9b787"},children:"σ-ALGEBRA HONESTY NOTE"}),t.jsx("p",{className:"text-xs",style:{color:"var(--color-a11oy-text-sub)",lineHeight:1.7},children:V})]}),t.jsxs("div",{className:"grid lg:grid-cols-2 gap-6 my-8",children:[t.jsxs(p,{children:[t.jsx(b,{children:"McAllester-1999 PAC-Bayes bound (TH13)"}),t.jsx("p",{className:"text-xs mb-4",style:{color:"var(--color-a11oy-text-ghost)",lineHeight:1.6},children:"R(Q) ≤ R̂(Q) + √( ( KL(Q‖P) + ln(2√n / δ) ) / (2n) ), with probability ≥ 1−δ. Code ported verbatim from knot-calculus-v1/code/src/pac-bayes-bound.ts."}),[{label:"n (samples)",value:e,set:l=>o(Math.max(1,Math.round(l))),step:1e3},{label:"KL(Q‖P) nats",value:s,set:r,step:.1},{label:"δ confidence",value:a,set:n,step:.01},{label:"R̂ empirical risk",value:c,set:i,step:.01}].map(l=>t.jsxs("label",{className:"block mb-3",children:[t.jsx("span",{className:"text-xs",style:{color:"var(--color-a11oy-text-sub)"},children:l.label}),t.jsx("input",{type:"number",value:l.value,step:l.step,onChange:N=>l.set(parseFloat(N.target.value)),className:"w-full mt-1 px-2 py-1 text-sm rounded",style:{background:"rgba(255,255,255,0.04)",color:"var(--color-a11oy-text)",border:"1px solid rgba(255,255,255,0.1)"}})]},l.label)),t.jsxs("div",{className:"mt-4 p-3 rounded",style:{background:"rgba(201,183,135,0.08)"},children:[t.jsxs("div",{className:"text-xs",style:{color:"var(--color-a11oy-text-sub)"},children:["slack = ",v(h.slack)]}),t.jsxs("div",{className:"text-sm font-semibold",style:{color:"var(--color-a11oy-text)"},children:["upper bound R(Q) ≤ ",v(h.upperBound)]}),t.jsx("div",{className:"text-xs mt-1",style:{color:h.nonVacuous?"#5fb878":"#d9737a"},children:h.nonVacuous?"NON-VACUOUS (bound < 1)":"VACUOUS (bound ≥ 1)"})]})]}),t.jsxs(p,{children:[t.jsx(b,{children:"TH11 Khipu summation-invariant verifier"}),t.jsx("p",{className:"text-xs mb-4",style:{color:"var(--color-a11oy-text-ghost)",lineHeight:1.6},children:"3-organ × 5-decision Khipu root. The runtime verifier is the counterpart to Lean TH11 khipuReceipt_checksum_invariant (two routine sorries)."}),t.jsxs("div",{className:"mb-3 p-3 rounded",style:{background:"rgba(255,255,255,0.03)"},children:[t.jsxs("div",{className:"text-xs",style:{color:"var(--color-a11oy-text-sub)"},children:["rootValue = ",m.rootValue]}),t.jsxs("div",{className:"text-xs font-mono break-all",style:{color:"var(--color-a11oy-text-ghost)"},children:["16-hex knot-invariant tag: ",j]})]}),t.jsxs("div",{className:"mb-2 text-sm",style:{color:g.ok?"#5fb878":"#d9737a"},children:["✓ Valid root → TH11 ",g.ok?"PASS":"FAIL"]}),t.jsxs("div",{className:"text-sm",style:{color:x.ok?"#d9737a":"#5fb878"},children:["✓ Tampered pendant (+1) → TH11 correctly ",x.ok?"ACCEPTED (BUG!)":"REJECTED"]}),!x.ok&&t.jsxs("div",{className:"text-[11px] mt-1 font-mono",style:{color:"var(--color-a11oy-text-ghost)"},children:["reason: ",x.reason]})]})]}),t.jsx(b,{children:"Lean obligations referenced"}),t.jsx(p,{children:t.jsxs("table",{className:"w-full text-xs",children:[t.jsx("thead",{children:t.jsxs("tr",{style:{color:"var(--color-a11oy-text-ghost)"},children:[t.jsx("th",{className:"text-left py-1",children:"Theorem"}),t.jsx("th",{className:"text-left py-1",children:"File"}),t.jsx("th",{className:"text-left py-1",children:"Status (honest)"})]})}),t.jsx("tbody",{children:d.leanObligations.map(l=>t.jsxs("tr",{style:{borderTop:"1px solid rgba(255,255,255,0.05)"},children:[t.jsx("td",{className:"py-1 pr-2",style:{color:"var(--color-a11oy-text)"},children:l.theorem}),t.jsx("td",{className:"py-1 pr-2 font-mono",style:{color:"var(--color-a11oy-text-sub)"},children:l.file}),t.jsx("td",{className:"py-1",style:{color:"#c9b787"},children:l.status})]},l.theorem))})]})}),t.jsx(b,{children:"Citations"}),t.jsx(p,{children:t.jsx("ul",{className:"text-xs space-y-1",style:{color:"var(--color-a11oy-text-sub)"},children:d.citations.map(l=>t.jsxs("li",{children:["• ",l]},l))})})]})}export{M as CookbookKnotCalculus}; | |