Skip to content

Lower P104 frame-0 hosting from 40 to 14 monomials (no κ) - #7167

Open
petalas wants to merge 3 commits into
CrocSwap:mainfrom
petalas:research/w8-1110b-p104-frame-hosting-min
Open

petalas wants to merge 3 commits into
CrocSwap:mainfrom
petalas:research/w8-1110b-p104-frame-hosting-min

Conversation

@petalas

@petalas petalas commented Nov 11, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Finite certificates and a scoped written proof for P104 frame-indicator hosting in the simple-root chart. This answers open question 2 of unpaidmoon's #7047 and lowers frame 0's explicit monomial charge from 40 to 14. Affine terms are free, as in #7031/#7047. No κ, supplier admission or selected-frontier change.

frame 0 on all 120 root lines
  #7031 product of letters                         40 charged monomials
  exact minimum among functions of four forms      16
  exact minimum among degree-at-most-3 hosts        14, unique minimiser

The four-form minimum is attained by (1+x0)(1+x5)(1+x1+x2+x4+x6+x7). The 120 lines occupy 15 of the 16 four-form fibres, eight lines per attained fibre. Exactly two functions match the indicator; their charges are 40 and 16.

For all 15 odd 8-cliques of #7014, the package certifies the minima over translation-invariant hosts and over cubic hosts. It also supplies explicit hosts from a fixed-budget search. For the 13 P104 rows, the separate per-row charges total 225 on 120 lines and 211 on 104 lines, against the letter-product total 1126. These are independently chosen rows, not a joint minimum.

Lemma 1 proves the coset structure. Each row is F = a+W with dim W = 3; the 32 cosets contain one eight-line coset, 28 four-line cosets and three empty cosets. The three empty cosets and F form a+W^perp. Consequently there are eight invariant hosts and five containing-flat indicators on the 120-line scope. A three-flat parity certificate excludes degree-at-most-2 hosts for every row. The 104-line computations cover the 13 P104 rows.

This contribution was produced by Nick Petalas. Credit unpaidmoon for #7014, #7031, #7046 and #7047, and DreamingOfClouds for #6933's ports and line map. The source frame partition is retained byte-identically. Predecessor executables were not replayed.

Evidence

The complete local verification passes with CPython 3.12.15 on macOS arm64, standard library only, at head 1af08e33b84c603c8e68ea6b41232f197a31692f, canonical base e54523517d0f03e58352e647c403a5af3e525a57.

  • PASS_P104_FRAME_HOST_MINIMUM: four-form minimum 16, cubic minimum 14, 15 degree-two exclusions, five flat hosts per row, and separate-row totals 225 and 211.
  • All three registered checks pass. The normal verifier, isolated optimized verifier and generator smoke check were individually timed at 0.25, 0.26 and 0.17 seconds. These are check-budget records.
  • Both complete 3000-order seeded searches were rerun, taking 69.71 and 57.20 seconds. Every regenerated JSON entry equals its committed counterpart: 15 hosts on 120 lines and 13 on 104 lines.
  • PASS_REGISTERED_RESEARCH_PACKAGE, committed-byte/mode/source-history checks, official export integrity/input coverage, and Git-free normal/optimized exported replay pass.
  • A separate local Gaussian-elimination calculation agrees on all 28 row/scope combinations and the unique frame-0 cubic minimiser. This is local corroboration, not independent human or proof-kernel acceptance.

The verifier checks the two four-form expansions by multiplication and by the subset-sum transform, enumerates the invariant and cubic classes, evaluates the supplied hosts directly, and rejects corrupted hosts and a wrong form. The written coset proof was also re-derived. The follow-up workload estimate in README/TASK is corrected to 2^52 degree-at-most-4 hosts on 120 lines: 163 columns, evaluation rank 111. Those hosts were not enumerated.

Reproduce from the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-frame-host-minimum
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-frame-host-minimum --check-source-history --check-modes
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/p104-frame-host-minimum/verify.py --table --show
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B research/p104-frame-host-minimum/verify.py
# Optional full deterministic regeneration; keep outputs outside the checkout.
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/p104-frame-host-minimum/search.py --scope T120 --iterations 3000 --seed 20261110 --write /tmp/hosts_T120.json
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/p104-frame-host-minimum/search.py --scope P104 --iterations 3000 --seed 20261110 --incumbent /tmp/hosts_T120.json --write /tmp/hosts_P104.json

Another CPython 3.12 executable can replace the absolute interpreter path.

Limitations and unrun obligations

