Exclude a historical C5 caller with a common-cut23 bound

.github/workflows/p112-common-slice.yml

@@ -15,9 +15,9 @@ jobs:
     if: github.repository == 'CrocSwap/integer-mult-bounds'
     runs-on: ubuntu-24.04
     timeout-minutes: 20
-    env:
-      TMPDIR: ${{ runner.temp }}/p112-common-slice
     steps:
+      - name: Initialise P112 work directory
+        run: echo "TMPDIR=$RUNNER_TEMP/p112-common-slice" >> "$GITHUB_ENV"
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
         with:
           fetch-depth: 0

research/p112-c5-followup-audit/AUDIT.md

@@ -0,0 +1,166 @@
+# Proof audit and correction of the next caller
+
+This is a fresh, same-author AI-assisted audit of PR3931 at
+`ce148e5aa2bbdc6f420e8a6cf6935e37d5b54cd2`. It is independently inspectable
+evidence, not an independent human/model review or proof-kernel certificate.
+No objection to the common-cut theorem or its literal caller implication was
+found. The important correction is research overlap: PR3295 already excludes
+the suggested next caller `4,5^3,6^6`, conditional on its stated premises.
+The original scientific package is retained byte-for-byte, including its
+historical 68/69 named-inventory receipt and superseded follow-up suggestion.
+
+## PR3931: finite facts and written implication
+
+The new executable imports no predecessor geometry or checker. It parses the
+original canonical caller table, adds the eight literal omitted frame roots,
+checks the complete elementary E8 root patterns, and solves the simple-root
+coordinates by dense Fraction elimination. It uses the original affine-bit-zero
+labels directly. It checks positivity, the evaluation Gram matrix `112 I_8`,
+960 simple-reflection images, parabolic face counts and the unique E7 root
+normal. These are finite facts, with the standard E8 Weyl-chamber theorem
+remaining an explicit mathematical dependency.
+
+For a support A define its binary character spectrum
+
+    F_A(a) = sum_(t in A) (-1)^(a dot ell(t)).
+
+For two independent characters a,b, exact character orthogonality gives
+
+    |A intersect ker(a) intersect ker(b)|
+       = (|A| + F_A(a) + F_A(b) + F_A(a XOR b))/4.
+
+The three nonzero characters of a two-dimensional annihilator form one
+sorted triple, so `a<b<a XOR b` covers precisely all 43,435 binary seven-spaces.
+This character-sum calculation replaces the original bit-mask section counts.
+The full global section histogram agrees, with maximum36. Each of the120
+root supports has section maximum32. A direct table-based enumeration also
+reproduces every coefficient of the 8,214,570-quadruple intersection histogram,
+with maximum14. That last enumeration corroborates the earlier calculation;
+it does not offer a fundamentally different fourfold proof.
+
+The written completeness step is sound. A qualifying direction has support
+at most23+36=59, hence at least53 perpendicular live roots. In a real closed
+Weyl chamber only the63-line E7 face can accommodate that many; its normal is
+a root. To spell out the characteristic-zero transfer: the rational zero-row
+kernel N has a rational point avoiding every declared nonzero root equation.
+If dim(N)>1, a real point of N can additionally avoid the finitely many120
+root lines, while keeping that zero pattern. This contradicts the real
+classification. Thus dim(N)=1 and scalar extension contains the original
+field-valued normal. No real ordering or Hermitian pairing is assumed for K.
+The same argument at support<70 proves the root-only classification and
+distance53 used in the quotient step.
+
+The common-set inequality has the correct quantifier. Live roots need at
+least53-32=21 deletions, frame roots need56-32=24 and cannot qualify. Four
+distinct qualifying root lines under ONE S of size23 would have joint
+off-intersection at least4*21-3*23=15, contradicting14. Four different cuts
+would not prove this. The statement is an upper bound of three lines; this
+audit supplies no three-line attainment or sharpness of23.
+
+The literal `2,3,4,4,7^6` caller transfer is also sound. Its four small
+supports occupy at most22<53 sites. Their quotient images are independent:
+a nonzero relation would be a nonzero codeword of support at most22. Since
+the quotient has dimension at most4, these images form a basis and its
+dimension is exactly4. Subtracting their unique lifts from the six other
+pieces produces six independent codewords. Outside their ONE common small
+support union, those codewords have binary support rank at most7. Evaluation
+injectivity gives six independent directions, contradicting the theorem.
+
+## Existing PR3295 already covers 4,5^3,6^6
+
+The exact public predecessor is Nick Petalas's
+[PR3295](https://github.com/CrocSwap/integer-mult-bounds/pull/3295), head
+`4cff8128f0f9ea1e61515b95ddbb884366e9362c`. All16 changed Git blobs match
+canonical main `20ecf2891d80b5acf18d980b2164fb44ea7faa90` byte-for-byte.
+The central ledger records archival intake as **partially reviewed**, which
+must not be interpreted as mathematical approval. Its proof and receipt are
+live source-bound inputs to this audit. Its existing registered primary,
+separate generating-basis checker and ten behavioral groups all pass here.
+
+The proof's six-piece statement is stronger than the requested caller:
+pieces of ranks at most4,5,5,5,6,6 have code-intersection dimension at most1.
+The normal-plane reduction and incidence/concentration argument withstand
+written review, conditional on the explicit inherited global12/20 capacities,
+all-A2 joint22/32 bounds and standard Weyl-chamber theorem:
+
+1. Two independent codewords in the six-piece span have union at most84.
+   Their at least28 common perpendicular live roots span rank6: smaller
+   parabolic rank allows at most20 root lines. The only qualifying six-node
+   types are D6 and E6. Rational rank and a generic real normal justify the
+   same reduction over every characteristic-zero field.
+2. In E6 a fixed coefficient column forces each piece's singleton sites into
+   one projective fiber. Thus required incidence is at least2*78=156, while
+   the inherited joint bounds permit at most16+3*22+2*32=146. Overlaps and
+   cancellations only consume more incidence, so do not defeat the bound.
+3. In D6 the live union is82 or84. With capacities c=(8,12,12,12,20,20), the
+   deficit identity bounds total missing capacity, outside-union incidence
+   and overlap excess by D=84-|U|<=2. For each piece i its nonsingleton
+   incidences are at most the total overlap excess, hence J_i>=c_i-D.
+   The five rank5/6 pieces therefore have at least10/18 singleton sites.
+4. A rank5/6 piece with that many singleton axis labels has its whole
+   support in that axis. Arbitrary ambient spaces are covered: ten affine
+   labels span rank5 and eighteen span rank6, so their ambient span lies in
+   the axis eight-space. The complete concentration census applies. Small
+   fibers allow only8/12 sites, so cannot hold those singleton counts.
+   The five pieces thus lie entirely on the large axes, leaving at least22
+   small-fiber sites for the rank4 piece, whose capacity is8. Contradiction.
+5. Delete any four of the original six rank6 pieces. The retained span has
+   codimension4, so code dimension at least6 would leave at least2 in the
+   retained6-piece span, contradicting the lemma. Independence is sufficient;
+   there is no assumed disjointness, fixed coefficient value or arbitrary-cut
+   relaxation in this dimension argument.
+
+The PR3295 replay rechecks its new concentration and transport facts; it
+authenticates, but does not reprove, the inherited global and A2 bounds.
+This session likewise does not independently reprove or rerun that entire
+inherited source chain. Source hashes and passing programs are not universal
+theorem acceptance.
+
+## Corrected conditional accounting and next research decision
+
+Within PR3289's fixed historical inventory, the composition is65 original
+contracts + PR3322 (`2^3,7^7`) + PR3405 (`2,5,6^8`) + PR3931
+(`2,3,4^2,7^6`) + the existing PR3295 (`4,5^3,6^6`) = **69/69**.
+This is a conditional partition of exactly that named inventory, not a
+global unresolved count, full C5, a decoder floor or supplier admission.
+The last caller exclusion belongs to PR3295, not this audit or PR3931.
+
+The broader uniform normal-plane question remains unsettled by this work.
+This now-complete conditional inventory supplies no remaining gap that needs
+it. Before another census, identify a different literal TWOSIDE caller and
+bind its quotient, capacities, common-set quantifier and required span bound.
+Otherwise the useful next task is independent review of the inherited
+universal premises and this finite-to-field argument. No new search is reserved.
+
+## Evidence, limits and credit
+
+PR3931 upstream registered CI run39200317292 at head ce148e5 passed on
+2026-10-19 at04:48:12UTC. Both plan and replay succeeded; its log contains
+the three package PASS markers and outcome=completed. CI does not prove the
+written universal arguments. That result concerns the pre-audit head, not a
+later follow-up commit's hosted status.
+
+New Fourier/table replay and controls are registered in VERIFY.json. The
+controls compare every43,435 dual space to direct membership for four literal
+supports (173,740 comparisons), reject four semantic faults, and run three
+actual optimized rejecting CLI corruptions on private copies. CHECKS.json
+records source/publication/export evidence as obtained.
+
+Entry overlap:643 distinct open PR bodies, including drafts, seven REST pages
+plus an empty eighth;2,487 local README/ledger records through the repository
+helper. Browser-loaded latest C5 replies and handoffs were checked. The helper
+could not refresh Discussions without gh; broader Discussion/diff/closed/
+unpublished coverage is partial. The local overlap corpus itself surfaced
+PR3295 and the later mixed566-cut32 package that explicitly cites it. The
+earlier PR3931 follow-up overlooked that public predecessor; this correction
+preserves the original record and credits the actual theorem.
+
+Credit Nick Petalas/PR3295 and PR3278/3267/3260/3262/3269, PR3283's related
+concentration lemma, PR3286's quantifier control, PR3282/3289's accounting,
+PR3322 and PR3405's other caller exclusions, DreamingOfClouds/PR3154,
+joaqcoo and the retained E8/P112 lineage. The common-cut23 theorem and this
+follow-up are by Chris R / Clear1nsight with substantial OpenAI Codex
+assistance. No independent human/model or kernel review is claimed.
+Full C5, the inherited complete scientific suites, selected cold replay,
+physical/native/restoration/consumer/supplier/all-size obligations, Lean and
+Docker remain outside this audit. No selected-frontier change or new kappa.

research/p112-c5-followup-audit/CHECKS.json

@@ -0,0 +1,123 @@
+{
+  "schema": "p112-c5-followup-checks/v1",
+  "environment": {
+    "python": "3.12.3",
+    "platform": "Linux-7.0.0-38-generic-x86_64-with-glibc2.39"
+  },
+  "original_PR3931_head": "ce148e5aa2bbdc6f420e8a6cf6935e37d5b54cd2",
+  "upstream_CI": {
+    "run": 39200317292,
+    "head": "ce148e5aa2bbdc6f420e8a6cf6935e37d5b54cd2",
+    "completed_at": "2026-10-19T04:48:12Z",
+    "conclusion": "success",
+    "jobs": [
+      "plan",
+      "replay (research/p112-common-cut23-caller)"
+    ],
+    "log_markers": [
+      "PASS_P112_COMMON_CUT23_CALLER",
+      "PASS_COMMON_CUT23_INDEPENDENT",
+      "PASS_COMMON_CUT23_CONTROLS",
+      "PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed"
+    ],
+    "scope": "Original PR head only; a later audit commit requires its own CI result."
+  },
+  "bounded_replays": {
+    "p112-common-cut23-caller": "PASS all three original registered commands",
+    "p112-six-piece-concentration": "PASS primary, separate generating-basis checker and all ten behavioral groups",
+    "p112-c5-followup-audit": "PASS fresh Fourier/table audit and semantic/primal/actual optimized CLI controls"
+  },
+  "PR3295_source_binding": {
+    "head": "4cff8128f0f9ea1e61515b95ddbb884366e9362c",
+    "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+    "files_checked": [
+      {
+        "path": "research/p112-six-piece-concentration/BASIS-CHECK.json",
+        "sha": "1e2822b565909dde005ebd988a36bc8047242271"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/CHECKS.json",
+        "sha": "aead13d2f036b2bb2511a6aeaefe9699a8b97cee"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/ENGINEERING.md",
+        "sha": "efec4f6a8c7e5f982f0a4131bcbed9dfaa195896"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/PREDECESSORS.json",
+        "sha": "b5bbae7cc633482fb7c14b00b0f3db8f6bbe4d74"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/PROOF.md",
+        "sha": "0728c80d3140b9e0a7d62ffc540d0313ef578eea"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/README.md",
+        "sha": "db56b0bbffa8862e43932d69ebb7a7a1bff2d40f"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/RESULT.json",
+        "sha": "d68a5599732bc44503a9c56b1f2c54caed98ace5"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/SOURCES.json",
+        "sha": "ae564a10d52e473bc2fa4d42ee938ec0deefa15e"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/TASK.json",
+        "sha": "ea31a85c41ab910189b953f1233784c9541c7063"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/VERIFY.json",
+        "sha": "8a792ea8d64e970a47c0e5d65f2311c7b88127ff"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/independent.py",
+        "sha": "2c0f10b5f4a72dabc504e4b2b9b6433ba7fae147"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/model.py",
+        "sha": "ce2a4c6c85b555eff21d17409cbf0c7f706141bd"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/predecessors/PR3278-PROOF.md",
+        "sha": "bedfda2d1d6babed32eb0abd349723b80a48dfb6"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/predecessors/PR3282-PROOF.md",
+        "sha": "d1a2b2057f04120f2661f72bab9c3b1294d35448"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/test_verify.py",
+        "sha": "cb8eb9d667cbf2edae644dce4c5ef7c33846a9f2"
+      },
+      {
+        "path": "research/p112-six-piece-concentration/verify.py",
+        "sha": "e1ad5d74370cdb6c0f0c797cc2d31c63e234bab0"
+      }
+    ],
+    "result": "All16 PR file Git blobs match canonical main; existing ledger status partially reviewed."
+  },
+  "new_checks": {
+    "dual_spaces": 43435,
+    "root_flat_pairs": 5212200,
+    "fourfold_subsets": 8214570,
+    "primal_membership_oracle_comparisons": 173740,
+    "semantic_rejections": 4,
+    "actual_optimized_CLI_rejections": 3
+  },
+  "entry_overlap": {
+    "at": "2026-10-19T05:34:58Z",
+    "open_PR_bodies": 643,
+    "complete_PR_pagination": true,
+    "local_records": 2487,
+    "Discussion_coverage": "Partial; latest loaded C5 and handoff text inspected, all-board helper refresh unavailable without gh."
+  },
+  "evidence_status": "Fresh same-author AI-assisted audit; no independent human/model or proof-kernel review.",
+  "unrun_obligations": [
+    "Independent reproof and complete replay of inherited global12/20 and all-A2 joint22/32 premises",
+    "Full C5 and global decoder-floor adoption",
+    "Independent human/model or formal-kernel acceptance",
+    "Selected cold replay, physical/native/consumer/restoration/supplier/all-size admission, Lean and Docker"
+  ]
+}

