Spaces:
Running
chore(sync): mirror front-door files to Space (hf-sync)
Browse filesAutomated front-door sync from szl-holdings/a11oy main via hf-sync.
Added/updated: cathedral.html, console/docs.html, console/index.html, console/pricing.html, console/throne-room.html, console/throne-room.js, pages/api-keys.html, pages/audit.html, pages/ayni.html, pages/brain-dual.html, pages/brain-jack.html, pages/brain.html, pages/chaski.html, pages/codex-kernel.html, pages/company.html, pages/compliance.html, pages/console.html, pages/counter-uas.html, pages/cued-engagement.html, pages/docs.html, pages/evidence.html, pages/gap-report.html, pages/hatun-mcp.html, pages/hub.html, pages/integrations.html, pages/landing.html, pages/mesh.html, pages/observability.html, pages/operator_organ.html, pages/pricing.html, pages/run-all.html, pages/sdk.html, pages/security.html, pages/status.html, pages/substrate.html, pages/superpowers.html, pages/throne-room.html, pages/throne-room.js, pages/uds.html, pages/upgrades.html, pages/wallpa.html, pages/warhacker.html, pages/wasi-rikuq.html, pages/wires.html, static/a11oy_cathedral.js
Deleted (gone from GitHub main): (none)
Keeps the served front-door (pages/*.html, console/*.html) identical
to GitHub main so an HF factory rebuild never drops a GitHub edit or
keeps serving a page that was deleted on GitHub.
- pages/console.html +8 -6
|
@@ -10248,10 +10248,10 @@ window.warboard_init=warboard_init; window.warboard_all=warboard_all;
|
|
| 10248 |
function reg(){
|
| 10249 |
var V=window.VIEWS; if(!V){ return setTimeout(reg,80); }
|
| 10250 |
var BR='sampler-putnam-10';
|
| 10251 |
-
var SHA='
|
| 10252 |
-
var SHORT='
|
| 10253 |
-
var COMPUTED='2026-06-
|
| 10254 |
-
var RUN='https://github.com/szl-holdings/lutar-lean/actions/runs/
|
| 10255 |
var TREE='https://github.com/szl-holdings/lutar-lean/tree/'+BR+'/Lutar/Putnam/Sampler';
|
| 10256 |
var BASE='https://github.com/szl-holdings/lutar-lean/blob/'+SHA+'/Lutar/Putnam/Sampler/';
|
| 10257 |
var TEAL='#3ddc97', GOLD='#c9b787', DIM='#8a8f98', WARN='#e0a82e';
|
|
@@ -10266,7 +10266,7 @@ window.warboard_init=warboard_init; window.warboard_all=warboard_all;
|
|
| 10266 |
['P06','P06.lean','Combinatorics \u2014 coin-flip parity invariant (PDF statement was incomplete; faithful restatement proven).',''],
|
| 10267 |
['P07','P07.lean','Analysis \u2014 partial harmonic sum dominates the logarithm.',''],
|
| 10268 |
['P08','P08.lean','Geometry \u2014 parallelogram law in \u211d\u207f.',''],
|
| 10269 |
-
['P09','P09.lean','Polynomial FE p(x)\u00b2=p(x\u00b2) \u2014
|
| 10270 |
['P10','P10.lean','Combinatorics \u2014 pigeonhole on residues: among n+1 integers, two differ by a multiple of n.','']
|
| 10271 |
];
|
| 10272 |
var nGREEN=PROBS.length;
|
|
@@ -10314,7 +10314,9 @@ window.warboard_init=warboard_init; window.warboard_all=warboard_all;
|
|
| 10314 |
+'kernel-checked counterexample (<code>p09_original_refuted</code>) rather than fabricating a proof \u2014 the same way '
|
| 10315 |
+'\u039b-uniqueness is surfaced as machine-FALSE (Conjecture\u00a01). We then prove the <b>faithful impossibility</b> the '
|
| 10316 |
+'equation actually implies: it forces p(1)\u2208{0,1}, so there is no such polynomial with p(1)=2 (<code>p09</code>). '
|
| 10317 |
-
+'Both are kernel-checked, sorry-free.
|
|
|
|
|
|
|
| 10318 |
H+='<div style="font-size:11px;color:var(--dim,#8a8f98);margin-top:14px;line-height:1.6;">'
|
| 10319 |
+'No fabricated proofs. Every row links to its exact source file at the verified commit; the headline count equals the '
|
| 10320 |
+'CI kernel run exactly. To promote the pack into the main numbers it must land on lutar-lean main and pass the v11 drift gate.</div>';
|
|
|
|
| 10248 |
function reg(){
|
| 10249 |
var V=window.VIEWS; if(!V){ return setTimeout(reg,80); }
|
| 10250 |
var BR='sampler-putnam-10';
|
| 10251 |
+
var SHA='b0d0f1b929542d1888b6e2897b2584b20e2bed26';
|
| 10252 |
+
var SHORT='b0d0f1b';
|
| 10253 |
+
var COMPUTED='2026-06-11';
|
| 10254 |
+
var RUN='https://github.com/szl-holdings/lutar-lean/actions/runs/27321295283';
|
| 10255 |
var TREE='https://github.com/szl-holdings/lutar-lean/tree/'+BR+'/Lutar/Putnam/Sampler';
|
| 10256 |
var BASE='https://github.com/szl-holdings/lutar-lean/blob/'+SHA+'/Lutar/Putnam/Sampler/';
|
| 10257 |
var TEAL='#3ddc97', GOLD='#c9b787', DIM='#8a8f98', WARN='#e0a82e';
|
|
|
|
| 10266 |
['P06','P06.lean','Combinatorics \u2014 coin-flip parity invariant (PDF statement was incomplete; faithful restatement proven).',''],
|
| 10267 |
['P07','P07.lean','Analysis \u2014 partial harmonic sum dominates the logarithm.',''],
|
| 10268 |
['P08','P08.lean','Geometry \u2014 parallelogram law in \u211d\u207f.',''],
|
| 10269 |
+
['P09','P09.lean','Polynomial FE p(x)\u00b2=p(x\u00b2) \u2014 full classification: solutions are exactly {0}\u222a{X\u207f}. See honesty note below.','NEW \u00b7 was OPEN \u00b7 CLASSIFIED'],
|
| 10270 |
['P10','P10.lean','Combinatorics \u2014 pigeonhole on residues: among n+1 integers, two differ by a multiple of n.','']
|
| 10271 |
];
|
| 10272 |
var nGREEN=PROBS.length;
|
|
|
|
| 10314 |
+'kernel-checked counterexample (<code>p09_original_refuted</code>) rather than fabricating a proof \u2014 the same way '
|
| 10315 |
+'\u039b-uniqueness is surfaced as machine-FALSE (Conjecture\u00a01). We then prove the <b>faithful impossibility</b> the '
|
| 10316 |
+'equation actually implies: it forces p(1)\u2208{0,1}, so there is no such polynomial with p(1)=2 (<code>p09</code>). '
|
| 10317 |
+
+'Both are kernel-checked, sorry-free. The full characterization is now itself a kernel-checked theorem '
|
| 10318 |
+
+'(<code>p09_classification</code>): over \u211d[X], p(x)\u00b2=p(x\u00b2) holds for all x <b>iff</b> p=0 or p=X\u207f for some n\u22650 \u2014 '
|
| 10319 |
+
+'turning the earlier \u201crefute + restate\u201d into the complete result.</div>';
|
| 10320 |
H+='<div style="font-size:11px;color:var(--dim,#8a8f98);margin-top:14px;line-height:1.6;">'
|
| 10321 |
+'No fabricated proofs. Every row links to its exact source file at the verified commit; the headline count equals the '
|
| 10322 |
+'CI kernel run exactly. To promote the pack into the main numbers it must land on lutar-lean main and pass the v11 drift gate.</div>';
|