[conorholds]

Change and mathematical scope

Closes both adapted and nonadapted d=3 branches of the actual-basis C1 invoice in #3154, using the load-bearing written raw-shape, intrinsic and geometric theorems of #3689, pinned at 3193d1ea9a4fc5d178570a61e6019454b53c1db9. That predecessor merged for archival intake on 2026-10-20 and remains partially reviewed in the central ledger. Its written theorems and E8 assembly remain dependencies; the finite replay does not validate their full proofs.

Let T span all S-words of binary support rank at most seven, with C contained in S, dim S=8+t and d=dim(C∩T)=3. For either adaptation status and t∈{2,3}, this proves:

• Under raw weight budgets 72/73, the actual invoice I=Σw−n_c is at least 65.
• With an actual live-root dual, I≥65 and I−εₖ≥64 for εₖ∈{0,1}.
• Without a mark, I≥64. The singleton-pivot consumer follows with its exact actual-rank, nonparallelity and pivot hypotheses and a d=3 nonpivot basis.

The proof closes every nonadapted residue, all fifteen adapted t=2 profiles, all ten all-low adapted t=3 profiles through inside sum 32, and twenty high-containing candidates via fifteen justified actual-profile transfers. At inside sum 33, a same-axis correction merge lowers raw weight, never increases the invoice and produces a t=2 basis with d=2 or3. The t=2 theorem is proved first, so the merge is not circular.

A reusable geometric lemma shows that two binary flats of rank at most seven contain at most 68 full E8 root lines in their union. Each distinct excluded frame label lowers the live bound by one. Distinct maximal 36-root sections have intersection counts 6,10,12,20 and union at most 66; a disjoint mixed 36/32 pair attains 68. The written proof uses quadratic character sums, with exhaustive finite corroboration. This is full-root union sharpness, not invoice sharpness.

No N8, minimum actual basis, distinct arbitrary inside correction indices or normalized-list completeness is assumed. Corrected weight-nine members and fixed actual coefficient maps are retained. The d≥4 invoices, global rank/pivot normalization and complete C1 remain open; κ and the selected frontier do not change.

Task and overlap

One focused submission commit containing only research/p112-d3-actual-invoice/, rebuilt on main 12fa8c5c844be21bfefb38a19503fbd867a11244, priority revision 7. The revision-6 scout changed scope from uniform-transfer-audit to the C1 handoff in Discussion3156. TASK.json preserves that historical assignment, pins the revision-7 catalogue and records continuation of the same scope. This package does not answer the card's new #4100 all-size audit; an off-card result may have lower intake priority.

Closest predecessors: #3689 supplies d=1/d=2 and partial d=3; #3455 supplies d=0, correction counts and the consumer; #3166 supplies the matched two-axis input. The seven cited #3689 manuscripts now also have current-main provenance pins, byte-identical to their original pinned-head citations.

Fresh read-only overlap check: 2026-10-20 16:10 UTC PR/main snapshot, with Discussion1166 metadata completed at 16:11:56 UTC. The external audit screened 602 changed PRs; the fresh REST/search union screened 29 updates, including ten additional PRs, for 612 distinct PR numbers across those lists. Nearby #4203/#4204 concern different physical-carrier contracts. Discussion3156/1167/1587 timestamps were unchanged; the fresh Discussion1166 delta was inspected. No competing d=3 completion was found. Unpublished work, uninspected diffs and changes absent from both PR responses remain outside that coverage. No public claim has been posted.

Validation

python3 scripts/research_package.py --package research/p112-d3-actual-invoice --check-only
python3 scripts/research_package.py --package research/p112-d3-actual-invoice
lean -DwarningAsError=true research/p112-d3-actual-invoice/formal/OutsideRestriction.lean
lean -DwarningAsError=true research/p112-d3-actual-invoice/formal/FiniteOutside.lean

Python 3.12, standard library only; Lean 4.21.0, Init only. Scientific checks run serially under a 256 MiB process-tree watchdog; sampled RSS is not a rigorous peak-memory bound.

