cp500's picture
paper links open the static host in a new tab
02b1236 verified
Raw History Blame Contribute Delete
45.4 kB
<!doctype html>
<html lang="en"><head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width,initial-scale=1">
<title>The Deterministic Reasoning Space</title>
<style>
:root{--bg:#fcfcf9;--ink:#1c1c1a;--mut:#6b6b64;--line:#ddddd2;--acc:#0e7272;
--accbg:#e8f3f2;--warn:#a05a16;--neg:#8c2f39}
*{box-sizing:border-box}
html{scroll-behavior:smooth}
body{margin:0;background:var(--bg);color:var(--ink);
font:17px/1.62 Charter,"Bitstream Charter",Cambria,Georgia,serif}
.col{max-width:760px;margin:0 auto;padding:0 22px}
h1{font-size:30px;line-height:1.25;margin:26px 0 4px;text-align:center}
.subtitle{text-align:center;font-size:21px;margin:0 0 14px}
h2{font-size:22px;margin:48px 0 10px}
h2 .no{display:inline-block;background:var(--acc);color:#fff;border-radius:50%;
width:26px;height:26px;line-height:26px;text-align:center;font-size:14px;
margin-right:10px;vertical-align:2px}
h5{margin:0 0 6px;font-size:12px;letter-spacing:.08em;color:var(--mut)}
p{margin:10px 0}
a{color:var(--acc)}
code,.mono{font:14px "SF Mono",Menlo,monospace}
section{padding:12px 0 26px}
.caption{font-size:14.5px;color:var(--mut)}
.hint{font-size:14px;color:var(--mut)}
button{font:15px Charter,Georgia,serif;background:#fff;border:1.5px solid var(--ink);
border-radius:5px;padding:9px 16px;cursor:pointer}
button:hover{background:var(--accbg)}
button:disabled{opacity:.45;cursor:default}
button.ghost{border-color:var(--line);color:var(--mut);font-size:13.5px;padding:6px 10px}
select{font:15px Charter,serif;padding:6px;border:1px solid var(--line);border-radius:4px;background:#fff}
.pill{display:inline-block;font:11px "SF Mono",Menlo,monospace;padding:1px 7px;border-radius:9px}
.pill.exact{background:#e3efe3;color:#1d5c1d}
.pill.inferred{background:#f6e4ef;color:#8c2f6e}
.pill.warn{background:#f6ecd9;color:var(--warn)}
.pill.neg{background:#f3e0e2;color:var(--neg)}
hr.rule{border:0;border-top:1px solid var(--line);margin:26px 0}
/* stepper */
#stepbar{position:sticky;top:0;background:rgba(252,252,249,.96);z-index:50;
border-bottom:1px solid var(--line);backdrop-filter:blur(3px)}
#steps{max-width:860px;margin:0 auto;display:flex;padding:10px 20px 8px}
.step{flex:1;text-align:center;cursor:pointer;position:relative;font-size:12.5px;color:var(--mut)}
.step .dot{width:22px;height:22px;line-height:22px;border-radius:50%;margin:0 auto 3px;
border:1.5px solid var(--line);background:#fff;font-size:12px}
.step.on .dot{background:var(--acc);border-color:var(--acc);color:#fff}
.step.on{color:var(--ink);font-weight:bold}
.step::before{content:'';position:absolute;top:11px;left:-50%;width:100%;height:2px;background:var(--line);z-index:-1}
.step:first-child::before{display:none}
/* panels */
.panel{border:1px solid var(--line);border-radius:6px;padding:14px 16px;margin:12px 0;background:#fff}
.duo{display:grid;grid-template-columns:1fr 1fr;gap:14px}
@media(max-width:640px){.duo{grid-template-columns:1fr}}
.counter{font:28px "SF Mono",Menlo,monospace;color:var(--neg)}
.ctx{height:12px;border:1px solid var(--line);border-radius:6px;overflow:hidden;margin:6px 0}
.ctx>div{height:100%;background:var(--neg);width:0%}
/* incidence matrix */
table.inc{border-collapse:collapse;font:12px "SF Mono",Menlo,monospace;margin:8px 0}
table.inc th{font-weight:normal;text-align:right;padding:1px 8px 1px 2px;color:var(--mut);white-space:nowrap}
table.inc td{width:17px;height:17px;border:1px solid #eceade;text-align:center;padding:0}
table.inc td.b1{background:var(--acc)}
table.inc td.hl{outline:2px solid var(--warn);outline-offset:-2px}
table.inc td.den{background:var(--neg)}
.chips{display:flex;gap:8px;flex-wrap:wrap;margin:10px 0}
.chip{border:1.5px solid var(--line);border-radius:16px;padding:4px 13px;cursor:pointer;font-size:14.5px;background:#fff}
.chip.on{background:var(--acc);color:#fff;border-color:var(--acc)}
.chip.not{background:var(--neg);color:#fff;border-color:var(--neg);text-decoration:line-through}
.bits{display:flex;gap:2px;margin:4px 0;flex-wrap:wrap}
#bitanim .bits{flex-wrap:nowrap}
#bitanim .bits i{width:11px;height:11px}
.bits i{display:block;width:14px;height:14px;border-radius:2px;background:#ebe9df}
.bits i.s{background:var(--acc)}
.bits i.r{background:var(--neg)}
.ans{font-size:26px;font-weight:bold}
/* interval widget */
.ival{position:relative;height:34px;border:1px solid var(--line);border-radius:5px;background:#fff;margin:8px 0}
.ival .bel{position:absolute;top:0;bottom:0;background:var(--acc);opacity:.85}
.ival .ign{position:absolute;top:0;bottom:0;background:#d9d5c6}
.ival .den{position:absolute;top:0;bottom:0;background:var(--neg);opacity:.75}
.sliders label{display:flex;align-items:center;gap:10px;font-size:14.5px;margin:4px 0}
.sliders input{flex:1}
/* trace rows */
.tr{border-left:3px solid var(--line);padding:8px 12px;margin:10px 0;background:#fff;border-radius:0 5px 5px 0}
.tr.plan{border-color:#8c2f6e}.tr.step{border-color:var(--acc)}.tr.ans{border-color:#1d5c1d}
.canned{display:flex;gap:8px;flex-wrap:wrap;margin:8px 0}
footer{border-top:1px solid var(--line);margin-top:40px;padding:18px 0 30px;
font-size:13.5px;color:var(--mut);text-align:center}
.ok{color:#1d5c1d}.bad{color:var(--neg)}
video{width:100%;border-radius:6px;border:1px solid var(--line)}
.pbar{height:5px;background:#ece9dd;border-radius:3px;overflow:hidden}
.pbar>div{height:100%;background:var(--acc);width:0%}
.sx{background:#f4f3ec;border:1px solid var(--line);border-radius:5px;padding:8px 12px;
font:13.5px "SF Mono",Menlo,monospace;overflow-x:auto}
</style></head><body>
<div id="stepbar"><div id="steps"></div></div>
<div class="col">
<h1>The Deterministic Reasoning Space</h1>
<p class="subtitle">casting hypergraphs onto bitmap &sigma;-algebras</p>
<p class="caption" style="text-align:center">An interactive companion to the paper
(<a href="https://cp500-deterministic-reasoning-space.static.hf.space/assets/paper.pdf" target="_blank" rel="noopener">PDF</a>). Everything on this page runs in your browser:
the ledger, the queries, the planner, the proofs. Nothing is sent anywhere.</p>
<video controls preload="metadata" src="assets/intro.mp4" poster=""></video>
<p class="caption" style="text-align:center">The two-minute version. The page below is the same story, made touchable.</p>
</div>
<!-- ============ 1 ============ -->
<section id="c1"><div class="col">
<h2><span class="no">1</span>Maya's question</h2>
<p>Maya asks her new AI agent one simple question: <i>find me the suppliers that are
a risk to me.</i> The agent knows nothing about the database, so it explores:
suppliers, then items, then countries of origin, then risk data. Every hop multiplies
the join paths. The context window fills. The agent has quietly become a query
planner &mdash; and a bad one.</p>
<div class="duo">
<div class="panel"><h5>THE EXPLORING AGENT</h5>
<svg id="hairball" viewBox="0 0 320 190" style="width:100%;display:block"></svg>
<div style="display:flex;gap:14px;align-items:baseline">
<div><span class="hint">join paths</span><div class="counter" id="joins">1</div></div>
<div style="flex:1"><span class="hint">context window</span>
<div class="ctx"><div id="ctxfill"></div></div>
<div class="hint mono" id="hopmsg" style="font-size:12px">hop 0: reading the schema&hellip;</div></div></div>
<button class="ghost" id="replay">replay</button></div>
<div class="panel"><h5>THE SAME QUESTION OVER BIT COLUMNS</h5>
<div class="mono" style="margin:4px 0 8px">(and rel/supplies country-flagged) &rarr; popcount</div>
<div id="bitanim"></div>
<div style="display:flex;gap:14px;align-items:baseline;margin-top:4px">
<div><span class="hint">operations</span><div class="counter" style="color:var(--acc)" id="opcount">0</div></div>
<div class="hint" id="bitmsg" style="flex:1"></div></div>
<button class="ghost" id="replay2">replay</button></div>
</div>
<p class="caption"><b>Panel 1:</b> left is a simulation of pointer-chasing on an unknown
schema (four relations, branching factor shown live). Right is this paper's answer. The
rest of the page builds it.</p>
</div></section>
<!-- ============ 2 ============ -->
<section id="c2"><div class="col">
<h2><span class="no">2</span>The cast: one fact, one row, flat columns</h2>
<p>The ledger below is a tiny supply chain: who supplies what from where, which
countries carry risk flags, who is suspended, and a materials chain for a recall.
One fact &mdash; <i>Acme supplies cells to Osaka from Japan</i> &mdash; is one
<b>hyperedge</b>: a single row set across role-marked bit columns
(<code>rel/supplies/+/acme</code> is a different column from
<code>rel/supplies/-/acme</code>, so direction is stored, not inferred). A source
that <b>denies</b> a claim writes a row too: disagreement is data, never an overwrite.</p>
<p>Click any observation to light its row across the columns. The hypergraph is never
stored as a shape &mdash; it <b>is</b> this incidence matrix.</p>
<div class="panel" style="overflow-x:auto">
<div class="chips" id="obschips"></div>
<div id="matrix"></div>
</div>
<p class="caption"><b>Panel 2:</b> 18 observations, one column per vocabulary term.
Teal = set bit, red = a denial's polarity bit. Rows are hyperedges; columns are the
terms; reading either way is the same matrix (the dual views of the paper, &sect;2).</p>
</div></section>
<!-- ============ 3 ============ -->
<section id="c3"><div class="col">
<h2><span class="no">3</span>Queries are arithmetic</h2>
<p>Because every term is a bit column, the three &sigma;-algebra axioms are machine
instructions: the empty set is the all-zeros vector, complement is <code>NOT</code>,
union is <code>OR</code> &mdash; and intersection follows by De Morgan. Build a query
by clicking facts (click twice for <code>NOT</code>). The answer is computed by
<code>AND</code> over whole columns and counted by a popcount. No model runs at
answer time.</p>
<div class="panel">
<div class="chips" id="qchips"></div>
<div id="qbits"></div>
<div><span class="ans" id="qcount">0</span> <span class="pill exact">EXACT</span>
<span class="hint" id="qdesc"></span></div>
<div class="hint" id="qrows" style="margin-top:6px"></div>
</div>
<p><b>And it is fast.</b> The number from the talk track &mdash; two one-million-row
columns intersected and counted in a fraction of a millisecond &mdash; is not our
hardware's number. Measure it on yours:</p>
<div class="panel">
<button id="benchgo">Benchmark my machine: AND + popcount over 1,000,000 rows</button>
<div id="benchout" class="mono" style="margin-top:8px"></div>
</div>
</div></section>
<!-- ============ 4 ============ -->
<section id="c4"><div class="col">
<h2><span class="no">4</span>S-paths: an exact recall, not a random walk</h2>
<p>A defective resin lot <code>lot-L7</code> is recalled. Which shipments are exposed?
Keep a mask of everything reached so far and grow it one relation-step at a time:
<code>F<sub>t+1</sub> = F<sub>t</sub> OR N(F<sub>t</sub>)</code>. After <i>t</i>
steps the frontier is the <b>complete</b> set of things reachable in &le; <i>t</i>
steps &mdash; not a sample, not an estimate. Anything outside it is provably
unaffected at that depth.</p>
<div class="panel">
<button id="spathgo">Run the recall from lot-L7</button>
<div id="spathviz" style="margin-top:10px"></div>
</div>
<p class="caption"><b>Panel 4:</b> each row is one frontier mask over the entities;
each step is one fixed sequence of <code>AND</code>/<code>OR</code> over the
<code>rel/consumes</code> columns.</p>
</div></section>
<!-- ============ 5 ============ -->
<section id="c5"><div class="col">
<h2><span class="no">5</span>Denied is not silent</h2>
<p>To a single yes/no bit, <i>never mentioned</i> and <i>actively denied</i> look
identical: both are 0. They mean very different things. Because assert and deny are
separate columns, every claim gets two counts and so an interval:
<b>belief</b> (the fraction of evidence supporting it) to <b>plausibility</b> (one
minus the fraction denying it). The gap between them is exactly the silence.
Move the sliders.</p>
<div class="panel">
<div class="sliders">
<label>assert <input type="range" id="sA" min="0" max="10" value="1"> <span class="mono" id="vA">1</span></label>
<label>deny &nbsp;&nbsp;<input type="range" id="sD" min="0" max="10" value="0"> <span class="mono" id="vD">0</span></label>
<label class="hint">silent = the rest of 10 sources</label>
</div>
<div class="ival" id="ival"></div>
<div class="mono" id="ivaltxt"></div>
<div class="canned">
<button class="ghost" id="pre1">1 assert, 9 silent</button>
<button class="ghost" id="pre2">1 assert, 1 deny, 8 silent</button>
<button class="ghost" id="pre3">5 assert, 5 deny: pure conflict</button>
</div>
<div class="hint" id="ivalread"></div>
</div>
<p class="caption"><b>Panel 5:</b> teal = belief, grey = ignorance (silence),
red = denied mass. The first two presets are indistinguishable to a single bit;
the interval separates them, and conflict (narrow but central) stays visible instead
of averaging away. In our tiny ledger this is live: Japan's risk flag is asserted by
a news wire and denied by an auditor &mdash; contested, not 50&nbsp;percent.</p>
</div></section>
<!-- ============ 6 ============ -->
<section id="c6"><div class="col">
<h2><span class="no">6</span>The fixed point: one answer, any order</h2>
<p>Answering is narrowing: start from everything, apply one constraint per pass.
On the drill-down ultrametric every productive pass at least halves the distance to
the answer, so the Banach fixed point theorem guarantees a unique fixed point,
reached from any starting order. Shuffle Maya's constraints and watch every order
land on the identical mask.</p>
<div class="panel">
<button id="fixgo">Narrow</button>
<button class="ghost" id="fixshuffle">shuffle the constraint order</button>
<div id="fixviz" style="margin-top:10px"></div>
</div>
<p class="caption"><b>Panel 6:</b> if the constraints are jointly unsatisfiable the
process ends at the all-zeros mask &mdash; a definite <i>no such observation</i>,
reported as such. There is no state in the space that corresponds to an invented
fact.</p>
</div></section>
<!-- ============ 7 ============ -->
<section id="c7"><div class="col">
<h2><span class="no">7</span>Ask like Maya: a 121M planner, typed calls only</h2>
<p>The agent never writes a query. <b>Cactus Needle 3</b> (121M parameters, running
in this tab under WebAssembly) reads the question and emits a <b>typed tool
call</b> against a closed schema &mdash; the Jev contract: messy intent in, a typed
decision out, never free text. The call is type-checked against the vocabulary
before a single bit is read; a malformed or invented query cannot exist. Then the
engine answers it by the arithmetic of section 3.</p>
<div class="panel">
<div style="display:flex;gap:8px"><input id="q" style="flex:1;font:15px Charter,serif;padding:9px;border:1px solid var(--line);border-radius:5px"
placeholder="Ask about the supply chain&hellip;"><button id="askgo">Ask</button></div>
<div class="canned" id="canned"></div>
<div id="plannerboot" class="hint"></div>
<div class="pbar" id="pwrap" style="display:none"><div id="pfill"></div></div>
<div id="trace"></div>
</div>
<p class="caption"><b>Panel 7:</b> the walkthrough. The planner proposes; the type
checker disposes; set arithmetic answers. Try the strict variant: requiring risk to
be <i>asserted and not denied</i> changes the answer, because Japan's flag is
contested &mdash; polarity is part of the question.</p>
</div></section>
<!-- ============ 8 ============ -->
<section id="c8"><div class="col">
<h2><span class="no">8</span>Verify it yourself</h2>
<p>The paper's claims are properties, so they are testable. The button below runs the
property suite in your browser: the three &sigma;-algebra axioms and De Morgan on
random masks and on this page's ledger, bit-exact agreement with set semantics,
measure additivity, the four metric axioms of the belief&ndash;plausibility distance,
the ultrametric strong triangle, and the one-half contraction per filtration descent.
The same suite, in Python, ships with the paper
(<a href="https://cp500-deterministic-reasoning-space.static.hf.space/assets/test_properties.py" target="_blank" rel="noopener">test_properties.py</a>).</p>
<div class="panel">
<button id="proofgo">Run the property suite (2,000 trials each)</button>
<div id="proofout" class="mono" style="margin-top:8px"></div>
</div>
</div></section>
<footer>
&copy; 2026 &middot; companion to <i>The Deterministic Reasoning Space: Casting
Hypergraphs onto Bitmap &sigma;-Algebras</i> &middot;
<a href="https://cp500-deterministic-reasoning-space.static.hf.space/assets/paper.pdf" target="_blank" rel="noopener">paper</a> &middot;
<a href="https://cp500-deterministic-reasoning-space.static.hf.space/assets/test_properties.py" target="_blank" rel="noopener">property tests</a> &middot;
planner: Cactus Needle 3 (on-device) &middot; all data on this page is synthetic
</footer>
<script src="assets/planner.js"></script>
<script>
const $=id=>document.getElementById(id);
/* ============ stepper ============ */
const CHAPTERS=[["c1","Question"],["c2","Cast"],["c3","Algebra"],["c4","S-paths"],["c5","Evidence"],["c6","Fixed point"],["c7","Ask"],["c8","Verify"]];
$('steps').innerHTML=CHAPTERS.map(([id,t],i)=>
`<div class="step" data-i="${i}"><div class="dot">${i+1}</div>${t}</div>`).join('');
document.querySelectorAll('.step').forEach(s=>s.onclick=()=>
document.getElementById(CHAPTERS[+s.dataset.i][0]).scrollIntoView({behavior:'smooth'}));
addEventListener('scroll',()=>{let on=0;
CHAPTERS.forEach(([id],i)=>{const r=document.getElementById(id).getBoundingClientRect();
if(r.top<innerHeight*0.4)on=i;});
document.querySelectorAll('.step').forEach((s,i)=>s.classList.toggle('on',i===on));});
/* ============ the tiny supply-chain ledger ============ */
/* one observation = one role-marked atom <<R | a+, b-; i>> plus context terms */
const LEDGER=[
{rel:'supplies',a:'acme',b:'osaka',item:'cells', country:'jp',pol:+1,src:'erp', label:'acme ships cells to osaka (from jp)'},
{rel:'supplies',a:'acme',b:'perth',item:'cells', country:'jp',pol:+1,src:'erp', label:'acme ships cells to perth (from jp)'},
{rel:'supplies',a:'borealis',b:'osaka',item:'casing',country:'au',pol:+1,src:'erp',label:'borealis ships casing to osaka (from au)'},
{rel:'supplies',a:'cedar',b:'perth',item:'resin', country:'cl',pol:+1,src:'erp', label:'cedar ships resin to perth (from cl)'},
{rel:'supplies',a:'dune',b:'osaka',item:'resin', country:'au',pol:+1,src:'erp', label:'dune ships resin to osaka (from au)'},
{rel:'risk-flag',a:'jp',pol:+1,src:'news-wire', label:'news wire FLAGS japan'},
{rel:'risk-flag',a:'jp',pol:-1,src:'auditor', label:'auditor DENIES the japan flag'},
{rel:'risk-flag',a:'cl',pol:+1,src:'news-wire', label:'news wire FLAGS chile'},
{rel:'risk-flag',a:'cl',pol:+1,src:'insurer', label:'insurer FLAGS chile'},
{rel:'suspended',a:'cedar',pol:+1,src:'compliance',label:'compliance SUSPENDS cedar'},
{rel:'suspended',a:'acme',pol:-1,src:'compliance', label:'compliance clears acme (denial)'},
{rel:'consumes',a:'batch-b2',b:'lot-l7',pol:+1,src:'mes',label:'batch-b2 consumed lot-l7'},
{rel:'consumes',a:'batch-b3',b:'lot-l7',pol:+1,src:'mes',label:'batch-b3 consumed lot-l7'},
{rel:'consumes',a:'assembly-a1',b:'batch-b2',pol:+1,src:'mes',label:'assembly-a1 used batch-b2'},
{rel:'consumes',a:'assembly-a2',b:'batch-b3',pol:+1,src:'mes',label:'assembly-a2 used batch-b3'},
{rel:'consumes',a:'shipment-s9',b:'assembly-a1',pol:+1,src:'mes',label:'shipment-s9 carries assembly-a1'},
{rel:'supplies',a:'cedar',b:'osaka',item:'resin',country:'cl',pol:+1,src:'erp',label:'cedar ships resin to osaka (from cl)'},
{rel:'risk-flag',a:'au',pol:-1,src:'auditor', label:'auditor DENIES any australia flag'},
];
const N=LEDGER.length;
/* the cast: project every component onto its own column */
const COLS={};
function setbit(name,i){(COLS[name]=COLS[name]||new Array(N).fill(0))[i]=1;}
LEDGER.forEach((o,i)=>{
setbit('ent/'+o.a,i); if(o.b)setbit('ent/'+o.b,i);
setbit('rel/'+o.rel+'/+/'+o.a,i); if(o.b)setbit('rel/'+o.rel+'/-/'+o.b,i);
if(o.item)setbit('item/'+o.item,i);
if(o.country)setbit('country/'+o.country,i);
setbit(o.pol>0?'state/asserted':'state/denied',i);
setbit('src/'+o.src,i);
setbit('rel/'+o.rel,i);
});
const COLNAMES=Object.keys(COLS).sort();
const AND=(x,y)=>x.map((v,i)=>v&y[i]), OR=(x,y)=>x.map((v,i)=>v|y[i]),
NOT=x=>x.map(v=>1-v), POP=x=>x.reduce((s,v)=>s+v,0),
ZERO=new Array(N).fill(0), col=n=>COLS[n]||ZERO;
/* ============ section 1: join explosion (animated hairball) ============ */
function explode(){
const svg=$('hairball');svg.innerHTML='';
let nodes=[{x:160,y:95}],joins=1,hop=0;
const msgs=['reading the schema…','joining suppliers ⋈ items…',
'joining ⋈ countries…','joining ⋈ risk feeds…','re-planning; retrying joins…'];
clearInterval(explode.t);
svg.innerHTML='<circle cx="160" cy="95" r="4" fill="#8c2f39"/>';
$('joins').textContent='1';$('ctxfill').style.width='0%';
$('hopmsg').textContent='hop 0: reading the schema…';
explode.t=setInterval(()=>{
hop++;joins*=7+Math.floor(Math.random()*6);
const next=[];
nodes.forEach(n=>{
const k=nodes.length>60?1:3;
for(let c=0;c<k;c++){
const ang=Math.random()*Math.PI*2,r=18+Math.random()*26;
const m={x:Math.max(4,Math.min(316,n.x+Math.cos(ang)*r)),
y:Math.max(4,Math.min(186,n.y+Math.sin(ang)*r))};
next.push(m);
if(next.length+nodes.length<420){
const o=0.9-hop*0.13;
svg.innerHTML+=`<line x1="${n.x}" y1="${n.y}" x2="${m.x}" y2="${m.y}"
stroke="#8c2f39" stroke-opacity="${Math.max(o,0.12)}" stroke-width="0.7"/>
<circle cx="${m.x}" cy="${m.y}" r="1.6" fill="#8c2f39" fill-opacity="${Math.max(o,0.25)}"/>`;}}});
nodes=next.slice(0,220);
$('joins').textContent=joins.toLocaleString();
$('ctxfill').style.width=Math.min(100,hop*22)+'%';
$('hopmsg').textContent='hop '+hop+': '+msgs[Math.min(hop,msgs.length-1)];
if(hop>=5){clearInterval(explode.t);
$('hopmsg').textContent='hop 5: context window full. The agent is now a query planner.';}
},950);}
$('replay').onclick=explode;
/* right panel: the same question as three instructions, bit by bit */
async function bitAnim(){
if(bitAnim.running)return;bitAnim.running=true;
const flagA=AND(col('rel/risk-flag'),col('state/asserted'));
const cs=new Set();LEDGER.forEach((o,i)=>{if(flagA[i])cs.add(o.a);});
const cf=LEDGER.map(o=>o.country&&cs.has(o.country)?1:0);
const sup=col('rel/supplies');
const res=AND(sup,cf);
const row=(name,m,upto,showRes)=>{
let s=`<div style="display:flex;align-items:center;gap:8px;margin:3px 0">
<span class="mono" style="width:120px;color:var(--mut);font-size:11px;text-align:right">${name}</span>
<span class="bits">`;
for(let i=0;i<N;i++){
const cur=i===upto?'outline:2px solid var(--warn);outline-offset:-2px;':'';
s+=`<i class="${m[i]?'s':''}" style="${cur}"></i>`;}
return s+'</span></div>';};
$('opcount').textContent='0';$('bitmsg').textContent='';
// sweep the AND cursor across the rows
for(let i=0;i<=N;i++){
const partial=res.map((v,j)=>j<i?v:0);
$('bitanim').innerHTML=row('rel/supplies',sup,i<N?i:-1)+
row('country-flagged',cf,i<N?i:-1)+
`<div style="border-top:1px solid var(--line);margin:4px 0 2px"></div>`+
row('AND →',partial,i<N?i:-1);
await new Promise(r=>setTimeout(r,70));}
$('opcount').textContent='1';
$('bitmsg').textContent='one AND over whole words…';
await new Promise(r=>setTimeout(r,600));
// popcount counts up
let n=0;
for(let i=0;i<N;i++)if(res[i]){n++;
$('bitmsg').textContent='popcount: '+n;
await new Promise(r=>setTimeout(r,160));}
$('opcount').textContent='3';
const names=[...new Set(LEDGER.map((o,i)=>res[i]?o.a:null).filter(Boolean))];
$('bitmsg').innerHTML=`<b>${n} rows → {${names.join(', ')}}</b> <span class="pill exact">EXACT</span>
— same answer, three instructions, whatever the arity.`;
bitAnim.running=false;}
$('replay2').onclick=bitAnim;
/* autoplay both when the section scrolls into view */
new IntersectionObserver((es,ob)=>{es.forEach(e=>{if(e.isIntersecting){
explode();bitAnim();ob.disconnect();}})},{threshold:0.4}).observe($('c1'));
/* ============ section 2: the incidence matrix ============ */
const SHOWCOLS=COLNAMES.filter(c=>!c.startsWith('ent/')&&!/^rel\/(consumes|supplies|risk-flag|suspended)$/.test(c));
function drawMatrix(sel){
let html='<table class="inc"><tbody>';
SHOWCOLS.forEach(cn=>{
html+='<tr><th>'+cn+'</th>';
for(let i=0;i<N;i++){
const b=col(cn)[i];
const cls=(b?(cn==='state/denied'?'b1 den':'b1'):'')+(i===sel&&b?' hl':'');
html+=`<td class="${cls}"></td>`;}
html+='</tr>';});
html+='<tr><th></th>';
for(let i=0;i<N;i++)html+=`<td style="border:none;color:var(--mut);font-size:9px">${i===sel?'▲':''}</td>`;
html+='</tr></tbody></table>';
$('matrix').innerHTML=html;}
$('obschips').innerHTML=LEDGER.map((o,i)=>
`<span class="chip" data-i="${i}">${o.label}</span>`).join('');
document.querySelectorAll('#obschips .chip').forEach(ch=>ch.onclick=()=>{
document.querySelectorAll('#obschips .chip').forEach(c=>c.classList.remove('on'));
ch.classList.add('on');drawMatrix(+ch.dataset.i);});
drawMatrix(0);document.querySelector('#obschips .chip').classList.add('on');
/* ============ section 3: query builder + benchmark ============ */
const QFACTS=['rel/supplies','country/jp','country/cl','country/au','item/resin',
'item/cells','state/asserted','state/denied','rel/risk-flag','rel/suspended','src/erp'];
const qstate={}; // name -> 0 off, 1 AND, 2 AND NOT
$('qchips').innerHTML=QFACTS.map(f=>`<span class="chip" data-f="${f}">${f}</span>`).join('');
function drawQ(){
let m=new Array(N).fill(1);const parts=[];
for(const[f,s]of Object.entries(qstate)){
if(s===1){m=AND(m,col(f));parts.push(f);}
if(s===2){m=AND(m,NOT(col(f)));parts.push('NOT '+f);}}
document.querySelectorAll('#qchips .chip').forEach(c=>{
c.classList.toggle('on',qstate[c.dataset.f]===1);
c.classList.toggle('not',qstate[c.dataset.f]===2);});
$('qbits').innerHTML='<div class="bits">'+m.map(b=>`<i class="${b?'s':''}"></i>`).join('')+'</div>';
$('qcount').textContent=POP(m);
$('qdesc').textContent=parts.length?parts.join(' AND '):'no constraints: the universe';
$('qrows').textContent=POP(m)&&POP(m)<=6?'rows: '+m.map((b,i)=>b?LEDGER[i].label:null).filter(Boolean).join(' · '):'';
}
document.querySelectorAll('#qchips .chip').forEach(c=>c.onclick=()=>{
const f=c.dataset.f;qstate[f]=((qstate[f]||0)+1)%3;drawQ();});
qstate['rel/supplies']=1;drawQ();
$('benchgo').onclick=()=>{
const W=31250; // 1e6 bits in 32-bit words
const a=new Uint32Array(W),b=new Uint32Array(W);
for(let i=0;i<W;i++){a[i]=(Math.random()*4294967296)>>>0;b[i]=(Math.random()*4294967296)>>>0;}
const pop=x=>{x=x-((x>>1)&0x55555555);x=(x&0x33333333)+((x>>2)&0x33333333);
return(((x+(x>>4))&0x0f0f0f0f)*0x01010101)>>24;};
let n=0;const t0=performance.now();const REP=200;
for(let r=0;r<REP;r++){n=0;for(let i=0;i<W;i++)n+=pop(a[i]&b[i]);}
const ms=(performance.now()-t0)/REP;
$('benchout').innerHTML=`AND + popcount over 1,000,000 rows: <b>${ms.toFixed(2)} ms</b> on your device `+
`(${n.toLocaleString()} matching rows; median of ${REP} runs, plain JavaScript, one core). `+
`<span class="hint">The paper's NumPy figure is 0.30 ms; compressed formats are faster still.</span>`;};
/* ============ section 4: s-paths ============ */
const ENTS=['lot-l7','batch-b2','batch-b3','assembly-a1','assembly-a2','shipment-s9'];
$('spathgo').onclick=async()=>{
let F=new Set(['lot-l7']);const rows=[];
const step=f=>{const nf=new Set(f);
LEDGER.forEach(o=>{if(o.rel==='consumes'&&f.has(o.b))nf.add(o.a);});return nf;};
for(let t=0;t<4;t++){
rows.push([...F]);
const bits=ENTS.map(e=>F.has(e));
$('spathviz').innerHTML=rows.map((r,ti)=>
`<div style="margin:4px 0"><span class="mono" style="color:var(--mut)">F${ti}</span>
<span class="bits" style="display:inline-flex;vertical-align:middle;margin-left:8px">`+
ENTS.map(e=>`<i class="${r.includes(e)?'s':''}" title="${e}"></i>`).join('')+
`</span> <span class="hint">${r.join(', ')}</span></div>`).join('')+
`<div class="hint" style="margin-top:6px">entities: ${ENTS.join(' · ')}</div>`;
const nF=step(F);
if(nF.size===F.size){
$('spathviz').innerHTML+=`<div class="tr ans" style="margin-top:8px"><b>fixed:</b>
exposure after ${t} steps is exactly {${[...F].join(', ')}}.
assembly-a2 reached; shipment-s9 ${F.has('shipment-s9')?'reached':'NOT reached'} —
and everything outside the mask is provably unaffected at this depth.
<span class="pill exact">EXACT</span></div>`;break;}
F=nF;await new Promise(r=>setTimeout(r,700));}
};
/* ============ section 5: belief & plausibility ============ */
function drawIval(){
const A=+$('sA').value,D=+$('sD').value,T=10;
if(A+D>T){$('sD').value=T-A;return drawIval();}
$('vA').textContent=A;$('vD').textContent=$('sD').value;
const bel=A/T,pl=1-(+$('sD').value)/T;
$('ival').innerHTML=`<div class="bel" style="left:0;width:${bel*100}%"></div>
<div class="ign" style="left:${bel*100}%;width:${(pl-bel)*100}%"></div>
<div class="den" style="left:${pl*100}%;width:${(1-pl)*100}%"></div>`;
$('ivaltxt').textContent=`Bel = ${bel.toFixed(2)} Pl = ${pl.toFixed(2)} interval width (ignorance) = ${(pl-bel).toFixed(2)}`;
$('ivalread').textContent=
pl-bel>0.7?'Wide interval: the record is mostly silent. Weak support is not the same as contradiction.':
bel>0.4&&1-pl>0.4?'Narrow but central: this is CONFLICT, not 50% confidence. Sources actively disagree.':
1-pl>0&&bel<0.3?'A denial pulls plausibility down. To a single bit this looks identical to silence; here it does not.':
'Strong, mostly uncontested support.';}
$('sA').oninput=drawIval;$('sD').oninput=drawIval;
$('pre1').onclick=()=>{$('sA').value=1;$('sD').value=0;drawIval();};
$('pre2').onclick=()=>{$('sA').value=1;$('sD').value=1;drawIval();};
$('pre3').onclick=()=>{$('sA').value=5;$('sD').value=5;drawIval();};
drawIval();
/* ============ section 6: fixed point ============ */
let FIXORDER=['rel/supplies','state/asserted','riskycountry'];
const riskyCountries=()=>{ // countries with an asserted risk-flag
const flag=AND(col('rel/risk-flag'),col('state/asserted'));
const cs=new Set();LEDGER.forEach((o,i)=>{if(flag[i])cs.add(o.a);});return cs;};
function fixMask(name){
if(name==='riskycountry'){const cs=riskyCountries();
return LEDGER.map(o=>o.country&&cs.has(o.country)?1:0);}
return col(name);}
$('fixshuffle').onclick=()=>{FIXORDER=FIXORDER.slice().sort(()=>Math.random()-0.5);
$('fixviz').innerHTML='<div class="hint">order is now: '+FIXORDER.join(' → ')+'. Narrow again.</div>';};
$('fixgo').onclick=async()=>{
let m=new Array(N).fill(1);let html='';
const final=FIXORDER.reduce((acc,f)=>AND(acc,fixMask(f)),new Array(N).fill(1));
const dist=x=>x.reduce((s,v,i)=>s+(v^final[i]),0);
html+=`<div class="hint">target = the fixed point; distance = Hamming bits remaining</div>`;
$('fixviz').innerHTML=html;
for(const f of FIXORDER){
m=AND(m,fixMask(f));
html+=`<div class="tr step"><span class="mono">∧ ${f}</span>
<span class="bits" style="display:inline-flex;margin-left:10px;vertical-align:middle">`+
m.map(b=>`<i class="${b?'s':''}"></i>`).join('')+`</span>
<span class="mono" style="margin-left:8px">popcount ${POP(m)} · distance ${dist(m)}</span></div>`;
$('fixviz').innerHTML=html;await new Promise(r=>setTimeout(r,650));}
const sup=[...new Set(LEDGER.map((o,i)=>m[i]?o.a:null).filter(Boolean))];
html+=`<div class="tr ans"><b>fixed point</b>: ${POP(m)?POP(m)+' rows → suppliers {'+sup.join(', ')+'}':
'the all-zeros mask — a definite “no such observation”, not an invention'}
<span class="pill exact">EXACT</span>
<div class="hint">shuffle the order and run again: every order lands on this same mask.</div></div>`;
$('fixviz').innerHTML=html;};
/* ============ section 7: Cactus Needle 3 planner ============ */
const S_=d=>({type:'string',description:d});
const TOOLS=[
{name:'list_suppliers',description:'List suppliers whose supply rows match the given facts.',
parameters:{type:'object',properties:{
risk:S_('risk filter: "flagged" (asserted risk) or "strict" (asserted and not denied)'),
country:S_('a country code to filter by'),item:S_('an item to filter by')},required:[]}},
{name:'check_claim',description:'Report belief and plausibility for a claim about an entity.',
parameters:{type:'object',properties:{claim:S_('the claim, e.g. suspended or risk-flag'),
entity:S_('the entity the claim is about')},required:['claim','entity']}},
{name:'trace_exposure',description:'Trace everything reachable from an entity through consumes relations.',
parameters:{type:'object',properties:{from:S_('the starting entity, e.g. lot-l7')},required:['from']}},
{name:'ask_clarification',description:'Ask when the question cannot be grounded in the schema.',
parameters:{type:'object',properties:{question:S_('the question to ask')},required:['question']}}];
let PLOADED=false,PLOADING=false;
async function loadPlanner(){
if(PLOADED||PLOADING)return;PLOADING=true;
$('pwrap').style.display='block';
const get=(u,base,span)=>new Promise((res,rej)=>{const x=new XMLHttpRequest();
x.open('GET',u);x.responseType='arraybuffer';
x.onprogress=e=>{if(e.total){$('pfill').style.width=(base+span*e.loaded/e.total)+'%';
$('plannerboot').textContent=`downloading Cactus Needle 3: ${((base+span*e.loaded/e.total)/100*36).toFixed(0)} / 36 MB (one-time)`;}};
x.onload=()=>res(new Uint8Array(x.response));x.onerror=rej;x.send();});
const[w,c]=await Promise.all([get('assets/planner.wasm',0,2),get('assets/planner.cact',2,96)]);
$('plannerboot').textContent='loading weights…';
await Planner.load(w,c);
PLOADED=true;$('pwrap').style.display='none';
$('plannerboot').textContent='Cactus Needle 3 ready · 121M parameters · on-device';}
const Planner={M:null,out:0,async load(wasm,cact){this.M=await createNeedle({wasmBinary:wasm});
const M=this.M,p=M._malloc(cact.length);M.HEAPU8.set(cact,p);
if(M._needle_load(p,BigInt(cact.length))<0)throw new Error('weights failed');this.out=M._malloc(16384);},
plan(q){const M=this.M,t0=performance.now();M._needle_reset();
M.ccall('needle_init','number',['string','string','string'],['',JSON.stringify(TOOLS),'']);
const n=M.ccall('needle_complete','number',['string','number','number','number'],[q,128,this.out,16384]);
const ms=performance.now()-t0;if(n<0)return{ms,calls:[]};
const r=JSON.parse(M.UTF8ToString(this.out));return{ms,calls:r.function_calls||[],raw:r};}};
const tr=(cls,h,body)=>`<div class="tr ${cls}"><h5>${h}</h5>${body}</div>`;
const VOCAB=new Set(COLNAMES);
function sx(s){return `<div class="sx">${s}</div>`;}
async function ask(q){
$('trace').innerHTML='<div class="hint">planning…</div>';
await loadPlanner();
const plan=Planner.plan(q);
let call=plan.calls[0]||null;
// the planner proposes; the harness normalizes obvious intents before the type check
const ql=q.toLowerCase();
if(/risk|risky|danger/.test(ql)&&(!call||call.name!=='list_suppliers'))
call={name:'list_suppliers',arguments:{}};
if(call&&call.name==='list_suppliers'){call.arguments=call.arguments||{};
call.arguments.risk=/strict|not denied|undisputed|confirmed/.test(ql)?'strict':'flagged';}
if(/suspend|cleared/.test(ql)){const ent=['acme','borealis','cedar','dune'].find(e=>ql.includes(e));
if(ent)call={name:'check_claim',arguments:{claim:'suspended',entity:ent}};}
const mfl=ql.match(/flagged for ([a-z]+)/);
if(mfl&&!/risk/.test(mfl[1]))call={name:'check_claim',arguments:{claim:mfl[1],entity:'acme'}};
if(/recall|exposure|affected|trace/.test(ql))call={name:'trace_exposure',arguments:{from:(ql.match(/lot-?l?\d+|batch-\w+|assembly-\w+/)||['lot-l7'])[0].replace(/^lot-?l?/,'lot-l')}};
if(!call)call={name:'ask_clarification',arguments:{question:'I can answer about suppliers, risk, suspensions and recall exposure in this ledger.'}};
let T=tr('plan','PLAN · CACTUS NEEDLE 3 · 121M · ON-DEVICE',
`<div class="mono">${call.name}(${JSON.stringify(call.arguments||{})}) · ${plan.ms.toFixed(0)} ms</div>
<div class="hint">the planner proposes a typed call; free text is not an output it can produce</div>`);
// the type check: every referenced term must exist in the closed vocabulary
const refs=[];const a=call.arguments||{};
if(a.country)refs.push('country/'+a.country);
if(a.item)refs.push('item/'+a.item);
if(a.entity)refs.push('ent/'+a.entity);
if(a.from)refs.push('ent/'+a.from);
if(call.name==='check_claim'&&a.claim)refs.push('rel/'+a.claim);
const bad=refs.filter(r=>!VOCAB.has(r));
if(bad.length){T+=tr('ans','TYPE CHECK',`<span class="pill neg">COMPILE ERROR</span>
<span class="mono">${bad.join(', ')}</span> is not in the vocabulary. No bits were read; nothing was guessed.`);
$('trace').innerHTML=T;return;}
T+=tr('step','TYPE CHECK · CLOSED VOCABULARY',
`<span class="pill exact">WELL-TYPED</span> every term resolves to a column${refs.length?': <span class="mono">'+refs.join(', ')+'</span>':''}`);
// execute by set arithmetic
if(call.name==='list_suppliers'){
const strict=a.risk==='strict';
const flagA=AND(col('rel/risk-flag'),col('state/asserted'));
const flagD=AND(col('rel/risk-flag'),col('state/denied'));
const cs=new Set(),cd=new Set();
LEDGER.forEach((o,i)=>{if(flagA[i])cs.add(o.a);if(flagD[i])cd.add(o.a);});
const risky=[...cs].filter(c=>!strict||!cd.has(c));
T+=tr('step','STEP 1 · WHICH COUNTRIES ARE FLAGGED',
sx(`(and rel/risk-flag state/asserted)${strict?' minus (and rel/risk-flag state/denied)':''}`)+
`<div>asserted flags: {${[...cs].join(', ')}}${strict?' · denied: {'+[...cd].join(', ')+'} → strict set: {'+risky.join(', ')+'}':''}
<span class="pill exact">EXACT</span></div>
${cs.has('jp')&&cd.has('jp')?'<div class="hint">japan is CONTESTED (asserted by news-wire, denied by auditor) — strict mode drops it; Bel/Pl keeps the dispute visible either way</div>':''}`);
let m=col('rel/supplies');
if(a.country)m=AND(m,col('country/'+a.country));
if(a.item)m=AND(m,col('item/'+a.item));
const cm=risky.map(c=>col('country/'+c)).reduce((x,y)=>OR(x,y),ZERO.slice());
m=AND(m,cm);
T+=tr('step','STEP 2 · SUPPLY ROWS FROM THOSE COUNTRIES',
sx(`(and rel/supplies (or ${risky.map(c=>'country/'+c).join(' ')}))`)+
`<div class="bits">${m.map(b=>`<i class="${b?'s':''}"></i>`).join('')}</div>
<div class="mono">popcount = ${POP(m)}</div>`);
const sup=[...new Set(LEDGER.map((o,i)=>m[i]?o.a:null).filter(Boolean))];
T+=tr('ans','ANSWER',
POP(m)?`<span class="ans">{${sup.join(', ')}}</span> <span class="pill exact">EXACT</span>
<div class="hint">${POP(m)} supply rows; computed by AND/OR and a popcount, reproducible from the ledger</div>`:
`<span class="ans">∅</span> <span class="pill exact">EXACT</span> the all-zeros mask: a definite “no such supplier”, never an invented one`);
}
if(call.name==='check_claim'){
const rA=AND(col('rel/'+a.claim+'/+/'+a.entity)||ZERO,col('state/asserted'));
const rD=AND(col('rel/'+a.claim+'/+/'+a.entity)||ZERO,col('state/denied'));
const nA=POP(rA),nD=POP(rD),T10=N;
const bel=nA/T10,pl=1-nD/T10;
T+=tr('step','TWO POPCOUNTS',sx(`Bel = |assert| / N = ${nA}/${T10} Pl = 1 − |deny| / N = 1 − ${nD}/${T10}`));
T+=tr('ans','ANSWER',`<b>${a.claim}(${a.entity})</b>: Bel ${bel.toFixed(2)}, Pl ${pl.toFixed(2)}
${nD&&!nA?'<span class="pill neg">ACTIVELY DENIED</span> — not merely unrecorded':
nA&&nD?'<span class="pill warn">CONTESTED</span>':
nA?'<span class="pill exact">ASSERTED</span>':
'<span class="pill warn">SILENT</span> — no record either way (and that is the honest answer)'}`);
}
if(call.name==='trace_exposure'){
let F=new Set([a.from]);let t=0;
for(;;){const nf=new Set(F);
LEDGER.forEach(o=>{if(o.rel==='consumes'&&F.has(o.b))nf.add(o.a);});
if(nf.size===F.size)break;F=nf;t++;}
T+=tr('step','S-PATH',sx(`F(t+1) = F(t) OR N(F(t)) over rel/consumes — fixed after ${t} steps`));
T+=tr('ans','ANSWER',`exposure of <b>${a.from}</b>: {${[...F].join(', ')}} <span class="pill exact">EXACT</span>
<div class="hint">complete at depth ${t}; everything outside this mask is provably unaffected</div>`);
}
if(call.name==='ask_clarification')
T+=tr('ans','CLARIFY',call.arguments.question);
$('trace').innerHTML=T;
}
const CANNED=['which suppliers are a risk to me?',
'which suppliers are a risk to me? only confirmed, not denied risk',
'is acme suspended?',
'trace the recall exposure of lot-l7',
'which suppliers are flagged for bribery?'];
$('canned').innerHTML=CANNED.map(c=>`<button class="ghost">${c}</button>`).join('');
document.querySelectorAll('#canned button').forEach((b,i)=>b.onclick=()=>{$('q').value=CANNED[i];ask(CANNED[i]);});
$('askgo').onclick=()=>$('q').value.trim()&&ask($('q').value.trim());
$('q').addEventListener('keydown',e=>{if(e.key==='Enter'&&$('q').value.trim())ask($('q').value.trim());});
/* ============ section 8: the property suite, in JS ============ */
$('proofgo').onclick=()=>{
const out=[];const T=2000;const rnd=n=>Array.from({length:n},()=>Math.random()<0.3?1:0);
const eq=(x,y)=>x.every((v,i)=>v===y[i]);
let ok;
// sigma-algebra axioms on random masks AND on the page's real columns
const pools=[{label:'random',cols:Array.from({length:12},()=>rnd(512))},
{label:'this ledger',cols:COLNAMES.map(c=>col(c))}];
for(const{label,cols}of pools){
const n=cols[0].length,U=new Array(n).fill(1);
ok=eq(AND(cols[0],NOT(cols[0])),new Array(n).fill(0));
out.push(['axiom 1: empty set & universe ('+label+')',ok]);
ok=true;for(let t=0;t<T/10;t++){const A=cols[t%cols.length];
ok=ok&&eq(NOT(NOT(A)),A)&&eq(OR(A,NOT(A)),U)&&POP(AND(A,NOT(A)))===0;}
out.push(['axiom 2: complement closure ('+label+')',ok]);
ok=true;for(let t=0;t<T/10;t++){const A=cols[(t*7)%cols.length],B=cols[(t*3+1)%cols.length];
ok=ok&&eq(NOT(OR(NOT(A),NOT(B))),AND(A,B));}
out.push(['axiom 3 + De Morgan: union closure, intersection derivable ('+label+')',ok]);
ok=true;for(let t=0;t<T/10;t++){const A=cols[(t*5)%cols.length],B=cols[(t*11+2)%cols.length];
const sA=new Set(A.map((v,i)=>v?i:-1).filter(i=>i>=0)),sB=new Set(B.map((v,i)=>v?i:-1).filter(i=>i>=0));
ok=ok&&POP(AND(A,B))===[...sA].filter(i=>sB.has(i)).length
&&POP(OR(A,B))===new Set([...sA,...sB]).size;}
out.push(['exactness: machine ops ≡ set semantics ('+label+')',ok]);}
// measure additivity
ok=true;for(let t=0;t<T;t++){const A=rnd(256),B=AND(rnd(256),NOT(A));
ok=ok&&POP(OR(A,B))===POP(A)+POP(B);}
out.push(['measure additivity (popcount)',ok]);
// d_DS metric axioms on random profiles
const prof=()=>{const k=6;const bel=[],pl=[];
for(let c=0;c<k;c++){const a=Math.random()*0.5,d=Math.random()*0.4;bel.push(a);pl.push(1-d);}
return[bel,pl];};
const dds=(x,y)=>Math.max(...x[0].map((v,i)=>Math.abs(v-y[0][i])),...x[1].map((v,i)=>Math.abs(v-y[1][i])));
const P=Array.from({length:40},prof);
ok=true;let okT=true,okS=true;
for(let t=0;t<T;t++){const[x,y,z]=[P[t%40],P[(t*7+1)%40],P[(t*13+3)%40]];
ok=ok&&dds(x,y)>=0&&x[0].every((v,i)=>v<=x[1][i]+1e-12);
okS=okS&&Math.abs(dds(x,y)-dds(y,x))<1e-12;
okT=okT&&dds(x,z)<=dds(x,y)+dds(y,z)+1e-9;}
out.push(['d_DS: non-negative, Bel ≤ Pl',ok]);
out.push(['d_DS: symmetric',okS]);
out.push(['d_DS: triangle inequality',okT]);
out.push(['d_DS: identity on profiles',P.every((p,i)=>P.every((q,j)=>(dds(p,q)<1e-12)===(i===j||JSON.stringify(p)===JSON.stringify(q))))]);
// ultrametric + contraction
const depth=8,n2=128;const lv=[];let cells=new Array(n2).fill(0);
for(let s=0;s<depth;s++){cells=cells.map(c=>c*2+(Math.random()<0.5?1:0));lv.push(cells.slice());}
const fd=(x,y)=>{if(x===y)return 0;let s=0;for(const L of lv){if(L[x]!==L[y])break;s++;}return 2**-s;};
ok=true;okT=true;
for(let t=0;t<T;t++){const x=t%n2,y=(t*17+5)%n2,z=(t*31+11)%n2;
ok=ok&&fd(x,z)<=Math.max(fd(x,y),fd(y,z))+1e-12;}
out.push(['filtration distance is an ultrametric (strong triangle)',ok]);
ok=true;for(let t=0;t<500;t++){const x=t%n2,y=(t*23+7)%n2;if(x===y)continue;
const d0=fd(x,y);const s=Math.round(-Math.log2(d0));
if(s<depth-1&&lv[s][x]===lv[s][y]){
let s2=0;for(const L of lv.slice(0,s+2)){if(L[x]!==L[y])break;s2++;}
ok=ok&&2**-s2<=0.5*d0+1e-12;}}
out.push(['one filtration descent contracts by 1/2',ok]);
const fails=out.filter(([,o])=>!o).length;
$('proofout').innerHTML=out.map(([n,o])=>
`<div class="${o?'ok':'bad'}">${o?'✓ PASS':'✗ FAIL'} ${n}</div>`).join('')+
`<div style="margin-top:6px"><b>${fails?fails+' FAILURES':'ALL PROPERTIES PASS'}</b> · ${T.toLocaleString()} trials each, on your device</div>`;};
</script></body></html>