research/p112-c5-followup-audit/README.md

@@ -0,0 +1,41 @@
+# C5 proof audit and predecessor reconciliation
+
+The fresh table/Fourier checker reproduces PR3931's complete seven-flat and
+fourfold histograms. Written review finds no objection to its characteristic-zero
+common-cut23 theorem or `2,3,4^2,7^6` caller transfer. This is a same-author
+AI-assisted audit, not independent human/model or proof-kernel verification.
+
+The key correction: **Nick Petalas's PR3295 already conditionally excludes
+`4,5^3,6^6`**. Its registered replay passes here. The named historical contract
+inventory composes to **69/69**, conditional on the inherited theorems; this
+is not full C5 or a global unresolved count. The original scientific package
+and its historical68/69 receipt stay unchanged. [AUDIT.md](AUDIT.md) supplies
+the detailed proof review, exact predecessor credit and coverage limits.
+
+## Reproduce
+
+```sh
+python3.12 -I -Werror -B scripts/research_package.py --package research/p112-c5-followup-audit
+```
+
+Standard library only. SOURCES.json pins the exact public head/base and all
+live input bytes; VERIFY.json declares both bounded commands. The primary
+imports no predecessor executable. Its character-sum method and173,740 direct
+membership controls test the flat calculation by a different method. The
+fourfold enumeration remains a direct complete corroboration. Three actual
+optimized CLI mutations on private copies must fail. CHECKS.json records the
+separate PR3931/3295 replays, CI scope, source binding and publication evidence.
+
+## Open next questions
+
+Independent review of the standard Weyl/scalar-extension implication and
+inherited global12/20 and A2 joint22/32 premises would strengthen adoption.
+The complete inherited scientific chain was not rerun or independently proved.
+Before expanding the uniform normal-plane census, bind a different literal C5
+caller whose actual quotient and common-set budget need that stronger statement.
+No such new gap is established here, and no further research claim is reserved.
+
+Credit Nick Petalas/PR3295 and its retained source chain, PR3282/3289, PR3322,
+PR3405, DreamingOfClouds/PR3154, joaqcoo and the E8/P112 lineage. New material
+by Chris R / Clear1nsight with substantial OpenAI Codex assistance, Apache-2.0.
+No full C5, physical supplier, selected-frontier change or new kappa is claimed.

