Solving & proof
Checked progress
Specialists propose deductions with evidence. The checker authorizes changes to the Sudoku state. A promising prediction never becomes a truth rule.
From architecture to executable laboratory
Built to solve, explain and survive a long run.
R6 brings multiple representations and a proof-checking runtime into one arena. HF3 adds matched causal controls, reliable recovery and terminal learning. The HF1 hotfix delivers the new long-campaign orchestration, Windows launch fixes and a compact local program package.
Recovery & memory
Continue without learning twice
Compact checkpoints preserve progress. Resume and completed-run no-op checks protect the learning record from duplicate terminal updates.
Local operation
See what is happening
One status line shows the time, stage, completed work and approximate ETA. FAST LIVE exports a verifiable snapshot while the experiment continues.
The program distribution is about 2.8 MB and contains 214 files: code, launchers, tests and required local data. Historical campaign archives are excluded.
Why R6 exists
Give the governor something qualitatively different to govern.
The HF3 pilot confirmed that strong classical strategies remain serious competitors. R6 gives the controller a richer choice: change the mathematical view, select a specialist or use ordinary search. The arena records the cost of that choice so a more elaborate method has to earn its place.
Representation
Multi-Representation Ecology
Evaluate method × representation × scale × state regime, not a single scalar leaderboard.
Compression
Proof Codec
MDL is attached to an actually encoded proof or choice stream with a decoder and verification cost.
Memory
Proof Atlas
Convert expensive verified discovery into a compact macro plus a cheap matcher that can be reused later.
Control
DCC Representation Governor
Choose whether to continue, switch view, change scale, fund a specialist, or do nothing beyond baseline work.
Product
Game Review
Evaluate actual player actions using verifiable explanations and a frozen reference proof language.
Distillation
Standalone destination
The Python arena tests mechanisms before browser integration. The playable web app keeps its own Logic/Trace engine; HF3 is not silently substituted into the game.
Core loop
Fund first. Then let the specialist work.
R6 explicitly charges representation construction, feature extraction, failed proposals, checking, learning and persistence. Views are not built for free before selection.
Verified Stategivens, domains, committed history
8z Forgeview/work descriptors, Atlas entries
MDLmodel + proof + library economics
DCC / controlcontinue, switch, scale, budget
X specialistpaid execution or continuation
Checkerverified effect or explicit no-effect/limit
Atlas / Productexperience, generator, review, distillation
1 · Decide where to work
Prediction and allocation
MDL models predict which work may pay off. DCC adjusts allocation using feedback. Both operate within a declared work budget.
2 · Establish what is true
A separate authority
A specialist supplies a proof or an exact search result. Independent checks validate deductions and completed grids; an exhausted budget remains an explicit limit.
3 · Keep useful experience
Proof and learning
Verified proof patterns can enter the Atlas. Learning updates are recorded once, with the cost of matching, checking and persistence included.
“Rank, Don’t Eliminate”: a weak method in one representation can become a strong specialist when a new lens creates the right niche.
First specialist families
Three mathematical lenses, with classical search anchors.
A · algebra
AIS / Digit Balance
Compile bounded count and linear relations into exact certificates, then distil recurring relations into Atlas matchers.
B · 729-space
CubeLift
Lift Sudoku into a 9×9×9 candidate cube with cell, row–digit, column–digit and box–digit projections.
C · geometry
Geometric Path-MDL
Use exact single-digit path structure, PATH_DAG queries, joint GLOBAL9 models and paid branch-ranking experiments.
Main causal anchors
Seeded MRV + Luby restarts
The new long experiment includes strong classical search strategies. The arena also implements an Algorithm X exact-cover reference using copied sets. Dancing-links DLX and certified SAT/CDCL remain reference targets from the earlier architecture, not delivered long-study arms.
Digit-Path research
From a visual seed to exact objects and falsifiable tests.
Connecting equal digits across rows first looked like a picture. R6 turns that picture into a concrete family of representations with explicit codecs, exact queries and causal branch-ordering tests.
46,656valid single-digit patterns
6⁶PATH6 factorization into six S₃ choices
9coupled digit paths in GLOBAL9
T0→T3correctness → diagnostic → prediction → causal search
Pattern → Path → Exact queries → Joint codec → Predictive signal → Causal search
PATH6Exact bijection for the 46,656 single-digit pattern space. A fixed 16-bit index is a codec, not yet a ranker.
PATH_DAGCount feasible paths and cell support without enumerating every full pattern when a dynamic program can answer the query directly.
PATH_COVERCompose compatible digit patterns as a macro exact-cover view; distinguish exact compatibility from geometric scoring.
GLOBAL9Model all nine paths jointly. It can be tested even if single-digit PATH6 has no useful marginal signal.
G_coupling = L_independent(Y | D) − L_joint(Y | D), with model/codebook/library/framing costs charged on both sides.
Shorter path description is not a truth rule. It becomes useful only if it predicts or causally improves verified search under matched cost and information.
Proof economy
Discovery only matters if it becomes cheaper next time.
Proof codec
Bits with a decoder
Reference proof bits are meaningful only inside a frozen proof language and codebook. Runtime, library cost and decoder work remain visible.
Atlas
Matcher cost matters
A beautiful macro that is expensive to recognize may compress storage without reducing solving work. R6 measures both.
Symmetry
Canonical schemas
Atlas entries are canonicalized across declared Sudoku symmetries so the library does not fill with equivalent positional copies.
Negative knowledge
Nogoods + Negative Atlas
Store verified forbidden combinations separately from completed “nothing found” scans; both retain exact scope and dependency conditions.
Forge economics
Search for views is not free
Representation/program search, compilation, canonicalization, failed candidates and maintenance are included in the system account.
Marginal value
Who survives distillation?
Measure value with ablation and replacement-aware contribution, not just isolated leaderboard rank or editorial enthusiasm.
The new long experiment
Separate prediction, allocation and experience.
The HF3 HF1 long launcher runs a frozen causal design with fresh development seeds.
It compares the same puzzles and declared checkpoint/service contract, then asks separately whether
training helps on unseen evaluation puzzles. This is a development experiment with protected=false.
COLD · eight main arms
Where does a gain come from?
Combined MDL + DCC; DCC with the same actuator; a constant predictor with the matched actuator; MDL with a fixed schedule; Sticky; Structural; seeded MRV; and Luby restarts.
Transfer · three learned arms
Does earlier work help later?
Train sequentially with ONLINE_PREQUENTIAL, then freeze learning. Compare fresh and trained states on the same EVAL puzzles. Training and evaluation are separated under the declared identity and symmetry checks.
Matched contract
Two puzzle profiles
UNIQUE_28 and UNIQUE_24 use 28 and 24 givens. Main comparisons share the 24-million-WU budget and compact checkpoint/service settings. Fewer givens alone do not certify greater human difficulty.
Bounded diagnostic
Context UCB has a smaller role
Context UCB runs on every fourth qualified evaluation puzzle. Its earlier service-finalization limits can be investigated without making it half the experiment.
Frozen study scope and exact policy names
MDL_DCC, DCC_ONLY_SAME_ACTUATOR, CONST_PRED_MATCHED_ACTUATOR, MDL_ONLY_FIXED_SCHEDULE, STICKY, STRUCTURAL, SEEDED_MRV, LUBY_RESTART.
The design requests 64 TRAIN and 64 EVAL puzzles in each profile: 256 generation requests, 36 study cells and at most 2,208 solving tasks after qualification. Failed generation requests are recorded without replacement. The 48-hour cumulative admission ceiling is a limit, not an ETA.
The main long study uses the CORE action set. Deliberate AIS, PATH, Cube and Atlas activation is tested separately in specialist screens; their presence in the arena does not imply activation in every long-run task.
Delivery and next steps
A working instrument, with the next questions exposed.
BUILT
Proof, recovery and specialist runtime
Checked deductions, proof replay, Atlas mechanisms, compact checkpoints, FAST LIVE and bounded specialist tests are executable.
HF1
Windows and experiment orchestration
Windows path and quoting fixes, a new causal launcher, status, stop, resume and verified live extracts. The old two-arm night launcher is labeled as a legacy engineering soak.
STUDY
Causal and frozen-transfer comparisons
The local Windows run has started. The first reviewed extract covers puzzle qualification; comparative solving results remain pending.
NEXT
Evidence-led browser integration
Promote mechanisms only after measured value, browser parity and acceptable size/runtime cost. Human learning benefit requires its own evaluation.
Product destination
The game stays focused on the player.
The current browser game lets you play, request hints and compare strategies. R6 runs as a separate Python research arena. The product direction is a compact browser experience with checked explanations, review of actual moves and useful next exercises. This page update documents the new arena; it does not install the Python specialists into the browser game.
Player mode
Quiet by default
The grid stays central. Proof and research machinery surface only when the player asks for help or review.
Laboratory mode
Inspectable when needed
Expose proof bits, work units, representations, DCC decisions and replay for research and advanced users.
Evidence · final bounded cut verified 12–13 September 2026
Engineering acceptance passed. Scientific superiority remains open.
The bounded HF4 acceptance chain is complete and internally consistent. It validates the arena, proofs and pilot orchestration; it does not substitute for the separate long scientific campaign, which was not started.
| Evidence | Observed result | Scope |
|---|---|---|
| HF4 bounded master | 5/5 PASS | Package, Windows/preflight, selftest, smoke and bounded pilot stages completed successfully. |
| Selftest + smoke | 444/444 assertions; 3 allowed SKIP · smoke 4/4 PASS | Engineering acceptance of the delivered arena; allowed skips are retained explicitly rather than hidden. |
| P1 / P2 / P3 pilots | PASS · 467 unique runtime tasks = 335 SOLVED + 132 LIMIT | One bounded development experiment. These counts are not an independent scientific replication. |
| Scientific status | Long campaign executions 0 · scientific_final=false | Semantic proof replay is NOT_RUN; no representation, MDL or DCC superiority is promoted from this cut. |
The earlier main P1 comparison remains an important negative control: MDL_DCC solved no more puzzles than the matched constant-predictor actuator and cost about 37.8% more WU; Seeded MRV and Luby restarts were cheaper. The final bounded acceptance does not reverse that result.
Exact artifact identities and evidence provenance
Final bounded live extract: HF3_ALL_LIVE_1789236581472973300.zip · 13,722,495 bytes · 3,021 members.
Final extract SHA-256:e1c5b282beaa0ef14a7ff15cc166852ca5e05c9ef459f9521243ca99f42a2b5f
The included verifier returned VERIFIED; its manifest SHA3-256 is 722125503ce7c1e918eab328082c2d7088ae9dd7d947667db4dba58955fb0ace.
Release receipt retained for lineage: AI8_Sudoku_R6_Program_v0_2_0_R1_HF3_HF1.zip · 2,765,694 bytes · 214 members.
Earlier qualification snapshot retained for history: HF3_LONG_FAST_LIVE_1789073761629256000.zip. The final bounded extract above supersedes it for current status.
Final bounded public evidence receipt ↗
Earlier R3L1 evidence, preserved under its original version ↗
No magical score
Bits, WU, CPU, solved rate, proof coverage and human learning are different quantities. They are not merged post hoc.
Strong baselines
Seeded MRV, Luby restarts, fixed and structural policies, matched predictor/actuator controls and bounded Context UCB diagnostics make the comparisons explicit.
10% has a denominator
Any “10% better” claim must name the task profile, comparator, quality gate, total account and uncertainty rule beforehand.