[jacobalansussman]

Change and mathematical scope

Headline (checked by computer, not proved in Lean). On Marius-Paul Dumitrean's #2979 words
(research/rank7-joint-endframes, unchanged, read in place from main) with a table of hosts that I re-solved for
the full cut (A-fc, carried in fills/2979Fc/), removing each of the 16,576 literal heads (job 25 on its array)
gives b = 1.7887045643e-3 for the DFT, certified at 17,887,045/10^10 (verify.py --instance 2979Fc, registered).
That table's own figure with no lever is 1.6897030e-3, below #2979's 1.7290340e-3: it pays off only with the full
cut, and the community's admission rejects it at its strict-gain steps, by design (details below). It is not proved
in Lean; the same full cut is proved in Lean on #3945 with every head kept, at 1.7806935e-3.

Result on #2979's published table. A change of the recursion, not of the word, raises the complex-side figure
from b = 1.7290339826e-3 to b = 1.7556473153e-3 (+1.539 %). It is a saving for the discrete Fourier transform in OpenAI's exact-arithmetic
machine model. On Dugongue's #3945 the same lever gives 1.7501109246e-3, and on #3945 with every head kept (its words
and price, with a table of hosts re-solved by the community's own allocation programs so that every block that can be
a head stays empty, carried in this package) 1.7581520168e-3; on that table the full cut (each head removed,
job 25 on its array, every other rank-48 block split into two blocks of 24 on the same role) gives
1.7806935406e-3. I have proved those DFT bounds in Lean (below), the highest at 1.7806935e-3. No κ is
claimed.

The change (the lever). In #2979's unit, 16,086 of the 28,190 rank-48 blocks per round (8,064 in child 8, 8,022 in
child 10) are literal heads: the first non-identity operation on their own array, acting on that array alone, with
nothing hosted there before. I cut each head by 24 of its 48 axes, so that its array takes a job of 49 axes while
every other array keeps the full 73. The recursion then feeds the word with jobs of two sizes in a fixed ratio
(50,218 : 16,086 arrays per round). Theorem 1G (PROOF.md) shows that such a recursion runs at the speed of its
balance, sum_r n_r (r/73)^(1-b) = 50,218 + 16,086 (49/73)^(1-b), provided every paid block is smaller than every job
(48 < 49).

Changed hypothesis. The community's recursion gives every array the same job; the ceiling tool assumes it. The
mixed-target recursion changes that coverage law, so, as the card's allowed variation says, I give Theorem 1G as the
replacement bound and do not apply the incumbent ceiling. Nothing else changes in the lever: no gate, no axis between children, no
endpoint; on #2979's published table no allocation row changes either, while A-fc and the tables with every head
kept are re-solved tables of hosts (described below and in README sections 7 and 9).

