Skip to content

Independently audit PR4992 sharp five-label excess cap #5049

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 1 commit into from
Oct 23, 2026
Merged

Independently audit PR4992 sharp five-label excess cap #5049

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
187 changes: 187 additions & 0 deletions research/f7-sharp-cap-independent-audit/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,187 @@
# Independent audit of the sharp five-label cap

**Corroboration; no new bound or kappa.** This answers Ali Romman's explicit
[independent-review handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19138920)
for [PR4992](https://github.com/CrocSwap/integer-mult-bounds/pull/4992).
The written-proof review below finds no blocking gap in its stated domain.
A separately implemented six-plus-six path join corroborates the cap **11**
and exclusion of every weight-four **(8,4)** split, without using either result
to discard a path. It imports no predecessor executable.

The audited theorem concerns simple restored universal singleton-prefix walks
of length twelve in F2^5, and functionals of weight four or five. For the two
functional classes A,B, the excess is

`choose(|A|,2) + choose(|B|,2) - |D(A)| - |D(B)|`,

where D(C) contains XORs of distinct pairs in C. Shared differences in the two
classes count twice. Universality means the twelve vertices have all 32 XOR
sums, including zero. The result and both equality witnesses belong to the
predecessors; this package adds independent implementation and proof coverage.
This is AI-assisted review, not independent human or proof-kernel acceptance.

## Written-proof audit

Reviewed source: PR4992 head `12a0105150f5f44a19a2199db8506d1aa44b009a`,
retained at main base `f259dabc7d70e0db8d6d36bfda888f008bbfecc1`.
Its [proof](../f7-five-label-sharp-cap/README.md), verifier and receipt are
exactly bound in [SOURCES.json](SOURCES.json). They are authenticated, not
executed by the new verifier. The original registered verifier was also replayed
separately, in both normal and optimized Python.

1. **Class coverage and balance.** Universality implies
`D(A) union D(B) = ker(f) minus {0}` because cross-class differences have
functional value one. For weight four, the omitted-coordinate edges form
a matching, including the closing edge. Counting degree two at every cycle
vertex gives `s-t=a-b`, `2a<=s`, `2b<=t`. Hence the only unordered splits
are (6,6), (7,5), (8,4). Weight five alternates and forces (6,6).
2. **Saturation in (8,4).** Equality forces four omitted-coordinate edges
in the majority, none in the minority, and eight crossing edges. Every
majority vertex belongs to exactly one matched pair. Contracting those
pairs leaves four distinct block labels T in the even subspace E of F2^4.
The four minority vertices alternate omitted-coordinate levels. No
planarity assumption on the minority is used.
3. **The potentially delicate repeated projection.** A planar T supplies only
seven lifted majority differences, insufficient even with six minority
differences. Thus T has six differences. Its missing direction z satisfies
`E = T disjoint-union (T+z)`. The minority must supply both missing lifts
(z,0) and (z,1). A same-level pair u,w=u+z occupies both vertices of one
level. A pair supplying (z,1) must use one of these vertices, so the other
level repeats u or w. Relabel to repeat u. The cyclic minority order is,
up to reversal and rotation, `u_0,u_1,w_0,y_1`; y=w is allowed. The four
distinct contracted blocks require at least three neighbors of u in T
and two of w. Translation by z exchanges T and its complement in E and
sends N(u) to N(w), so those two neighbor counts sum to four. This is
the claimed contradiction. Distinctness of the block labels, rather than
distinctness of all four projected minority points, justifies the count.
4. **Small support lemma.** Five, six or seven points have affine dimension
at least three. In dimension three their difference support is seven.
In dimension four an affine basis gives ten differences; a sixth point
of weight two or three gives twelve, and weight four gives fifteen.
To make the weight-three case explicit, translate
`{0,e1,e2,e3,e4,e1+e2+e3}` by e1 and use the basis
`(e1,e1+e2,e1+e3,e1+e4)`. The extra point is the sum of the second and
third basis vectors. Thus both twelve-support cases reduce to the source's
`{0,1,2,3,4,8}`. Its four-row table covers every possible seventh point
and contributes a new difference, giving at least thirteen.
5. **Final excess.** In (6,6), supports of size seven and seven cannot cover
fifteen directions, so their sum is at least 7+12. In (7,5), a
three-dimensional seven-point class would require the five-point class
to cover eight directions outside that subspace. Its two cosets supply
at most `k(5-k)<=6` such pairs. Hence the seven-point class has full
affine dimension; the support sum is at least 13+7. Both excess bounds
are eleven. The two cited words attain equality.

This review covers the claimed proof implications, including the nonplanar
minority. It does not establish any seven-label or partial-prefix assertion.

## Independent finite method and completeness

The new enumerator lists **every simple six-edge cube path starting at zero**,
grouped by its final vertex. It joins every unordered pair with that same
endpoint whose vertex-set intersection is exactly the two endpoints. Reversing
one path yields a simple twelve-edge cycle, with the closing edge included.

Conversely, split any simple twelve-edge cycle based at zero at its sixth
edge. Its two halves appear in these lists and have disjoint interiors.
The split is unique, and reversing the cycle only exchanges the halves.
Thus the join enumerates each cycle exactly once up to reversal. There is no
label-permutation reduction, universality prune, matching-balance prune,
quotient test, or excess prune in this generation step.

After generation, direct pair XORs decide universality and compute each of
the six high-weight functionals. Every generated cycle separately passes
vertex, simplicity, adjacency and closing-edge checks. Six smaller domains
compare the complete cycle sets against literal enumeration of every word;
they also check that the join emits no duplicate cycle.

| Quantity | Independently recomputed count |
|---|---:|
| All rooted cycles up to reversal in Q5, length 12 | 221,700 |
| Those using all five labels | 202,860 |
| Universal cycles | 49,680 |
| Universal cycle / high-weight functional checks | 298,080 |
| Universal weight-four (8,4) splits | 0 |
| Maximum excess for each of the six masks | 11 |
| Literal words in the six calibration domains | 77,019 |
| Distinct calibration cycles | 418 |

The complete excess histogram agrees with PR4907's earlier receipt after
multiplying by 60. This comparison happens after generation and evaluation.
That factor is exact: a simple twelve-cycle uses four or five labels, and
both label orbit sizes in Q5 are 120; this audit then identifies the two
orientations. Summing over every high-weight functional preserves the same
factor. The prior 828 universal normalized words and their maxima are not
new discoveries. [RESULT.json](RESULT.json) retains the full histogram and
a digest of the deterministic universal-cycle stream.

## Reproduction and controls

Python 3.12, standard library only, from the repository root:

```sh
python3.12 -B scripts/research_package.py --package research/f7-sharp-cap-independent-audit
```

The registered commands run the independent audit normally and with `-O`,
then its mutation controls. Expect `PASS_F7_SHARP_CAP_INDEPENDENT_AUDIT`,
`PASS_F7_AUDIT_CONTROLS`, and `PASS_REGISTERED_RESEARCH_PACKAGE`.
One full enumeration took about five seconds locally on Windows 11 with
CPython 3.12.0; this is a reproduction estimate, not a speedup claim.
Direct commands, also valid in an export containing the declared inputs:

```sh
python3.12 -I -B research/f7-sharp-cap-independent-audit/verify.py
python3.12 -I -O -W error -B research/f7-sharp-cap-independent-audit/verify.py
python3.12 -I -O -W error -B research/f7-sharp-cap-independent-audit/test_mutations.py
```

Eight semantic rejections cover the too-small cap, wrong functional domain,
length, repeated vertex, omitted closing edge, boolean vertex, nonuniversality
and a universal point set lacking the cycle contract. Both sharp witnesses
are positive controls. The set-only and low-weight counterexamples have
excess 18 and 21, respectively, and demonstrate why the hypotheses matter.

Six actual code mutations exercise the small literal-word calibrations and
semantic controls **without receipt comparison**: overlapping path interiors,
a missing coordinate, a missing closing edge, coordinate-bit grouping,
cross-class support, and cap ten. Two additional private-copy CLI controls
alter the reviewed proof and replace integer 1 by boolean true in the receipt.
The latter requires typed JSON comparison. Frozen inputs are never edited.

## Scope, coordination and credit

Task `census-pruning-audit`, changed scope under the explicit handoff; priority
revision 7. [Canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19140301).
The entry overlap check covered 324 open PRs and 4,127 Discussion records
with complete remote pagination. After materializing relevant f7 packages,
103 local records were searched; 6,609 tracked notes remained omitted.
Arbitrary diffs and unpublished work are also outside that coverage.
PR5001 and JoyboyBrian's active prefix-engine integration are separate.

The source-binding orientation for selected #4470 passed. The selected kappa
remains `60403/20000000`. No selected cold replay, engine integration,
seven-label census, supplier admission, full multiplication theorem, Lean
or independent human review is claimed. Full-history ancestry preflight
is not claimed in this shallow checkout. The audit covers the exact pinned
proof and finite domain; later source changes require reassessment.

Credit **Ali Romman / PR4992** for the sharp theorem and neighbor-count proof;
**Mihir Srivastava / PR4907** for the earlier cap, quotient setup, finite
measurements and handoff; **Nick Petalas / PR4894** for matching balance.
Retain **unpaidmoon / PR4148**, **Nicholas Stone / PR2973**,
**James Reed / PR3096**, and **Ross Richardson / PR943** for the question,
corrected excess boundary, audit and singleton-prefix model. The new algorithm
is separately implemented; the reviewer read the predecessor sources and
does not claim a blinded review. Original sources and notices are unchanged.
Prepared by Mihir Srivastava with substantial OpenAI Codex assistance, solo.
New work is Apache-2.0.

## Open next questions

Independent human or proof-assistant review can strengthen confidence in the
four-block contradiction; begin with step 3 above, including y=w, and the
explicit affine-basis change in step 4. This requires new review, not a larger
finite census. PR5001's partial-prefix contract and its already claimed engine
integration remain the relevant downstream work. This audit does not reserve
them or infer a runtime benefit. No larger census is justified by this result.
186 changes: 186 additions & 0 deletions research/f7-sharp-cap-independent-audit/RESULT.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,186 @@
{
"audit": {
"all_cycles": 221700,
"all_five_labels": 202860,
"functional_checks": 298080,
"histogram": [
{
"count": 25920,
"excess": 3,
"split": [
6,
6
],
"weight": 4
},
{
"count": 83520,
"excess": 6,
"split": [
6,
6
],
"weight": 4
},
{
"count": 5760,
"excess": 8,
"split": [
6,
6
],
"weight": 4
},
{
"count": 7920,
"excess": 11,
"split": [
6,
6
],
"weight": 4
},
{
"count": 31680,
"excess": 6,
"split": [
7,
5
],
"weight": 4
},
{
"count": 48960,
"excess": 8,
"split": [
7,
5
],
"weight": 4
},
{
"count": 25920,
"excess": 9,
"split": [
7,
5
],
"weight": 4
},
{
"count": 18720,
"excess": 11,
"split": [
7,
5
],
"weight": 4
},
{
"count": 11520,
"excess": 3,
"split": [
6,
6
],
"weight": 5
},
{
"count": 33120,
"excess": 6,
"split": [
6,
6
],
"weight": 5
},
{
"count": 2880,
"excess": 8,
"split": [
6,
6
],
"weight": 5
},
{
"count": 2160,
"excess": 11,
"split": [
6,
6
],
"weight": 5
}
],
"maxima_by_mask": {
"15": 11,
"23": 11,
"27": 11,
"29": 11,
"30": 11,
"31": 11
},
"universal_cycle_stream_sha256": "5caaa895d18de8f878566eb553d83cd4263b558bc0b34815184292470ad553d7",
"universal_cycles": 49680
},
"calibration": [
{
"cycles": 1,
"length": 4,
"literal_words": 16,
"n": 2
},
{
"cycles": 3,
"length": 4,
"literal_words": 81,
"n": 3
},
{
"cycles": 12,
"length": 6,
"literal_words": 729,
"n": 3
},
{
"cycles": 6,
"length": 8,
"literal_words": 6561,
"n": 3
},
{
"cycles": 48,
"length": 6,
"literal_words": 4096,
"n": 4
},
{
"cycles": 348,
"length": 8,
"literal_words": 65536,
"n": 4
}
],
"controls": {
"low_weight_excess": 21,
"semantic_rejections": 8,
"set_only_excess": 18,
"sharp_witnesses": 2
},
"package_sha256": {
"README.md": "5ae16b49f957ab009194bdb85af4bcf63b27b62149c15d0f5cf09a6a83e812a5",
"SOURCES.json": "352f93ec3b588b3eac2bb71a8b0a391bbdad4ebb8fdf630f72e1669c8ade303c",
"TASK.json": "bbb17fa71a29a4cd3c6e3ad874fa9403f7b49aef27a1f0eeeab36109e99cf503",
"VERIFY.json": "4d61d05693e88246eb9129f456c859ccbc38137033a55df00a10a9ce7442d348",
"test_mutations.py": "09cdf95ed0f30eabfcf7f8a7e0776a7e2f1f8c783b7cb49bf7a5b99dd300c18e",
"verify.py": "e8ba74747f14dcce1bd14c6676c1214d1b38f76cc44590fc5468a7743045028c"
},
"schema": "f7-sharp-cap-independent-audit/v1",
"source_sha256": {
"research/f7-five-label-pruning-proof/RESULT.json": "5bd83ffe534373471731bc59c6795ee864192882b6bd31683ffb44a88c864755",
"research/f7-five-label-sharp-cap/README.md": "c03f524035f4abeb9103e7e43486ee75b83538e41abb50cd3beaecd01119f871",
"research/f7-five-label-sharp-cap/RESULT.json": "08251f786df0070dea092ae180fc3fa5efe7b386aed04fa86aff601343bfd718",
"research/f7-five-label-sharp-cap/verify.py": "035687ed280ac001fc29c24f36ee7974966011206e11140891f9312ccefd69fb"
}
}
Loading