Lesson 01 - Frontier Status and How to Read the Spine¶
Goal¶
Learn the current Conjecture 3 map as a live proof frontier, not as a list of topics. The key habit is to separate:
- theorem-backed statements;
- chosen-presentation arguments;
- presentation-invariant arguments;
- compiler-native reformulations;
- open gaps.
Prerequisites And Diagnostic Checks¶
Before starting, answer these quickly.
- What does it mean for a QLDPC family to have bounded-weight checks and bounded qubit degree?
- Why does an expander-like Tanner graph create large balanced cuts?
- Why does a near-square 2D grid have only \(O(\sqrt n)\) bisection width?
- What is the difference between a stabilizer code and a choice of stabilizer generators?
- Why would a SWAP-only compiler suggest a routing-style lower bound?
If 1-3 are weak, return to the foundations lessons on QLDPC, expansion, and grids. If 4-5 are weak, continue but slow down in Lessons 04 and 05.
Concrete Motivation From The Research Map¶
The first version of the research instinct is:
Expander-style QLDPC checks want nonlocal communication, but static 2D hardware has narrow separators.
That intuition is correct but too coarse for the current frontier. The local graph now says something sharper:
- the minimal static 2D lower bound is already solved for theorem-level Quantum Tanner families;
- the chosen-presentation expansion route is also strong and useful;
- the remaining problem is to say the same phenomenon in a compiler-native
CD(T_n,G)language that does not depend on a fragile generator presentation or false token-crossing picture.
So the frontier is not simply "prove a 2D lower bound." It is:
identify the right intrinsic demand object for a stabilizer family and the right compiler meaning for that object.
Worked Example Before Abstraction¶
Suppose a code has \(n\) qubits and an expanding Tanner graph. A balanced cut of the qubits has \(\Omega(n)\) check incidences crossing it. A near-square 2D grid has only \(O(\sqrt n)\) physical edges crossing a balanced geometric separator.
A naive depth argument says:
- many checks need to communicate across the logical cut;
- few hardware edges cross the physical separator per time step;
- depth must be at least \(\Omega(n/\sqrt n)=\Omega(\sqrt n)\).
That is the right shape, but three questions now matter.
- Are the crossing objects real stabilizer demands, or artifacts of one generator set?
- Does "crossing" mean a qubit token must traverse the separator?
- Can the demand be represented by ordinary graph cuts, paths, or packets?
The current graph answers:
- stabilizer cut rank is the generator-invariant demand;
- token crossing is false, but cut-edge service survives in the SWAP-only model;
- ordinary graph-cut semantics fail in general, so the canonical object is currently submodular rather than classical-routing.
Formal Map¶
The course uses two files as the default entrypoint:
The current research state can be compressed as follows.
Established Theorem Layer¶
The minimal static 2D target is solved for theorem-level Quantum Tanner families:
- 2d-syndrome-depth-from-code-parameters.md
- quantum-tanner-good-family-presentation-invariant-2d-barrier.md
- weighted-separator-function-to-syndrome-depth.md
Chosen-Presentation Mechanism Layer¶
The local-expander route explains the cut mechanism:
Intrinsic Demand Layer¶
The invariant object is stabilizer cut rank:
- cross-cut-stabilizer-rank.md
- cross-cut-stabilizer-rank-rank-formula.md
- stabilizer-cut-rank-functional.md
Compiler-Native Layer¶
The current compiler-side replacement for naive routing is submodular cut congestion:
- stabilizer-cut-rank-defines-canonical-submodular-cd-object.md
- submodular-cut-congestion-lower-bounds-swap-only-compiler-depth.md
Open Frontier Layer¶
The strongest open targets are:
- explicit deterministic component-code packaging;
- linear balanced cut rank in the chosen Quantum Tanner presentation;
- dense original-matroid connectivity, especially dense tangle breadth;
- meaningful
CD(T_n,G)semantics beyond the settled submodular cut-functional formulation.
Conjecture Linkage¶
This lesson sets the correct target. For Conjecture 3, do not ask:
Can we prove QLDPC codes are hard on a 2D grid?
Ask:
Which exact model, family, presentation, and demand object are we proving hardness for?
The local graph already answers the static 2D version in a strong way. The live frontier concerns the route from that theorem to a robust compiler-native statement.
What This Does And Does Not Prove¶
This lesson proves nothing new. It is an orientation layer.
It does establish the working distinction for the rest of the course:
- established theorem: safe to use as a proof input;
- chosen-presentation theorem: useful but may not be invariant under generator changes;
- inferred bridge: plausible and graph-supported, but not a theorem unless a node says so;
- open gap: should not be taught as fact.
Active Recall¶
- State the minimal static 2D theorem target in one sentence.
- Why is that not the whole Conjecture 3 frontier anymore?
- What does stabilizer cut rank fix that raw crossing-generator counts do not?
- Why does a false token-crossing picture not kill the SWAP-only lower-bound route?
- What is the difference between submodular
CDand classical routingCD?
Next-Step Handoff¶
Next lesson: prove to yourself that the static 2D theorem is genuinely solved, and learn why the separator meta-theorem is stronger than just a square-grid argument.