• Exact nonadapted/adapted profiles, c9 allowances, correction counts and sum 33 merge arithmetic. The η upper endpoint is derived from the raw budget.
• All 43,180 affine six-sections, 5,440 maximal 36-root sections and 14,794,080 unordered distinct maximal pairs in two implementations. flat_union.py reuses frame_pair_geometry.py's E8 model; the independent canonical_union.py imports no package model. Both derive the universal bound 68 and must agree on both spectra. Wrong-coset controls reject changed sections and false sharpness fixtures.
• All 56 ordered frame pairs, 1,792 completion deletions, 224 coefficient-support strata and 2,040 matched G2 cuts; all 42,840 matched G4 residuals, with 1,271,200 direct deletions using a second rank criterion.
• A genuine nonadapted basis with dim S=11, dim T=6, d=3, r=1 and nonzero duals; its true T is certified over all 43,435 rank-seven binary flats. Raw 84/invoice 83 is outside the theorem budgets. An exact singleton-pivot Gram fixture directly checks ranks (9,11), nonparallel rows and cost 84.
• Semantic controls reject omitted profiles, invalid allowances, altered geometry, a false G4 label, omission of a genuine low generator, wrong pivot sign and an omitted Gram term. The PASS summary now reads its counters from the computed result.
• Ten unchanged Lean declarations cover additive outside restriction and finite scalar combinations: two use Quot.sound; eight have no axioms. Prior author and external AI-audit compilations passed; those unchanged files and toolchain pins are retained. The E8 bridge, geometric exclusions, merge and complete invoice assembly remain unformalized.

RESULT.json binds the exact package bytes and recomputed counters. It was regenerated explicitly after the audit fixes, and the registered Python 3.12 replay passes with all prior scientific counters unchanged. Committed-byte/source-history, official export, optimized Python 3.14 Git-free replay and attribution checks cover the exact publication artifacts. Export replay is read-only, including with an empty PATH. Timing and sampled memory observations are private evidence rather than proof claims.

The external AI audit rederived all new written arguments and independently probed the section/pair geometry. Restricted four-axis rigidity, G4, A2-plane facts and parts of the predecessor's E8 assembly remain inherited written inputs rather than independently validated conclusions of that audit. Hosted CI, repository-wide builds, full predecessor suites and independent human review have not been run.

Credit

Retains DreamingOfClouds's #3154 actual-basis programme and #2816 root-pencil lineage; conorholds's #3689/#3455/#3166; Nick Petalas's #3269/#3300 capacities and #3171 coordinate-kernel method; David Arias's E8 model lineage and the source packages' existing credits. Exact sources, licenses and substantial AI-assistance disclosure are in NOTICE.md and DEPENDENCIES.md.

Open next questions

Actual invoices with d≥4, the actual-vector-space bridge for the finite outside-restriction Lean core, and global rank/pivot normalization remain open. README.md and TASK.json give first steps and blockers.

[rcfc-jreed]

Independent scoped audit of #4219 complete d=3 actual P112 invoices (t=2,3) at f067a8ef: RESULT matches (28/28)

Code-disjoint checks; does not import package verify.py (local fork against pinned geometry.py at base 12fa8c5c…). Package bytes from head f067a8ef06a186e36518d8ed5a6d0d6820f56e92 via GitHub contents API. CLAIM.

No packaging defect in scope. RESULT.json matches fork recomputation.

What passes:

1. All fifteen SOURCES digests match (live geometry input + provenance pins).
2. Nonadapted positive fixture: (dim S, dim T, d, r, raw, invoice) = (11, 6, 3, 1, 84, 83) with true_T_certified.
3. Matched two-axis G4 exhaustive check pass; double-seven full-root union pass; independent canonical union spectra agree.
4. Geometry failure controls all detect (frame / G4 / double-seven / canonical mutations).
5. Profile arithmetic receipts present for nonadapted + adapted t=2/t=3 branches; status pass. Written E8 theorem assembly remains out of finite replay scope (as declared).

Not covered: Lean formalization acceptance; predecessor #3689 full written-proof review; #3154 ledger closure as maintainer merge; new κ.

This is a finite pin/seal/math replay, not a formal proof.

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).