The minimum over all Boolean hosts is open. Exact minima apply only to their named classes; the searched hosts are upper bounds. The charge is an ANF monomial count, not a gate count or a complete signed invoice. No mapping to selected-invoice primitives, shared thirteen-row circuit, physical hosting, restoration or supplier implementation is supplied. All five selected framework assumptions remain. No selected cold replay, degree-four enumeration, Lean, Docker, independent human review or formal proof-kernel review is claimed.

Open next questions

  1. Prove a lower bound for unrestricted Boolean hosts. Start with an exact branch-and-bound on one degree-four evaluation system or a coset-leader lower bound for excluded clique X0, whose supplied host has charge 7.
  2. Minimise the union of charged supports across the 13 rows, starting with the eight invariant and 512 cubic hosts per row on 120 lines. The joint circuit and charging rule remain open.
  3. Name chart monomials as actual invoice primitives under a complete physical contract, beginning with the charge-14 frame-0 host.

Related open work

  • #7031: the frame-0 product charges 40. This package's baseline also computes 40, then supplies the smaller hosts above.

  • #7046: the frame-1 product charges 111. This package's baseline also computes 111. Its 31-monomial intersection is not recomputed here, and shared charging remains open.

  • #7047: excludes affine sums of letters and asks the four-form minimum. This package answers question 2 and extends the named-class census; it does not replay the predecessor proof.

  • #7048: identifies the missing invoice-primitive map for the old forty. No map for the new hosts is provided either.

  • #7014: supplies the frame partition. The factorisation is cited, not re-proved.

  • #7168: optimizes Gram-class support-pairing cost over deleted E8 sets. That cost and matrix constraint differ from the ANF host charge here; no shared host minimum is computed.

  • #7169: constructs a one-sided COPY completion on 93 live E8 lines. It computes support-pairing ranks, not frame-indicator ANF charges.

  • #7170: bounds scalar COPY savings at that 93-line puncture. Its fixed-basis perturbation quantity differs from this hosting census.

  • #7174: excludes an 8k block-mask realisation of a fixed 96-line complement. It constructs and prices no frame-indicator host.

The prepublication overlap check examined 466 open PR titles/bodies, the latest 30 #1166 comments, active discussions, cached card coverage, merged semantic searches and canonical-main README searches. Search coverage is not proof of novelty.

The completion check read all twelve other open account PRs created since the CLAIM: #7132, #7133, #7134, #7135, #7168, #7169, #7170, #7172, #7173, #7174, #7175 and #7176. The E8 geometry neighbors are described above; the others study stock, guards, splitting, Gram spectra, stage ranks or connector chains. None reports a competing ANF charge for these frame indicators. No extra computations were run to check their results.

CI notes

CI did not certify this package. At exact head 1af08e33b84c603c8e68ea6b41232f197a31692f, run 42983769381 completed with the plan job failing and the package replay job skipped. The completed checks were read once, and the run metadata confirms this head.

The failed step is "Onboarding helper tests". Its log reports one failure among 760 tests, with 24 skipped:

test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record
AssertionError: '`make frontier7000-verify`' not found in the CI verification document

On canonical main e54523517d0f03e58352e647c403a5af3e525a57, certificates/selected-result.json requires make frontier7000-verify, while docs/ci-verification.md still describes #6030 and make frontier6030-verify. This PR changes neither shared file. The same failure was reproduced locally before publication with:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B tests/test_research_current_status.py CurrentCiNavigationTests.test_current_ci_section_matches_selected_record

The inspected failed logs for #7132, run 42914704054 and #7134, run 42914997118 show this same sole failing test among 760, with 24 skipped and package replay skipped. These are the other runs independently checked here.

The scientific evidence remains the complete local verification and regeneration recorded above. The head is unchanged; no repository-level fix, retrigger commit or job rerun was made.

Merge danger

Door: two-way. Blast radius: isolated. Nine files in one opt-in research package; no shared code, workflow, selected record or frozen predecessor changes.

Answers open question 2 of CrocSwap#7047. The 120 root lines miss one of the 16
values of the four CrocSwap#7031 forms, so exactly two functions of those forms
host frame 0, with charges 40 and 16.

Adds the coset structure of all 15 odd 8-cliques (28 cosets with 4 lines,
3 empty, one clique), no host of degree 2 or less, exact minima over flat,
translation-invariant and cubic hosts on the 120-line and 104-line scopes,
and explicit sparser hosts for every row. No kappa change.
…kage

The 32 cosets of W split as F, 28 cosets with four lines and 3 empty ones.
The flat indicators are a subclass of the W-invariant hosts, so the invariant
minimum covers them on both scopes. Only the three-form host is compared with
the linear-system enumeration, since the degree-4 product lies outside it.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant