Circuit-SETH GET / Companion 01
A guided tour of the research environment: what each system proposes, how the pieces connect, and what evidence would make the next step meaningful.
Research scaffold · implementations openThe folder structure, source archive and scaffold validator exist. Compiler passes, five experiments, proof files and seven automated theorem guardrails are placeholders. These pages explain the proposal; they do not execute the Python pipeline or establish a Circuit-SETH result.
The supplied explorer is preserved unchanged and loads Tailwind, fonts and KaTeX from external services. Its formulas and status labels reflect the source document. Use this companion for the repository’s implementation status.
01 / The research question
Circuit-SAT asks whether an assignment makes a Boolean circuit accept. The proposal investigates whether special geometric circuit families admit a verifiable encoding that removes some branching. Extending a result to arbitrary bounded-depth circuits requires a separate argument.
02 / Four proposed systems
PASS 01 / OPEN
Represent a three-dimensional point as X(x) = (x, ‖x‖²/2, 1). The lifted vector has zero norm under the specified indefinite bilinear form.
The proposed compiler would translate suitable constraints into sphere equations and examine exact dependencies. A general Boolean clause-to-sphere encoding and recoverable variable locking still require proofs.
pass1_twistor_null_cone.py ↗
PASS 02 / OPEN
An open chain of compatible increments can telescope to its endpoints. The three gears organize fine frames into aggregates.
Endpoint evaluation is useful only after the coboundary structure is established. Reading or validating the chain still costs work; constraints on intermediate states must survive. A cyclic product equal to one is not a closure test.
pass2_torsional_markov_pump.py ↗
PASS 03 / OPEN
Pair frame residues modulo 8 and modulo 3 to obtain a 24-frame schedule. Six handshake slots connect the proposed orbital channels.
The planned router combines tier transformations, D₃ symmetry and branch recovery. Single-erasure recovery needs a specified codec; two erasures are generally ambiguous. The proposed Form 3 layout conflicts with the existing local profile.
pass3_orbital_crt_router.py ↗
PASS 04 / OPEN
Use a graph walk to propose residual candidates, then check candidates with exact arithmetic and the original circuit.
A Ramanujan spectral gap concerns mixing, not a SAT-search speedup. The residual solver, graph construction and witness verifier are future implementations. Headers and residue checks alone are not general SAT certificates.
pass4_dual_helix_ramanujan.py ↗
03 / Try the ideas
These browser calculations are teaching aids. They are independent of the unimplemented research modules.
If a sound encoding could eliminate a fraction α of n Boolean decisions, exhaustive search over the remainder has base b = 2^(1 − α). This model excludes encoding and verification costs.
A slider value is an assumption, not a measurement of α_GET or evidence of asymptotic savings.Move through one joint schedule. Every pair (frame mod 8, frame mod 3) occurs once per cycle. Highlighted handshake slots satisfy frame mod 4 = 2.
04 / Inside the workspace
| Directory | Responsibility |
|---|---|
00_epistemic_specs/
|
Tags, C1–C5 proof obligations and obstruction audit plans. |
01_core_substrate/
|
Planned exact fields, rational rotations, CRT tracks and a separately specified tile adapter. |
02_circuit_seth_benchmarks/
|
Planned netlists, circuit families, planted cases and DIMACS intake. |
03_geometric_compiler_passes/
|
The four passes and master pipeline; all entry points currently raise NotImplementedError. |
04_use_case_experiments/
|
Five script skeletons; no experimental results recorded. |
05_proofs_and_monographs/
|
Open proof obligations and a draft registration, not an externally timestamped preregistration. |
tests/ contains planned research-test placeholders. validate_scaffold.py checks the 27 planned files’ existence, Python syntax and hashes of three archived uploads. It does not test the proposed algorithms.
05 / The experiment notebook
Sweep clause growth and measure certified eliminated variables. Compare against an explicit baseline and count all encoding costs; finite sizes cannot settle asymptotics.
Compare a reversible cascade’s serial product with its endpoint expression. Include non-coboundary and externally constrained intermediate states as negative controls.
Check single-branch recovery against original data. Treat any mismatch or silent acceptance of ambiguous two-branch loss as failure.
Compare graph-walk mixing with declared reference walks and separately measure witness finding. The filename mentions CDCL, but a solver configuration and fair CDCL protocol remain to be specified.
Measure encoding plus evaluation and verify every returned witness against the original circuit. One failing witness rejects correctness; finite successes do not prove polynomial runtime.
06 / Keep the evidence honest
These are the blueprint’s proposed checks associated with Theorems 5.1 and 5.14. Their automated implementations and the cited mathematical claims remain open to review.
07 / Reproduce the current state
From the repository root:
python3 ecosystem/experiments/circuit-seth-get-lab/validate_scaffold.py
make verify-all
The first command validates the scaffold. The second exercises the existing exact-arithmetic reference suite and golden vectors. A passing reference suite does not establish the proposed compiler’s correctness.
Next: specify a versioned codec, formalize one restricted circuit family, implement a pass with positive and adversarial fixtures, then register and run a bounded experiment. Promote a claim to COMPUTED only with reproducible evidence; PROVEN requires a mathematical proof.