research: r=1 bounded-summary non-compression witness for the cut network

[LightChainr]

Purpose

Advance the cut-network / predictive-state paper by one exact, independently verified lemma: a predeclared bounded summary that includes the complete safe-subset polynomial and the radius-1 terminal neighbourhood is not sufficient for a frozen depth-2 compositional language.

This is the minimality-up-to-summary test named as next PRIMARY in PR #549. It does not reopen the research DAG, add Monte Carlo, or enlarge the descriptor ladder.

Dependency PRs (read-only, not stacked): #491 cut-network theorem, #549 parallel-gadget lower bound, #435 survival-law no-go. This branch is additive from current main.

Verdict

Manuscript token: BOUNDED_SUMMARY_INSUFFICIENT

Frozen search-protocol token (locked before search, not rewritten): NO_COMPRESSION_WITNESS_FOUND. Same mathematical outcome.

Primary pair: n=7 planar two-terminal vertex-networks, identical

S(z) = 1 + 7z + 21z² + 35z³ + 33z⁴ + 15z⁵ + 2z⁶
H2 = b2 = 0
r=1 neighbourhood (unique L-port, unique R-port, no L–R edge)

first split on frozen experiment E2_c2:

P(A) = 937/1050
P(B) = 313/350
gap  = 1/525

Delayed-fork E1_c1 equals 1 on both graphs, so this is independent of the PR #549 successor-second-moment mechanism. Radius-2 neighbourhoods of this pair differ, so the lemma is r=1 only. The n=7 pair is the smallest witness found in the declared enumerated families, not a claimed global minimum among all plane two-terminal vertex-networks.

Census (contract limits)

Declared families were exhausted to the frozen n≤12 bounds:

family	size	r=1 splits
exhaustive n≤5	7398	0 (also closed at r=2)
hidden hop grid, 9 combinations	66582	1 (L1R1 = primary witness)
series-parallel n≤12	295654	330 (smallest found there at n=8)
Wheatstone+SP / multipath / grids	858	0

HID r=2 is closed on all nine hop combinations. SP n=11 and n=12 unique generation is included (59324 + 212771 graphs).

Analysis notes completed with this PR

• A. Cut dependence: CUTS_LAW_EQUIVALENT_NOT_ISOMORPHIC. Alternate admissible occupied cuts preserve pair/triple event sets and the future connecting-subset family; they need not be isomorphic as rooted networks. Finite examples: N16 cut reversal; two occupied-cycle searches on each saved N425 checkpoint. The network is a proof device in a fixed-cut gauge, not a physical angular mark.
• B. Embedding: GENERAL_REALIZATION_LEMMA. A new general lemma (notes/p1-plane-tt-realization-lemma-20260902.md) constructs, for every finite plane two-terminal vertex-network with cofacial terminals and no terminal edge, a finite honestly embedded torus host and a rank-one occupied essential cycle whose residual cut-network recovers the network. The n=7 pair only needs the hypotheses. Parallel-gadget §6 is not a surjectivity proof (it embeds k copies of two already-realised N16 gadgets). The cut-network theorem is the opposite direction. No named square-HNF occupation of the n=7 pair is constructed.
• C. Theorem scope: notes/p1-theorem-scope-skeleton.md filled without Issue/PR numbers as hypotheses. Cut-network minimality remains UNRESOLVED.
• Claim-wording erratum: notes/p429-r1-claim-wording-erratum-20260902.md.

Files

• research/summary_search/ — exact fractions.Fraction library, search-independent hard-coded witness verifier (same stdlib primitives; not a fully independent implementation), census generators
• tests/test_p429_r1_noncompression_witness.py
• results/p429-r1-bounded-summary/ — machine JSON, markdown census, metadata
• notes/p429-r1-noncompression-certificate-20260902.md
• notes/p429-r1-search-contract-20260902.md — frozen contract (protocol tokens locked; provenance header only)
• notes/p429-r1-claim-boundary-20260902.md
• notes/p429-r1-claim-wording-erratum-20260902.md
• notes/p1-cut-dependence-20260902.md
• notes/p1-plane-tt-realization-lemma-20260902.md — new general realization lemma + proof
• notes/p1-n7-torus-embedding-20260902.md — hypothesis check for the n=7 pair
• notes/p1-theorem-scope-skeleton.md

No docs/STATUS.md, ROADMAP, claim-ledger, production source, or Issue lifecycle change.

Claim boundary

Proves failure of (S(z), n, H2, b2, r=1 neighbourhood) on the declared finite class. Does not prove: r=2 failure; Euclidean dimension lower bound; scalar-encoding impossibility; continuum/CFT statements; minimality of the full cut network (UNRESOLVED); the same split for every HNF square-site torus; global n-minimality among all plane two-terminal networks.

Proposed claim level: C5 for the finite two-terminal statement and for the realization lemma; C1 for the search-independent hard-coded witness verifier (not a fully independent implementation).

Checks

python3 research/summary_search/bounded_summary_search.py
python3 research/summary_search/verify_witness.py
python3 -m unittest tests/test_p429_r1_noncompression_witness.py -v

Expected: self-checks passed, VERIFY_OK, S (1, 7, 21, 35, 33, 15, 2, 0), E2_c2 937/1050 vs 313/350, gap 1/525. All four unit tests pass.

Stop rule

No larger parallel products, no new descriptors, no further SP census as a default. Next useful step after this PR is manuscript mode for P1, not another search class.

No main write, auto-merge, Issue lifecycle change, or production authorization.