Status of the headline A-fc. Checked by computer here (verify.py --instance 2979Fc, both parts): the table
pinned by sha256, 16,576 literal heads (8,288 + 8,288) and no other rank-48 block in my network, the global profile
equal to fills/2979Fc/PROFILE.json, the uniform root equal to the community's own root for this table to 24 digits,
the full-cut price, and the exact rate certificate at 17,887,045/10^10, refused one step higher. Proved in Lean,
outside this repository: Theorem 1G (Eng.engine_seam_final) and the general theorem of the full cut
(cut_heads_full, Work/Mixed/Bridge/CoreF), as used on #3945 with every head kept. Not in Lean: A-fc's own
instance (its heads-first certificate, the cut fact on #2979's words, which is argued from the template it shares
with #3945's, and the rate fact at 17,887,045/10^10).

How A-fc's table was made, and the community's checks on it. A class solution of a mixed-integer program on
#3815's Hall model, then #3815's own reverse-time placement (Erwan Secousses' / ChaloupeMusic's build_fill.py) in a
tolerant mode: a role with no planned slot left at its call goes to a spare bin that is open at that call, is not a
head bin, is not yet used at that call and has room. Nine roles were placed that way (8 of width 6 at call 553, 1 of
width 4 at call 0), and 8 planned width-6 slots stayed idle. However it was made, the table is checked as a table:
run unmodified on a fresh clone at the base, #2979's checks pass it, including #2979's PR2839 owner engine (271,728
roles, T = 74, its seven corruption controls rejected), check_allocation.py's pins, words, PROVIDERS, physical
count 66,813 and 5 rejection controls, the exact moment auditor (root 1.6897030e-3), check_cap.py's cap
certificate, rank mass and local profile, and the complete replay up to the admission (fresh natives, owners, parent
lift, rebind, discovery 7 of 7, outer ledger with 63 positive checks). It is rejected exactly where the lower figure
1.6897030e-3 is compared with a higher one: the moment auditor's strict gain (audit_allocation_moment.py line 65),
the complete admission (admit_extension.py line 388), and the release's strict-gain list (at PR2269); and by
check_cap.py's recorded gap (line 68), which is a near-optimality bound on #2979's own claim (root within 1e-6 of
the cap; A-fc's gap is 3.93e-5), not literally a strict-gain check. The community's moment engine cannot price A-fc's
model with two job sizes: its halving constraint m^2 > 2 r_max^2 holds for the uniform model (5,329 > 2 * 48^2 = 4,608) and
fails for the job of 25 (625 < 2 * 23^2 = 1,058). The 1.7887046e-3 comes from my own pricing under Theorem 1G, which has no such
condition (the full cut on #3945 with every head kept, 625 < 1,152, is proved in Lean the same way).

Status of the other instances. Construction plus proof. Checked by computer here: my conversion of both words, the head count, the
global profile (equal to PROFILE.json digit for digit), the uniform root (equal to complex_lower to 24 digits), the
half-cut price, and an exact rational certificate of the rate inequality at the figure, refuted one grid step higher.
Proved in Lean, outside this repository: the DFT bound (OpenAI's UniformFourier statement with only the exponent and
the names changed), with Theorem 1G and the cut theorems inside that proof.

Remaining obligations. (0) A-fc's instance in Lean (open question 3). (1) Whether the outer step for integer multiplication accepts a supplier with two job
sizes is open; that is why no κ is claimed. For orientation only: b is above the selected bit side c = 1.7334270e-3
(#589), so the bit side would bind. (2) The cut is not replayed in the community's exact eight-stream operator model
(checked in my lowering and network, and in Lean for the DFT). (3) The halving guard m^2 > 2R^2 of the outer recipe
holds for the half cut (49^2 > 2 * 24^2; argued, not checked) but fails for the full cut, the headline included
(25^2 = 625 < 2 * 23^2 = 1,058; < 1,152 on #3945), so the outer recipe as written does not take the full cut; one
more reason no κ is claimed.

Task and overlap

• Base 12fa8c5c844be21bfefb38a19503fbd867a11244. Inputs: ten files of Conditional κ ≈ 0.0017290339826465: joint rank-7 end frames, five paired extractions and #2957's rewrites on #2942's words (+5.00e-6 over #2969) #2979 on main (head
  be191346391661f4d35fc0d1508d0a6029572576), pinned by Git blob and sha256 in SOURCES.json and declared in
  VERIFY.json. No foreign commit; nothing of Conditional κ ≈ 0.0017290339826465: joint rank-7 end frames, five paired extractions and #2957's rewrites on #2942's words (+5.00e-6 over #2969) #2979 is copied.
• Card complex-new-helper-inventory (the card Conditional κ ≈ 0.0017290339826465: joint rank-7 end frames, five paired extractions and #2957's rewrites on #2942's words (+5.00e-6 over #2969) #2979 and Raise conditional staged544 κ by filling idle owner slots #3945 used), scope_status: changed, reason in TASK.json.
  It also bears on independent-moment (my head test and lowering are an independent reconstruction of Conditional κ ≈ 0.0017290339826465: joint rank-7 end frames, five paired extractions and #2957's rewrites on #2942's words (+5.00e-6 over #2969) #2979's paid
  profile from its words and FILL rows) and formal-interface-lemma (the Lean statements in README section 5).
• Second instance: Dugongue's Raise conditional staged544 κ by filling idle owner slots #3945 (head 91f81d131252db704f945891da1ea54e29d46b8b, archived on main on 20 October 2026 with the same files):
  57,312 heads, b = 1.7501109246e-3, with the same programs (verify.py --instance 3945, README section 6). Not
  registered: its files were on an open pull request when this package was made.
• Third instance: Raise conditional staged544 κ by filling idle owner slots #3945 with every head kept (verify.py --instance 3945H, README section 7): the same words, order,
  dispatch, plan, template and global profile, the table of hosts fills/3945H/FILL.json.gz (made with the
  allocation programs Raise conditional staged544 κ by filling idle owner slots #3945 uses, with one added condition; Raise conditional staged544 κ by filling idle owner slots #3945's complete stated verification passes on it, 119 of
  119 controls rejected): 80,640 heads (40,320 + 40,320), b = 1.7581520168e-3, certified at 17,581,520/10^10. Not
  registered either, for the same reason.
• Headline instance A-fc (verify.py --instance 2979Fc, registered, README section 9): Conditional κ ≈ 0.0017290339826465: joint rank-7 end frames, five paired extractions and #2957's rewrites on #2942's words (+5.00e-6 over #2969) #2979's words with the table
  fills/2979Fc/FILL.json.gz (sha256 7fc766c6c3e1561cee60b258138a918020b96d85ea782a2b01ad0ee035fd082e) and its
  paid profile; 16,576 heads removed, no split needed, every paid block of rank at most 23 < 25; b = 1.7887045643e-3,
  certified at 17,887,045/10^10, refused one step higher, with a single head, with one head fewer and with the heads
  kept as blocks of 48. The programs that made the table, its class solution and the commands to re-create it are in
  the Lean repository (research/record-track/programs/a-fc/, research/record-track/data/a-fc/).
• Fourth instance: the full cut on Raise conditional staged544 κ by filling idle owner slots #3945 with every head kept (the table of 3945H; verify.py --instance 3945F,
  README section 8): the 80,640 heads
  removed (job 25 on their arrays) and the 57,312 other rank-48 blocks split 24 + 24, so every paid block has rank
  at most 24 < 25; b = 1.7806935406e-3, certified at 17,806,935/10^10 and refused one step higher, with the figure
  also refused for a single head, one head fewer and the profile without the split. Not registered either.
• Nearest work and what this adds: the idle-axis chain retracted on 18 and 19 October (Conditional κ = 0.001730189061233850760095: idle rank-48 star exchanges on #3148's T740 fill (+0.0238%) #3184, Conditional κ = 0.001733427039589844234749 (bit-bound): idle-remainder donors on #3148's T740 fill (+0.187% over #3184) #3190, Conditional κ = 0.001734770557111513160495: R438 bit supplier with #3190's idle-remainder donors (complex binds again, +0.0775%) #3198, Conditional κ = 0.001734807021726127552033: greedy idle-axis phase on #3198 with the R438 bit supplier (+0.0021%) #3200,
  Conditional κ = 0.001734815770385098563484: exact per-group idle-donor search on #3200 (+8.75e-9) #3251; Conditional κ = 0.001734846264120199151475 (+0.00176%): hosted remainders as receivers on #3251, complex passes R438 again #3934 to Conditional κ = 0.001736738651088946052684 (+0.00533%): pooled R437 slack across bit replicas on #3958 #3959, after Research: the open PR3934 → PR3959 chain still uses PR3251's retracted idle-axis moves (no new κ) #4046) moved idle axes between children and changed the exact operator; this package
  moves nothing and keeps the operator, it changes the job taken by the head arrays. The audits of Conditional κ ≈ 0.0017290339826465: joint rank-7 end frames, five paired extractions and #2957's rewrites on #2942's words (+5.00e-6 over #2969) #2979 (Independently audit #2979's joint rank-seven frame paths #2993,
  Independent verification (no κ): #3015's R1 restore edit on #2979's words is exact and correctly priced; R1 unique in its rewrite class; #3018 journal and #3021 composition reproduced; no defect found #3053, Research: independently replay #2979 staged rank profile and T74 aggregate #3079, Research: audit #2979 profile against kappa=0.1 #3093, Research: audit PR #2979's group-A native paths and their binding to the T74 invoice (no new kappa) #3236, Research: certify PR #2979's V45 final-word controls fail the complete packing budget #3237, Research: audit all PR #2979 private frees and their expanded native dependencies #3238, Prove dirty-private identity for PR2979's isolated cleanup #3245, Research: independently re-solve PR #2979's fixed-capacity stage caps and price each stage-one group alone (no new κ) #3285, Research: group B native residual widths under #2979 joint W (no new kappa) #3411, Research: group C native residual widths under #2979 joint W (no new kappa) #3436, Research: group D native residual widths under #2979 joint W (no new kappa) #3441; open Add independent V45 frame and ledger audit #3911 and research: audit exact T74 moment endpoints #3923, and Record the archive-only blob disposition for PR 2979 #3585, archived on 20 October) found no
  defect; none uses jobs of two sizes. "Lever" in research/complex-local-word-ceiling (levers.py) names budget
  screens of the local word, an unrelated use of the word. I found no pull request with a recursion of two job sizes.
  Newest complex figures when I wrote this (20 October 2026, 03:00 EDT, after that morning's archive merges; read again at 13:03 EDT, up to research: exclude eight calls for one GL3 dirty-register target #4211): Conditional κ = 0.001730980255989036959962 (+1.140e-9 over #4088): one-third fourth-entry fill attaining #4091's pooled ceiling #4181
  (open) 1.7309803e-3, a fill that attains the pooled ceiling certified in Prove the sharp pooled optimum for fourth staging #4091 (a ceiling, not a construction);
  Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 and Improve conditional κ with a mixed fourth staged entry (+8.696e-9) #4088 1.7309791e-3, Conditional κ = 0.001730970419199163702738 (+1.614e-7 over #4076): receiver sharing on the staged T360 supplier #4085 1.7309704e-3, Conditional κ = 0.001730809033576552081734 (+1.458e-7 over #3945): three staged helper entries and an LP-exact T360 fill #4076 1.7308090e-3, archived on main. The
  headline is above every complex-side construction claimed on the hub by others; some research notes there print
  higher ceilings, targets or hypothetical ledgers (for example the archived Research: exact Toom-3 five-product profile screen #3974, and the widened-window ledger of
  KB1c: admission-ready evidence for the typed-window z4 typed-echo schedule (no new kappa) #2705 / KB1b: the ERASE deferral is not necessary — legal per-call COPY/ERASE windows keep the typed-echo pair saving (no new kappa) #2595), which are not constructions.

Validation

python3.12 -B scripts/research_package.py --package research/lever-mixed-targets-2979 --install-deps
# = python3 -B research/lever-mixed-targets-2979/verify.py --part main      (PASS_LEVER_MIXED_TARGETS_2979_MAIN)
#   python3 -B research/lever-mixed-targets-2979/verify.py --part controls  (PASS_LEVER_MIXED_TARGETS_2979_CONTROLS)
#   python3 -B research/lever-mixed-targets-2979/verify.py --instance 2979Fc --part main      (PASS_LEVER_MIXED_TARGETS_2979Fc_MAIN)
#   python3 -B research/lever-mixed-targets-2979/verify.py --instance 2979Fc --part controls  (PASS_LEVER_MIXED_TARGETS_2979Fc_CONTROLS)

Standard library only. On a clean clone at the base, with Python 3.12.3 on Linux: --check-only passes, the
registered replay passes in about 5 minutes (peak 0.28 GB) and leaves git diff --exit-code clean, the planner selects
only this package, the onboarding tests pass, check_research_commit.py --check-source-history passes, and the diff
against the base touches only this folder. The hosted checks will wait for maintainer approval.

Evidence inside the check: both words transported to the native canonical form and replayed exactly on all 632
columns in both orientations, lowered with residual widths equal to #2979's helper by helper, and seven wrong versions
of each rejected; the head test on all 271,728 FILL rows (every role in a window, no bin over its rank, global
profile = PROFILE.json); the price; the rate certificate on the half-cut profile derived from the measured heads,
equal to the histogram of the Lean rate module. For the headline A-fc the same checks run on its own table and paid
profile (fills/2979Fc/): the head test, the price under the full cut (jobs of 73 and 25) and the rate certificate
on its full-cut profile, which has no Lean rate module.

Failure controls: moving gate A4 before its climb leaves no heads; deleting gate C2 turns the 12,104 other rank-48
blocks into tails; the T74 regression finds the 11,010 heads of the first head test; the figure is refused with a
single head, with one head fewer (16,085), for a profile that is not separated, and one grid step above.

Lean (not run by this repository's checks): jacobalansussman/wht-power-saving-lean
at 563b4e6e913625637f36ba7869bf5fcd0dd4975a, for the full cut on #3945 with every head kept theorems OAI.PowerSaving.transform_mainL3945F and
OAI.PowerSaving.convolution_mainL3945F, exponent 1 - 17806935/10^10, axioms propext, Classical.choice,
Quot.sound only, one step stronger refused; the same for #3945 with every head kept (half cut) at 1.7581520e-3,
#2979 at 1.7556473e-3, #2979 with every head kept at 1.7564707e-3 and #3945 at 1.7501109e-3 (one package each,
README section 5). The official comparator, with the Lean kernel and nanoda, accepts it against OpenAI's statement at this exponent and rejects the statement one step stronger. Prepared for the Lean
leaderboard bigospeedrun.com/exact-dft as a pull request to bigospeedrun/verifier adding submissions/dft/jacobalansussman-lever-3945-full-cut (meant to be opened alongside this one; I will add its link and its robot's receipt as a comment once it is open). The package's
programs (tools/*.py) and network/ files equal, byte for byte, files of that commit (pairs of paths in SOURCES.json).

Checks not run: A-fc's instance in Lean; the cut in the community's eight-stream operator model; the outer step; the halving-guard question;
any κ assembly.

Credit

#2979 is Marius-Paul Dumitrean's (with substantial AI assistance, Anthropic Claude via Claude Code), on Jeremy Kothe's
#2957 / #2948 / #2966 rewrites, Mason Hale's #2917, Jeremy Diviney's #2908, Dugongue's #2969 / #2863 / #2839, Yiyang
Lu's #2857 / #2848, RossRichardson's #2918, Jeremy Kothe's #2894 / #2833, Tekalign's owner checker, icekylinx's
auditor, themilkman216's integrality observation and Gareth Davidson's #1995 / #2013. The borrowed helpers and warps
are Cinna Davis's (#2226), with Jeremy Kothe's width exchange (#2312); the T74 layout underneath is the work of Rohan
Arun, Marius-Paul Dumitrean, Jeremy Kothe, LeverRank, Thomas DiFiore, Jeremy Diviney, Chafik Boukhalfa and Vlado
Vojdanovski, and the T74 control data come from Jeremy Kothe's #1839. The second instance is Dugongue's #3945 (with substantial OpenAI Codex assistance, as its NOTICE says) and the
line it ends (dataisfire's #3734, zxv's #3682 and #3638, Ross Richardson's #3605, ChaloupeMusic's #3815, hexapode's
#3802 and #3875, and the earlier line its NOTICE names), with Chris R's (Clear1nsight's) audits #3969, #3988, #3994
and #4016; the table with every head kept was made with Erwan Secousses' (ChaloupeMusic's, #3815) allocation
programs that #3945 uses, and the headline's table A-fc with the same construction (its Hall model and reverse-time
placement, in a tolerant mode of mine) on #2979's files. tools/pricer.py re-implements the community's moment engine. The Lean route rests on Ryan Shea's
pipeline and Lean tree (from which network/Gates.lean is copied, Apache-2.0), Nil Mamano's extension, and OpenAI's
model and statement. New here: the lever (the half cut and the full cut with the split), Theorem 1G, the tables with every head kept, the
table A-fc (its class solution and the tolerant placement), my conversion and head test, the
rate certificate and the Lean proofs. The new files were written by AI agents (Claude) under my direction; no person outside this project has
reviewed them. Apache-2.0; NOTICE lists every copied file and its source.

Open next questions

README section Open next questions and TASK.json open_questions. The smallest useful follow-up is the replay of
the cut of a sample of heads in the community's exact eight-stream operator model (#3187's replay, as #4046 used),
with a control that a wrong cut changes the operator. Blocker: none. The largest is the outer step with two job
sizes; it needs a precise statement of the outer theorem's supplier hypotheses.

Workflow feedback (optional)

--print-card and the pin rules made the metadata easy to get right. What I missed is a documented way to bind a
proof that lives in another public Git repository (here a Lean proof): the package records the commit and a
byte-equality of the shared files, but no pin form covers it.

🤖 Generated with Claude Code

[jacobalansussman]

Update: A-fc is now proved in Lean, at 1.7887045e-3.

The headline of this pull request, the full cut on #2979's words with the table A-fc (fills/2979Fc/), is now proved in Lean. The theorem is OpenAI's statement for the DFT of every length, and for convolution (UniformFourier.lean of openai/math, family 130), in OpenAI's exact machine model, with the exponent 1 - 17887045/10^10: a saving of 1.7887045e-3. That is the point of the 10^-10 grid just below the price 1.7887045643e-3. The 1.7887046e-3 in the title of this pull request (#4268) is that price rounded to the nearest; it is a computed figure and is not proved in Lean. The rate fact is false there, and Lean proves that too.

What the proof covers. This pull request said that Theorem 1G and the general theorem of the full cut are proved in Lean, as used on #3945, and that A-fc's own instance is not. That instance is now in Lean as well:

• Lean's kernel checks the table of hosts of all 271,728 roles and counts its 16,576 heads (8,288 + 8,288); one head more is refused.
• The heads-first certificate on Conditional κ ≈ 0.0017290339826465: joint rank-7 end frames, five paired extractions and #2957's rewrites on #2942's words (+5.00e-6 over #2969) #2979's words holds with this table.
• The cut fact on Conditional κ ≈ 0.0017290339826465: joint rank-7 end frames, five paired extractions and #2957's rewrites on #2942's words (+5.00e-6 over #2969) #2979's words (the 48 directions of each head are the 48 lines that the cut removes) is proved. This pull request described it as argued from the template that Conditional κ ≈ 0.0017290339826465: joint rank-7 end frames, five paired extractions and #2957's rewrites on #2942's words (+5.00e-6 over #2969) #2979's words share with Raise conditional staged544 κ by filling idle owner slots #3945's.
• The rate fact holds at 17,887,045/10^10 and fails one unit higher.

#2979's words, order and dispatch enter the proof as data that Lean checks. The proof does not rest on the community's premises or on its moment engine; Theorem 1G has no halving condition.

Checks, each with its log in the package:

• The two theorems depend only on propext, Classical.choice and Quot.sound.
• tools/Compare.lean passes: the theorems are OpenAI's statement with only the exponent and seven names changed. The same comparison one unit stronger fails.
• The official comparator accepts the proof with nanoda and with Lean's kernel, and rejects the statement one unit stronger. It ran in a stand-in for its sandbox.
• An offline re-creation of the Big O Speedrun verifier's three phases accepts the merged form (449 files) and the unmerged one, and rejects the bound one unit higher. A separate check found the merged form identical to the unmerged one, theorem by theorem.
• Three AI agents, each with the sole job of refuting the result, re-checked it on other machines, with rebuilds and programs of their own. All three upheld it. No person has reviewed the Lean files line by line.

Where the files are. package/leverAFc in the sixth revision of my repository: https://github.com/jacobalansussman/wht-power-saving-lean/tree/86e575e28ed94890872dcff1bb2621d7ff559cbd/package/leverAFc. The theorems are OAI.PowerSaving.transform_mainL2979Fc and OAI.PowerSaving.convolution_mainL2979Fc in Work.FourierL2979Fc.Main. The package's README.txt lists every check with its log, and section 12 of the repository's VERIFY.md says how to build it over Ryan Shea's tree. KNOWN-ISSUES.txt lists the cosmetic points, and fill/ holds the same table as fills/2979Fc/ here (sha256 7fc766c6...).

Nothing in this pull request's files changes. Its registered checks, its claim (b for the DFT, no new κ) and its account of why the admission rejects A-fc at the strict-gain steps stay as they are.

I did this work with AI agents (Claude) under my direction.

[jacobalansussman]

The leaderboard pull request for the Lean proof of A-fc (1.7887045e-3, package/leverAFc of the sixth revision) is open: bigospeedrun/verifier#29. Its robot's verdict will appear there; I will link it here when it is in.