Commit graph

2 commits

Author SHA1 Message Date
openresearch
e5cecac388 docs: update test matrix — C1 FAIL, C2 PARTIAL (HCMR builds, rest fail)
Lake build results (run 019f2f3f, 24min, 8 vCPUs):
- HCMR.lean: BUILT  (agent fix worked — removed excess omega,
  downgraded false theorem from > to ≥)
- CacheSieve.lean: FAILED  (agent fix incomplete — still has errors)
- Blitter6502OISC.lean: FAILED  (type class synthesis L62,
  rewrite failures L135/L142)
- YangMillsPerformance.lean: FAILED  (10 errors — omega/linarith
  can't handle Nat.div, 1 sorry)
- WorkloadTestbench.lean: NOT REACHED (depends on failed CacheSieve)
- CRTSidonN.lean: FAILED  (errors after agent fix)

Root causes:
- YangMills: proofs use omega/linarith for Nat.div goals (wrong tactic)
- Blitter: type class instance missing, rw patterns don't match
- CacheSieve: agent fix didn't fully resolve all issues
- CRTSidonN: compilation errors remain

For future builds: add 'lake exe cache get' before 'lake build' to
download precompiled Mathlib oleans (saves ~20min).
2026-07-04 22:55:02 +00:00
openresearch
209a66a98e docs(research): complete test matrix — 42 tests, every assumption
Good science tests all assumptions and answers all questions that can
be answered. 42 tests across 9 categories:

- CRT Encode Engine (T01-T06): preserve? create? redundant? scale? cost?
- Chiral System (T07-T11): drift varies? Kelvin exists? position-invariant?
- Sidon Filter (T12-T15): sufficient? differs from quaternion? breaks?
- COUCH Gate (T16-T19): rejects Kelvin? necessary? QUBO correlation?
- HCMR (T20-T22): measured or assumed? self-loop=collision?
- Hoffman (T23-T25): gap=1 universal? tight for regular? WW better?
- q-Profile (T26-T28): robust? q=1 always degenerate? encoding or selection?
- Conservation (T29-T30): always bounded? filtering avoids bound?
- Pipeline (T31-T34): reduces space? each stage needed? GPU works?
- Lean (T35-T38): compiles? non-tautological? native_decide?
- QUBO/QAOA (T39-T42): COUCH predicts? golden angle helps? gates used?

Each test: question → input → prediction → receipt → rejection.
DONE: 13 tests completed. PENDING: 29 tests to run.
No test skipped. No result assumed.
2026-07-04 21:34:17 +00:00