feat(proof-complexity): bound canonical oracle openings

[windsornguyen]

Establishes a Lean-checked semantic and resource boundary for canonical-oracle opening, then proves that the direct sparse-checksum/local-slice construction cannot achieve the target compression. No issue is currently tracking this research milestone.

What does this change?

This adds exact canonical-opening interfaces, composition theorems for one, two, and arbitrary well-founded adaptive oracle-query paths, and conservative pathwise resource accounting.

The principal verified results are:

• Exact opening preserves perfect acceptance for every well-founded adaptive verifier. The strategy type fixes oracle answers before later opening challenges, excluding challenge-dependent answers by construction.
• If the original verifier fits budget B0, each opening fits budget B, and an execution asks q queries, every tracked resource is bounded by B0 + q * B.
• A full-slice tensor opening has exact false descent but hits a product barrier. Any fixed number of plain local-slice rounds fails to compress mass 2^(m^2) to 2^O(m) at sufficiently large m.
• A radius-one linear checksum must touch every input coordinate. Consequently, a checksum cannot simultaneously have 2^O(m) rows and 2^O(m) row support while covering 2^(m^2) coordinates.
• Exhaustive Lean evaluation over three-bit binary words finds no valid radius-one checksum with zero or one row and exactly six with two rows; every one-row matrix has a retained collision certificate.

This is not a proof that P != NP. It rules out a broad but restricted grammar: sparse linear syndromes followed by local row opening, including any fixed-round rearrangement of ordinary slices. A surviving de-oraclization construction must add genuine far-case proximity machinery or an algebraic way to open dense checksum symbols.

The PR is larger than the repository's usual 200-line target because the result is one dependency-closed theorem chain: semantic composition, resource accounting, executable finite counterexamples, and the two barrier theorems. Each module remains focused and below the 500-line file limit. The included research notes audit the Athamnah-Ron-Zewi-Rothblum oracle layers and state the evidentiary boundary explicitly.

How was it tested?

• lake build --wfail passes (1,696 jobs from a fresh origin/main worktree)
• lake lint passes
• No sorry or new axioms, or this PR does not change Lean proofs
• git diff --check origin/main..HEAD passes
• Local, remote, and PR head resolve to commit ce2639039e288b439276d73febcb9def19bccb42