Pythia-IV Certificate Lab

Code:

<!DOCTYPE html>

<head>

<title>Pythia-IV Certificate Lab — Rigorous Residue Envelope (100% Local)</title>

<style>

:root{

--ink:#2d3436; --bg:#f4f6f8; --panel:#fff; --accent:#6c5ce7; --accent-d:#5847ea;

--muted:#555; --ok:#00b894; --warn:#d97706; --err:#e74c3c; --soft:#fafbfd;

}

body{font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Roboto,Helvetica,Arial,sans-serif;background:var(--bg);color:var(--ink);line-height:1.6;margin:0;padding:20px}

.container{max-width:1200px;margin:0 auto}

h1,h2,h3{color:#1a2533;border-bottom:2px solid var(--accent);padding-bottom:10px;margin-top:0}

.panel{background:var(--panel);padding:20px;border-radius:12px;box-shadow:0 6px 24px rgba(0,0,0,.07);margin-bottom:18px}

.description{background:var(--soft);border-left:4px solid var(--accent);color:var(--muted)}

.row{display:flex;gap:8px;flex-wrap:wrap;align-items:center}

input[type="text"],input[type="number"],select{padding:10px;border:1px solid #d1d5db;border-radius:8px}

.btn{background:var(--accent);color:#fff;border:none;border-radius:8px;padding:10px 14px;font-weight:700;cursor:pointer}

.btn:hover{background:var(--accent-d)}

.btn.ghost{background:#64748b}

.btn.warn{background:var(--warn)}

.btn.danger{background:#c53030}

.mono{font-family:ui-monospace,SFMono-Regular,Menlo,Consolas,monospace}

.console{font-family:ui-monospace,SFMono-Regular,Menlo,Consolas,monospace;background:#1f2937;color:#e5e7eb;border-radius:8px;padding:12px;height:260px;overflow:auto;white-space:pre}

.tag{display:inline-block;background:#eef2ff;color:#3730a3;border-radius:999px;padding:2px 8px;font-size:.85em}

.badge{padding:2px 8px;border-radius:6px;font-weight:700}

.ok{background:#e0f8f7;color:#035c4a}

.fail{background:#ffe9e6;color:#8b2c24}

table{width:100%;border-collapse:collapse;font-size:.95em}

th,td{border:1px solid #e5e7eb;padding:8px;text-align:left}

th{background:#f8fafc}

details{background:#fff;border:1px solid #e5e7eb;border-radius:10px;padding:10px 14px}

details>summary{cursor:pointer;font-weight:700}

code{background:#f6f8fa;padding:2px 6px;border-radius:4px}

.note{color:#6b7280}

</style>

</head>

<body>

<h1>Pythia-IV Certificate Lab</h1>

<p><strong>Goal.</strong> Find a finite, periodic Lyapunov certificate for the accelerated odd-step map

<span class="mono">T(k)=K(3k+1)</span>, where

<span class="mono">K(n)=|n|/(n&−n)</span> is the largest odd divisor (<code>K(0)=0</code>).</p>

<p><strong>Rigor envelope.</strong> This page enforces the Lyapunov inequality for <em>all</em> integers in each residue class

$k\equiv r\pmod{2^m}$ using exact 2-adic logic:

if $t=\nu_2(3r+1)<m$, the next residue ranges over a full congruence class; if $t\ge m$, <em>any</em> odd residue can occur.

Constraints are encoded with bucket-max variables so we don’t miss any 2-adic branch.</p>

<p class="note"><strong>Important.</strong> Passing these finite tests would provide a checkable witness; it would still need a careful formal write-up.

This app does not claim a proof of Collatz.</p>

</div>

<h2>1) Odd-Step Chain Explorer</h2>

<label>Start integer n:</label>

<button class="btn ghost" id="clearChain">Clear</button>

</div>

<div class="console" id="chainLog">Ready.</div>

</div>

<h2>2) Rigorous Certificate Finder (covers all 2-adic branches)</h2>

<label>m (rigorous):</label><input id="mRig" type="number" value="16" min="4" max="18">

<label><input id="exemptSink" type="checkbox" checked> Exempt sink {1}</label>

<button class="btn" id="buildCert">Search Certificate</button>

<button class="btn ghost" id="exportPhi">Export φ (JSON)</button>

</div>

<table>

<thead><tr><th>Metric</th><th>Value</th></tr></thead>

<tbody>

<tr><td>Odd residues</td><td id="rc_nodes">—</td></tr>

<tr><td>Residues with t < m</td><td id="rc_low">—</td></tr>

<tr><td>Residues with t ≥ m</td><td id="rc_high">—</td></tr>

<tr><td>Bucket classes used</td><td id="rc_classes">—</td></tr>

<tr><td>Variables (φ + M’s)</td><td id="rc_vars">—</td></tr>

<tr><td>Constraints</td><td id="rc_edges">—</td></tr>

<tr><td>Verdict</td><td id="rc_verdict">—</td></tr>

</tbody>

</table>

</div>

<h2>3) Random-Integer Inequality Verifier</h2>

<label>Trials:</label><input id="verTrials" type="number" value="5000" min="100" max="200000">

<label>u range (k = r + u·2^m, 0 ≤ u < U):</label><input id="verU" type="number" value="100000" min="1" max="1000000000">

<button class="btn warn" id="runVerify">Run Verifier</button>

</div>

</div>

<h2>Proof Dock — precise statements</h2>

<summary>Arithmetic facts (used exactly)</summary>

<p><strong>Dyadic kernel.</strong> <code>K(n)=|n|/(n&−n)</code> equals the largest odd divisor (set <code>K(0)=0</code>).

Here <code>n&−n</code> isolates the least power of two dividing $n$.</p>

<p><strong>Odd-step map.</strong> For odd $k$, one step sends $k\mapsto (3k+1)/2^{\nu_2(3k+1)}$.</p>

</details>

<summary>Residue logic (covering all 2-adic branches)</summary>

<p>Fix $m\ge 1$ and an odd residue $r\in\{1,3,\dots,2^m-1\}$.

Write $t=\nu_2(3r+1)$.</p>

<ul>

<li>If $t<m$, then for all odd $k\equiv r\pmod{2^m}$ we have $\nu_2(3k+1)=t$.

The next residue ranges over the entire class

$ \{\,s\equiv (3r+1)/2^t \pmod{2^{m-t}},\ s\text{ odd}\,\}$ — we enforce the inequality for <em>all</em> those $s$.</li>

<li>If $t\ge m$, then for $k\equiv r\pmod{2^m}$ one can realize any $\nu_2(3k+1)=m+j$ with $j\ge 0$;

hence every odd residue $s$ can occur as the next residue. A worst-case bound

$w_{\max}(r)=\log(3+\tfrac1r)-m\log 2$ covers all those branches; we enforce the inequality

against the global maximum of $\phi$ over all odd residues.</li>

</ul>

</details>

<summary>Certificate theorem (rigorous finite witness)</summary>

<p>If there exist integers $m\ge 1$, $\varepsilon>0$, and a function

$\phi:\{\text{odd residues}\bmod 2^m\}\to\mathbb{R}$ such that:</p>

<ul>

<li>For every odd residue $r\neq 1$ with $t=\nu_2(3r+1)<m$, and for every odd

$s\equiv (3r+1)/2^t\ (\bmod\ 2^{m-t})$:<br>

$\phi(s)\le \phi(r) - \big(\log(3+\tfrac1r)-t\log 2 + \varepsilon\big).$</li>

<li>For every odd residue $r\neq 1$ with $t\ge m$: letting $M=\max\_s\phi(s)$,<br>

$M \le \phi(r) - \big(\log(3+\tfrac1r)-m\log 2 + \varepsilon\big)$, and $\phi(s)\le M$ for all odd $s\neq 1$.</li>

</ul>

<p>then the Lyapunov function $V(k)=\log k+\phi(k\bmod 2^m)$ strictly decreases by $\varepsilon$ at each odd

Collatz step for every odd $k\neq 1$. With the sink $\{1\}$ absorbing, all odd orbits terminate.</p>

</details>

</div>

/* ===== Core integer utilities ===== */

function absBig(n){ return n<0n ? -n : n; }

function K(n){ n=absBig(n); if(n===0n) return 0n; const twoPow = n & (-n); return n / twoPow; }

function v2(n){ if(n===0n) return Infinity; let c=0; while((n & 1n)===0n){ n >>= 1n; c++; } return c; }

function parseBigInt(s){ s=(s||'').trim().replace(/_/g,''); if(!s) throw new Error("Empty input"); try{ return BigInt(s); }catch{ throw new Error("Invalid integer"); } }

/* ===== 1) Chain explorer ===== */

const chainLog = document.getElementById('chainLog');

function logChain(s){ chainLog.textContent += '\n'+s; chainLog.scrollTop = chainLog.scrollHeight; }

document.getElementById('clearChain').onclick = ()=>{ chainLog.textContent='Cleared.'; };

document.getElementById('runChain').onclick = ()=>{

try{

const n0 = parseBigInt(document.getElementById('nInput').value);

if(n0<=0n) throw new Error("n must be positive");

chainLog.textContent = 'Running odd-step chain…';

let k = (n0 & 1n) ? n0 : K(n0); // start at odd

let steps=0;

while(true){

steps++;

const t = 3n*k+1n, e = v2(t), next = t>>BigInt(e);

logChain(`k=${k} -> (3k+1)=${t} = 2^${e} * ${next} ⇒ T(k)=${next}`);

if(next===1n){ logChain(`HIT 1 in ${steps} odd steps.`); break; }

if(steps>20000){ logChain(`Stopped at 20,000 steps.`); break; }

k = next;

}

}catch(e){ alert(e.message); }

};

/* ===== 2) Rigorous certificate builder (bucket maxima) ===== */

const ln2 = Math.log(2), ln3 = Math.log(3);

let lastCert = null;

function buildRigorousCertificate(m, eps, exemptSink){

const MOD = 1n<<BigInt(m);

// Build odd residues and maps

const odds = [];

for(let r=1n; r<MOD; r+=2n) odds.push(r);

const N = odds.length; // = 2^(m-1)

const idxOf = new Map(); odds.forEach((r,i)=>idxOf.set(r.toString(), i));

const sinkIdx = idxOf.get('1');

// Per-residue t and w_max

const tArr = new Uint16Array(N);

const wmax = new Float64Array(N);

let lowCount=0, highCount=0;

for(let i=0;i<N;i++){

const r = odds[i];

const t = v2(3n*r+1n);

const tt = (t===Infinity)? 0 : Number(t);

tArr[i] = tt;

const cut = Math.min(tt, m);

const wr = Math.log(3 + 1/Number(r)) - cut*ln2;

wmax[i] = wr;

if(tt < m) lowCount++; else highCount++;

}

// Build bucket classes for t<m

// Key: `${t}|${Amod}` where Amod in [0, 2^(m-t)-1]

const classMap = new Map(); // key -> classIndex

const classT = []; // classIndex -> t

const classAmod = []; // classIndex -> Amod (number)

const classMembers = []; // classIndex -> array of residue indices "s" in this class (s odd, s ≡ A mod 2^(m-t))

const pow2 = (k)=> 1<<k;

// Precompute lists of s in each class lazily (cache by (t,Amod))

function getClassIndex(t, Amod){

const key = t+"|"+Amod;

if(classMap.has(key)) return classMap.get(key);

const idx = classT.length;

classMap.set(key, idx);

classT.push(t);

classAmod.push(Amod);

classMembers.push(null); // fill on demand

return idx;

}

function buildMembersForClass(ci){

if(classMembers[ci]!==null) return;

const t = classT[ci], Amod = classAmod[ci];

const step = 1<<(m-t); // 2^(m-t)

const start = Amod % step;

const mem = [];

// iterate s in {Amod mod 2^(m-t)} that are odd in [1,2^m)

for(let s=start; s<(1<<m); s+=step){

if((s & 1)===1){

const sBig = BigInt(s);

const idx = idxOf.get(sBig.toString());

if(exemptSink && idx===sinkIdx) continue;

mem.push(idx);

}

classMembers[ci]=mem;

}

// Prepare edges for difference constraints v ≤ u + c

// We'll assign indices:

// φ residues: 0..N-1

// M_class variables: N..N+C-1

// M_all: N+C (only if used)

const edges = []; // [u,v,c]

let classIndexForResidue = new Int32Array(N); classIndexForResidue.fill(-1);

// First pass: gather classes and connect residue r (t<m) to its class

for(let i=0;i<N;i++){

if(exemptSink && i===sinkIdx) continue;

const tt = tArr[i];

if(tt < m){

// class key

const r = odds[i];

const A = Number(((3n*r+1n) >> BigInt(tt)) % (1n<<BigInt(m-tt))); // (3r+1)/2^t mod 2^(m-t)

const ci = getClassIndex(tt, A);

classIndexForResidue[i]=ci;

}

// Create M_class -> φ(s) edges (0 weight) for each class, once

const C = classT.length;

for(let ci=0; ci<C; ci++){

buildMembersForClass(ci);

const members = classMembers[ci];

const M_idx = N + ci;

for(const sIdx of members){

edges.push([M_idx, sIdx, 0]); // φ(s) ≤ M_class

}

// Add φ(r) → M_class edges with cost = -(wmax(r)+eps)

for(let i=0;i<N;i++){

if(exemptSink && i===sinkIdx) continue;

const tt = tArr[i];

if(tt < m){

const ci = classIndexForResidue[i];

const M_idx = N + ci;

const c = -(wmax[i] + eps);

edges.push([i, M_idx, c]); // M_class ≤ φ(r) - (w+ε)

}

// For t≥m residues: use global M_all

const useGlobal = true; // always create it; it’s cheap

const Mall = N + C;

// M_all -> φ(s) edges (0 weight) for all odd s except (maybe) sink

for(let sIdx=0; sIdx<N; sIdx++){

if(exemptSink && sIdx===sinkIdx) continue;

edges.push([Mall, sIdx, 0]); // φ(s) ≤ M_all

}

// For each residue r with t≥m, add φ(r) → M_all with cost = -(wmax(r)+eps)

for(let i=0;i<N;i++){

if(exemptSink && i===sinkIdx) continue;

if(tArr[i] >= m){

const c = -(wmax[i] + eps);

edges.push([i, Mall, c]); // M_all ≤ φ(r) - (w+ε)

}

// Now solve difference constraints via Bellman–Ford (shortest paths)

const V = N + C + 1; // include M_all

const dist = new Float64Array(V);

dist.fill(0); // gauge fixing: zero source with 0 edges to all vars makes 0 an admissible baseline

// Add super source S -> every node with weight 0 (implicit by dist init and relaxation form)

// Bellman-Ford

const E = edges.length;

let changed = true;

for(let it=0; it<V; it++){

changed = false;

for(let e=0; e<E; e++){

const u = edges[e][0], v = edges[e][1], c = edges[e][2];

const cand = dist[u] + c;

if(dist[v] > cand){

dist[v] = cand;

changed = true;

}

if(!changed) break;

if(it===V-1 && changed){

return {

ok:false,

reason:'Negative cycle detected (constraints infeasible)',

stats:{N,lowCount,highCount,C,V,E}

};

}

// Build φ from the first N entries

const phi = new Float64Array(N);

for(let i=0;i<N;i++) phi[i]=dist[i];

// Report

return {

ok:true,

phi, odds, m, eps, exemptSink,

stats:{N,lowCount,highCount,C,V,E}

};

}

/* ===== Export and UI glue for certificate ===== */

document.getElementById('buildCert').onclick = ()=>{

const m = Math.max(4, Math.min(18, Number(document.getElementById('mRig').value||16)));

let eps = Number(document.getElementById('eps').value||'1e-6');

if(!(eps>0)) eps = 1e-6;

const exemptSink = document.getElementById('exemptSink').checked;

const log = document.getElementById('certLog');

log.textContent = 'Building rigorous constraints (this is exact for all 2-adic branches at this modulus)…';

// Build & solve

const res = buildRigorousCertificate(m, eps, exemptSink);

const nodesCell = document.getElementById('rc_nodes');

const lowCell = document.getElementById('rc_low');

const highCell = document.getElementById('rc_high');

const clsCell = document.getElementById('rc_classes');

const varCell = document.getElementById('rc_vars');

const edgCell = document.getElementById('rc_edges');

const verCell = document.getElementById('rc_verdict');

if(!res.ok){

nodesCell.textContent = res.stats.N.toLocaleString();

lowCell.textContent = res.stats.lowCount.toLocaleString();

highCell.textContent = res.stats.highCount.toLocaleString();

clsCell.textContent = res.stats.C.toLocaleString();

varCell.textContent = res.stats.V.toLocaleString();

edgCell.textContent = res.stats.E.toLocaleString();

verCell.innerHTML = '<span class="badge fail">NO CERTIFICATE</span> '+res.reason;

log.textContent = `Variables = ${res.stats.V.toLocaleString()}, Constraints = ${res.stats.E.toLocaleString()}\n`+

`Infeasible at ε=${eps}. Try adjusting m or ε.`;

lastCert = null;

return;

}

const {N,lowCount,highCount,C,V,E} = res.stats;

nodesCell.textContent = N.toLocaleString();

lowCell.textContent = lowCount.toLocaleString();

highCell.textContent = highCount.toLocaleString();

clsCell.textContent = C.toLocaleString();

varCell.textContent = V.toLocaleString();

edgCell.textContent = E.toLocaleString();

verCell.innerHTML = '<span class="badge ok">CERTIFICATE FOUND</span> Rigorous residue envelope satisfied.';

log.textContent =

`Rigorous constraints satisfied for m=${m}, ε=${eps}.\n`+

`N (odd residues) = ${N.toLocaleString()}\n`+

`t<m residues = ${lowCount.toLocaleString()}\n`+

`t≥m residues = ${highCount.toLocaleString()}\n`+

`Bucket classes used = ${C.toLocaleString()}\n`+

`Variables (φ + M’s) = ${V.toLocaleString()}\n`+

`Constraints = ${E.toLocaleString()}\n`+

`Note: This certificate enforces the inequality for all 2-adic branches in each residue class.`;

lastCert = res;

};

document.getElementById('exportPhi').onclick = ()=>{

if(!lastCert){ alert("No certificate to export."); return; }

const {phi, odds, m, eps, exemptSink} = lastCert;

const obj = {

modulus:`2^${m}`, m, epsilon:eps, exemptSink,

residues: odds.map(x=>x.toString()),

phi: Array.from(phi)

};

const b = new Blob([JSON.stringify(obj,null,2)], {type:'application/json'});

const url = URL.createObjectURL(b);

const a = document.createElement('a'); a.href=url; a.download='collatz_phi_rigorous.json';

document.body.appendChild(a); a.click(); a.remove(); URL.revokeObjectURL(url);

};

/* ===== 3) Random-integer verifier (real k, not just residues) ===== */

document.getElementById('runVerify').onclick = ()=>{

const trials = Math.max(100, Math.min(200000, Number(document.getElementById('verTrials').value||5000)));

const U = Math.max(1, Math.min(1_000_000_000, Number(document.getElementById('verU').value||100000)));

const verLog = document.getElementById('verLog');

const verSum = document.getElementById('verSummary');

if(!lastCert){ verLog.textContent='No φ loaded. Run the rigorous certificate search first.'; verSum.textContent='—'; return; }

const {phi, odds, m, eps, exemptSink} = lastCert;

const MOD = 1n<<BigInt(m);

const idxOf = new Map(); odds.forEach((r,i)=>idxOf.set(r.toString(), i));

const sinkIdx = idxOf.get('1');

function residueIndex(x){ const r = x % MOD; return idxOf.get(r.toString()); }

let ok=0, fail=0;

let worstSlack = Infinity, example = null;

for(let t=0;t<trials;t++){

// random residue

const i = (Math.random() * odds.length) | 0;

const r = odds[i];

if(exemptSink && i===sinkIdx){ t--; continue; } // skip sink as start

// random u

const u = BigInt( (Math.random()*U) | 0 );

const k = r + (u<<BigInt(m));

// odd step

const T = 3n*k + 1n;

const e = v2(T);

const next = T >> BigInt(e);

// Check inequality

const idxNext = residueIndex(next);

if(exemptSink && i===sinkIdx && idxNext===sinkIdx){ continue; } // trivial

const lhs = Math.log(Number(next)) + phi[idxNext];

const rhs = Math.log(Number(k)) + phi[i] - eps;

const slack = rhs - lhs; // want >= 0

if(slack >= -1e-12){ ok++; } else { fail++; if(slack<worstSlack){ worstSlack=slack; example={k:k.toString(), next:next.toString(), i, idxNext}; } }

}

verSum.textContent = `${ok} ok, ${fail} fail`;

if(fail===0){

verLog.textContent = `All sampled integers satisfied the rigorous inequality (tol 1e-12).`;

}else{

verLog.textContent =

`${fail} failures. Worst slack = ${worstSlack}\n`+

`Example: k=${example.k} → next=${example.next}, class i=${example.i}, next idx=${example.idxNext}\n`+

`Try smaller ε or different m.`;

}

};

</script>

</body>

</html>