research/p112-c5-followup-audit/RESULT.json

@@ -0,0 +1,42 @@
+{
+  "schema": "p112-c5-followup-audit/v1",
+  "flats": 43435,
+  "root_flat_tests": 5212200,
+  "quadruples": 8214570,
+  "flat_size_histogram": {
+    "0": 255,
+    "16": 7,
+    "20": 336,
+    "22": 3584,
+    "24": 3752,
+    "26": 10752,
+    "28": 6416,
+    "30": 10752,
+    "32": 3549,
+    "34": 3584,
+    "36": 448
+  },
+  "fourfold_histogram": {
+    "0": 154056,
+    "1": 12544,
+    "2": 127008,
+    "3": 698880,
+    "4": 2383164,
+    "5": 901824,
+    "6": 1952160,
+    "7": 1046528,
+    "8": 354774,
+    "9": 275520,
+    "10": 168000,
+    "11": 10752,
+    "12": 21840,
+    "13": 86016,
+    "14": 21504
+  },
+  "common_cut_bound": 3,
+  "common_cut_budget": 23,
+  "fixed_inventory_conditional_coverage": 69,
+  "fixed_inventory_rows": 69,
+  "existing_last_caller_source": "PR3295 / 4cff8128f0f9ea1e61515b95ddbb884366e9362c",
+  "scope": "Conditional contract composition; no full C5 or human/kernel review."
+}