[petalas]

Result

Scoped written proof with exhaustive finite corroboration. No κ change. This answers the first half of open question 1 of #6861 (research/p104-e8-subspace-invariants, DreamingOfClouds): a closed-form derivation of the ports-per-dimension law N_e = 2^(e-2) + 4 for 4 <= e <= 7 from the radical of B|V and the restriction of q to V, and the reason it stops at e = 8.

Setting of #6861: F2^9, q(x) = C(wt x, 2) mod 2 with polar form B, even hyperplane E, P120 the odd vectors with q = 1, N(V) the number of ports in a subspace V. For V of dimension e let R be the radical of B|V, rho = dim R, delta = 1 if the all-ones vector lies in V, q' = q + (wt mod 2), and sigma, sigma' the sums of (-1)^q and (-1)^q' over V.

1. Closed form. If V is not inside E: N(V) = 2^(e-2) + (sigma' - sigma)/4, with sigma^2 = 2^(e+rho) if q vanishes on R and 0 otherwise, and the same for sigma' and q'.
2. Constraints. e + rho <= 8 + 2 delta. If delta = 1 then sigma' = 0. If e + rho = 8 + 2 delta and q vanishes on R, then sigma = 2^(4 + delta) > 0.
3. Bound. N(V) <= 2^(e-2) + 4 for every subspace, with equality in exactly three radical classes, and N(V) <= 64 at e = 8.
4. Ports per dimension. N_e(S) <= min(2^(e-1), 2^(e-2) + 4) for every subset S of P120. P120 and P104 attain it at every e = 1..7 (1, 2, 4, 8, 12, 20, 36).

At e = 8, rho = 2 delta is forced, so every subspace sits at the cap of item 2 and has sigma >= 0; the bias is at most 0 and N_8 = 64, not 68. Item 3 also recovers the saturation depth of #6861 Theorem 1.

Claim types: items 1 to 3 and the upper bound in item 4 are written proofs (PROOF.md) that use two identities and no enumeration. Attainment in item 4 is a finite certificate: seven explicit bases checked by direct enumeration. The census over all subspaces is corroboration.

Evidence

• research/p104-e8-port-count-closed-form/PROOF.md: Theorems 1 to 3 and Corollary 4.
• verify.py visits all 8,283,458 subspaces of F2^9. On the 7,866,259 not inside E it computes N, sigma, sigma' and R and requires every clause. It recomputes the same invariants from first principles on 3,094 subspaces, checks the seven P104 witnesses, and runs five rejecting controls.
• CENSUS.json: the 98 classes (e, delta, rho, sign sigma, sign sigma', N) with sizes. Subspaces attaining 2^(e-2) + 4: 11,475 at e = 4, 107,100 at e = 5, 85,680 at e = 6, 5,440 at e = 7.

The N_e(P120) values and the maximizer counts at e = 1..4 (120, 7,140, 32,130, 11,475) agree with #6861 Theorems 2 and 1.

Reproduce

From the repository root, CPython 3.12, standard library only:

~/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/p104-e8-port-count-closed-form/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-e8-port-count-closed-form
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-e8-port-count-closed-form --check-source-history

Expected: PASS_P104_E8_PORT_COUNT_CLOSED_FORM, PASS_REGISTERED_RESEARCH_PACKAGE, PASS_RESEARCH_COMMIT_BYTES. Local results on macOS arm64, Python 3.12.15: all three pass; the verifier takes 19 s (registered timeout 300 s). It also passes with -O.

Limitations

• A statement about port sets only. No word, helper split, invoice or supplier; the selected frontier and the five framework assumptions are unchanged.
• The signs of sigma and sigma' are not expressed through rho alone; only the constraint at the radical cap is proved and used.
• For P104 the proof gives N_8 <= 64. The exact value 60 is Prove E8 subspace invariants of the P104 ports: saturation depth, port counts per dimension, and a star law for bicliques (no κ) #6861's exhaustive result and is not derived here.
• The flag-rectangle masses (second half of the same open question) and the star law are not addressed.
• No independent human review and no formal proof-kernel check.

Open next questions

1. Do the flag-rectangle maxima of Prove E8 subspace invariants of the P104 ports: saturation depth, port counts per dimension, and a star law for bicliques (no κ) #6861 Theorem 4 follow in closed form from the class table? The joint constraint between a hyperplane g of A and A^perp is not derived.
2. Does the star law max N(V) N(V^perp) = degree follow from the same classes?
3. Which property of the 16 ports removed from P120 forces N_8(P104) = 60 rather than 64?
4. For which punctures of P120 is the bound still attained at every e <= 7?

Related open work

• P104 port window is exactly 9 in characteristic 2 (no κ) #7114 (DreamingOfClouds): port window of P104 in characteristic 2. Same port set, different quantity; no number in common with this PR.

CI notes

CI did not certify this package. At head 7e4e01a281afa5c76930f6a211b381c653912d75, run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/42905806694:

• plan failed in the "Onboarding helper tests" step: 760 tests ran, 1 failed, 24 skipped. The failing test is test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record, with AssertionError: '`make frontier7000-verify`' not found in '# CI verification ... Current selected-family replay: #6030 ...'.
• replay was skipped because plan failed, so the registered package command did not run in CI. The evidence for this package is the local run recorded under Reproduce.

Cause, as read from the job log and from main at e54523517: certificates/selected-result.json gives "reproduce": "make frontier7000-verify", while docs/ci-verification.md still has the heading "Current selected-family replay: #6030" and does not contain that command. The test compares those two files. This PR touches neither; it adds only research/p104-e8-port-count-closed-form/.

The same single test is the only failure (760 run, 1 failed, 24 skipped) in four other pull-request runs checked today: 42905094314 (research/kappa-response-7123), 42903313790 (research/kappa-recharted-003641239650184), 42905202459 (#7125) and 42905330981 (#7126). No fix or retrigger commit was pushed here.