Skip to content

Conjecture 3 Progress Audit - 2026-03-31 (Update 7)

Executive Verdict

Minimal-target closure remains stable. This round sharpens the connected-regime frontier further: the selected-OR gadget is now proven nonexpressible as a hidden-vertex binary-submodular function for any auxiliary budget, but that obstruction is currently quotient-level and does not yet lift to a whole-family nonexpressibility theorem for the connected multi-parallel-circuit class. Net effect: stronger obstruction precision, yet full Conjecture 3 closure remains open.

Contract Checklist

  • Full two-sided Conjecture-3 inequality in the general contract remains open.
  • Minimal static-2D lower-bound target remains closed at theorem level in the map.
  • Compiler-native routing interpretation bridge remains the dominant unresolved step.
  • Threshold-consequence integration at full contract level remains partial.

Gap Matrix

  1. Obligation: Lower-bound side lift to full compiler-native CD interpretation.
  2. Current best support: generator-invariant stabilizer cut-rank functional, SWAP-only service lower bound, connected chi>=3 test family, and a theorem-level nonexpressibility result for the selected-OR selector in the compressed route.
  3. Missing bridge: either (i) lift the selector obstruction to a whole-family nonexpressibility theorem, or (ii) construct a genuinely global hidden-vertex realization of the connected family that bypasses the selector quotient; then connect either outcome to pivot-robust routing semantics.
  4. Risk: high.

  5. Horizon: medium.

  6. Obligation: Upper-bound side in full conjecture contract.

  7. Current best support: routing/separator machinery plus restricted-model tightness statements.
  8. Missing bridge: broad constructive compiler theorem achieving CD * polylog in the same formal model as the lower side.
  9. Risk: high.

  10. Horizon: medium-long.

  11. Obligation: Threshold-consequence integration.

  12. Current best support: 2D-local overhead/noise-consequence stack.
  13. Missing bridge: direct derivation of the contract-level delta_eff * CD criterion from a completed two-sided theorem.
  14. Risk: medium-high.

  15. Horizon: medium-long.

  16. Obligation: Linear balanced-cut intrinsic rank for targeted parity-check spaces.

  17. Current best support: decomposition/tangle/connected-set reductions remain strong and now better separated from low-order and quotient-level artifacts.
  18. Missing bridge: theorem forcing linear balanced-cut intrinsic rank under the final irreducibility assumptions.
  19. Risk: high.
  20. Horizon: medium-long.

Proof Readiness Scores

  • Minimal target proof readiness: 94-98
  • Full lower-bound side readiness: 71-82
  • Full upper-bound side readiness: 35-50
  • Full conjecture proof readiness overall: 59-69

Disproof Readiness Scores

  • Full disproof readiness: 23-38
  • Most plausible axis: promote selector-level impossibility into a family-level hidden-vertex nonexpressibility theorem in the connected chi>=3 regime.
  • Counterexample maturity: improved from update-6 because nonexpressibility is now unconditional for the selector itself (not only bounded-auxiliary search), but still incomplete for the full connected family.

What Actually Changed Since Last Check

  • Node graph increased from 133 to 136 markdown nodes.
  • New theorem-level deltas:
  • [[minimizing-hidden-binary-submodular-energy-preserves-submodularity.md]] establishes closure: minimizing hidden bits preserves visible submodularity;
  • [[selected-or-selector-is-not-hidden-vertex-graph-cut-expressible.md]] upgrades the selector bottleneck to a full nonexpressibility theorem (any auxiliary budget);
  • [[selector-quotient-is-not-a-submodular-minor-of-connected-family.md]] clarifies why this does not automatically imply whole-family nonexpressibility (quotient map is not closure-preserving as a minor operation).
  • Net effect: the natural compressed-state positive route is closed decisively, but the whole-family status remains unresolved and now demands a more global positive or negative argument.

Highest-Leverage Next 3 Moves

  1. Prove or refute liftability: establish a theorem that either transfers selector nonexpressibility to the full connected family or proves such transfer impossible under current closure tools.
  2. Attempt a global constructive bypass: search for hidden-vertex realizations of the connected family that do not factor through (u,C,D)-style quotient compression.
  3. Keep compiler-native closure aligned: whichever side wins (global realization or family-level obstruction), tie it to pivot-robust routing/load semantics needed for the CD(T_n,G) lower-bound interpretation.