EPOCH：通过证据治理搜索实现可靠发现

# EPOCH: Reliable Discovery through Evidence-Governed Search
Source: [https://arxiv.org/html/2610.06986](https://arxiv.org/html/2610.06986)
Aisheng MoAffiliation:Zhejiang UniversityRuitong LiAffiliation:The University of Hong KongXinle DengAffiliation:Zhejiang University

###### Abstract

AI research agents are increasingly used to search over programs, mathematical constructions, and proofs\. However, existing systems typically optimize evaluator feedback without adequately governing how that feedback is interpreted, challenged, and reused\. As a result, promising but fragile candidates can be promoted as discoveries, while benchmark improvements, finite certificates, and theorem\-level claims are too easily conflated\. We introduce EPOCH, an evidence\-governed architecture designed to close this gap\. EPOCH implements an evidence\-governed discovery loop by combining explicit task contracts, typed memory, active falsification, admission checks, and independent replay, so that each candidate is evaluated against the strength and scope of the claim it supports\. EPOCH achieves state\-of\-the\-art aggregate performance on AlgoTune, substantially exceeding the strongest baseline in mean normalized score \(0\.65 vs\. 0\.53\), and attains the highest mean score on the internal Math14 suite \(0\.57\)\. It further shows favorable held\-out behavior under official\-test replay and leads the descriptive aggregate on AgentHPO\. Across ten discovery problems, EPOCH delivers substantial task\-specific advances, including improved executable constructions, optimized algorithms, counterexamples, and proof\-supported results\. These advances demonstrate its ability to convert search into concrete progress across mathematical and computational domains\. Together, the results suggest that evidence governance is a necessary step toward AI research agents that produce not only stronger solutions, but also more trustworthy scientific discoveries\.

## 1Introduction

AI research agents are increasingly being developed not only to solve well\-specified tasks, but also to generate candidate discoveries in code, algorithms, mathematics, and science\. Recent systems have demonstrated this potential across games, program synthesis, tensor decompositions, geometric constructions, formal proofs, and scientific screening\([Silver et al\., 2018](https://arxiv.org/html/2610.06986#bib.bib25);[Schrittwieser et al\., 2020](https://arxiv.org/html/2610.06986#bib.bib24);[Li et al\., 2022](https://arxiv.org/html/2610.06986#bib.bib16);[Fawzi et al\., 2022](https://arxiv.org/html/2610.06986#bib.bib7);[Trinh et al\., 2024](https://arxiv.org/html/2610.06986#bib.bib27);[Hubert et al\., 2025](https://arxiv.org/html/2610.06986#bib.bib12);[Merchant et al\., 2023](https://arxiv.org/html/2610.06986#bib.bib18)\)\. FunSearch and AlphaEvolve further show that evaluator\-guided evolution can transform large language models into effective engines for open\-ended search\([Romera\-Paredes et al\., 2024](https://arxiv.org/html/2610.06986#bib.bib23);[Novikov et al\., 2025](https://arxiv.org/html/2610.06986#bib.bib19)\)\. Despite this progress, current systems are primarily designed to generate and optimize candidates, rather than to construct the evidence needed to support a discovery\. A promising program, construction, or conjecture is only a starting point: establishing its value may require identifying a mechanism, producing a counterexample to a competing explanation, checking a finite certificate, or distinguishing an experimentally supported observation from a proof\-backed claim\. These supporting objects are often generated, tested, and recorded only opportunistically\. As a result, an agent may return an improved candidate without a clear account of why it works, what evidence supports it, or how that evidence can be independently revisited\. The central challenge is therefore to couple search with an explicit process for constructing, challenging, and retaining the evidence that turns promising candidates into supported discoveries\.

Existing agents combine generation with execution, testing, or verification, but they do not provide a common protocol for this evidence\-construction process across domains\. We ask:*what protocol should govern the promotion of a candidate into a retained discovery when the required supporting evidence differs across tasks?*For code, this may involve semantic checks, resource measurements, and held\-out replay; for algebra, exact identities, constructions, or obstruction witnesses; and for theorem discovery, computational evidence and formal proof with distinct scopes\. A scalar reward can guide a search procedure toward better candidates, but it cannot by itself organize the generation of supporting evidence, specify the scope of a claim, or preserve the failed attempts that may explain or challenge it\.

We proposeEPOCH\(Evidence\-conditioned Proposal Optimization through Cumulative Hypothesis\-governance, Fig\.[1](https://arxiv.org/html/2610.06986#S1.F1)\), an evidence\-governed architecture that frames discovery as constrained search over an explicit evidence ledger\. Each task begins with a contract specifying permissible edits, applicable checks, resource limits, and the scope of admissible claims\. Typed memory retains both successful and failed trials, allowing later search to reuse supporting evidence and avoid known failure modes\. Candidates are actively challenged against their declared mechanisms, admitted only when their support satisfies the task contract, and independently replayed after the search endpoint is frozen\. Rather than making a verifier complete or elevating finite evidence into a general theorem,EPOCHprovides a domain\-general protocol that aligns each retained result with its supporting evidence and makes the limits of that support explicit\.

Figure 1:EPOCHcouples discovery search to an explicit evidence ledger\. Successful and failed trials enter typed memory; failures are fed back into search for repair and refinement \(red loop\)\. Challenge, admission, and independent replay determine whether a candidate is retained, while the task contract fixes the checks, budget, and claim scope governing that decision\.Our contributions are:

- •Evidence\-governed discovery\.We introduce a domain\-general architecture in which task contracts, typed memory, active falsification, claim\-aware admission, and independent replay jointly govern how candidate solutions become retained results\.
- •Strong exploration and exploitation performance\.EPOCHachieves state\-of\-the\-art aggregate performance on AlgoTune, the highest mean score on internal Math14, favourable official\-test replay behaviour, and the leading descriptive aggregate on AgentHPO\.
- •Major discoveries with scoped evidence\.Across ten discovery problems,EPOCHdelivers eleven improved tensor border\-rank upper bounds, including an explicit 30\-path construction forTss444T\_\{\\rm ss444\}; a reusable uniform Big\-centroid construction; a record\-setting 54\-comparison executable procedure for median\-of\-23 selection; a 1,512\-gate \(14\.10%14\.10\\%\) matched\-PyZX T\-count reduction for AES; a Lean\-checked all\-dimensional hypercube determinant inequality with complete equality classification; and a Lean\-checked nine\-element counterexample to the proposedHβH\_\{\\beta\}coefficient ordering, extended to an infinite family\.

## 2Related Work

##### Evaluator\-Guided Search and Discovery\.

AlphaCode generates programs at scale and filters, clusters, and reranks them according to their behavior on generated test inputs, whereas AlphaTensor formulates matrix\-multiplication algorithm discovery as a search for low\-rank decompositions of the matrix\-multiplication tensor\([Li et al\., 2022](https://arxiv.org/html/2610.06986#bib.bib16);[Fawzi et al\., 2022](https://arxiv.org/html/2610.06986#bib.bib7);[Google DeepMind, 2022](https://arxiv.org/html/2610.06986#bib.bib8)\)\. FunSearch couples language\-model proposals to evolutionary selection, and AlphaEvolve extends evaluator\-guided evolution to mathematical and computational tasks\([Romera\-Paredes et al\., 2024](https://arxiv.org/html/2610.06986#bib.bib23);[Novikov et al\., 2025](https://arxiv.org/html/2610.06986#bib.bib19)\)\. OpenEvolve, AdaEvolve, and AI\-Scientist further broaden the landscape of evolutionary and end\-to\-end research workflows\([OpenEvolve contributors, 2026](https://arxiv.org/html/2610.06986#bib.bib21);[Cemri et al\., 2026](https://arxiv.org/html/2610.06986#bib.bib5);[Lu et al\., 2024](https://arxiv.org/html/2610.06986#bib.bib17);[Yamada et al\., 2025](https://arxiv.org/html/2610.06986#bib.bib28)\)\. These systems establish the effectiveness of evaluator\-guided search;EPOCHcomplements them by introducing an evidence contract that governs which candidates may be retained as discoveries, what support their claims require, and how rejected paths remain available for subsequent search\.

##### Domain\-Specific Evidence for Discovery\.

AlphaGeometry combines learned construction with symbolic deduction, AlphaProof searches formally checkable Lean states, and GNoME couples learned screening to first\-principles calculations\([Trinh et al\., 2024](https://arxiv.org/html/2610.06986#bib.bib27);[Google DeepMind, 2024](https://arxiv.org/html/2610.06986#bib.bib10);[Hubert et al\., 2025](https://arxiv.org/html/2610.06986#bib.bib12);[Merchant et al\., 2023](https://arxiv.org/html/2610.06986#bib.bib18);[Google DeepMind, 2023](https://arxiv.org/html/2610.06986#bib.bib9)\)\. Their domain\-specific validators are essential rather than interchangeable\. Recent AI\-assisted mathematical studies likewise combine model\-guided exploration with expert scrutiny and, where applicable, formal verification, while distinguishing suggestive evidence from established mathematical claims\([Anthropic, 2026](https://arxiv.org/html/2610.06986#bib.bib3);[OpenAI, 2026](https://arxiv.org/html/2610.06986#bib.bib20)\)\.EPOCHtherefore does not seek to replace specialist validation with a universal truth score; instead, it standardizes how domain\-specific outputs support discovery\. Typed receipts bind a retained result to the checks that produced its evidence, three\-valued gates distinguish supported, refuted, and unresolved candidates, and independent replay tests frozen artifacts outside the search loop\. The result is a replayable admission record that specifies what was checked, what outcome was obtained, and which claim the available evidence permits\.

## 3Evidence\-Governed Discovery

We organize the protocol around three decisions: what counts as an admissible endpoint, how evidence changes subsequent proposals, and what may be claimed after independent replay\.

### 3\.1Task contract and admissible endpoints

A task contract is𝒞=\(Dpub,Dterm,E,B,A,S\)\\mathcal\{C\}=\(D\_\{\\rm pub\},D\_\{\\rm term\},E,B,A,S\): public and terminal data views, evaluators, resource budget, editable artifact space, and allowed claim scope\. A candidatecchas objectiveq𝒞​\(c\)q\_\{\\mathcal\{C\}\}\(c\)and evidence bundleξ\\xi; a claimσ\\sigmastates what the result asserts\. Endpoint selection is

\(c∗,ξ∗,σ∗\)∈arg⁡maxc,ξ,σ​q𝒞​\(c\)s\.t\.c∈A,uj\(c,ξ\)≤Bj,CorrectE\(c;ξ\)=1,Challenge\(c;ξ\)=1,ReplayE\(c;ξ\)=1,Supports\(ξ,σ\)=1,Scope\(σ\)⊆S\.\\begin\{gathered\}\(c^\{\*\},\\xi^\{\*\},\\sigma^\{\*\}\)\\in\\arg\\max\_\{c,\\xi,\\sigma\}\\ q\_\{\\mathcal\{C\}\}\(c\)\\\\ \\begin\{aligned\} \\text\{s\.t\.\}\\quad&c\\in A,\\quad u\_\{j\}\(c,\\xi\)\\leq B\_\{j\},\\\\ &\\operatorname\{Correct\}\_\{E\}\(c;\\xi\)=1,\\quad\\operatorname\{Challenge\}\(c;\\xi\)=1,\\\\ &\\operatorname\{Replay\}\_\{E\}\(c;\\xi\)=1,\\quad\\operatorname\{Supports\}\(\\xi,\\sigma\)=1,\\quad\\operatorname\{Scope\}\(\\sigma\)\\subseteq S\.\\end\{aligned\}\\end\{gathered\}\(1\)The maximization ranges only over proposals generated within the registered run, including a verified fallback when supplied\. It is not a global optimum over all programs or proofs\. Gates take values in\{1,0,⊥\}\\\{1,0,\\bot\\\}, where⊥\\botdenotes unresolved evidence; only 1 permits admission\.

### 3\.2Evidence memory, falsification, and phase control

At steptt, the state isst=\(ct∗,Mt,zt,bt\)s\_\{t\}=\(c\_\{t\}^\{\*\},M\_\{t\},z\_\{t\},b\_\{t\}\): incumbent, append\-only memory, phase, and remaining resources\. The proposal policy emits

at=\(ct,Ht,δ^t,Rt,Ft\)∼πθ\(⋅∣𝒞,𝒱\(Mt\),zt,bt\),a\_\{t\}=\(c\_\{t\},H\_\{t\},\\widehat\{\\delta\}\_\{t\},R\_\{t\},F\_\{t\}\)\\sim\\pi\_\{\\theta\}\(\\cdot\\mid\\mathcal\{C\},\\mathcal\{V\}\(M\_\{t\}\),z\_\{t\},b\_\{t\}\),\(2\)containing a candidate, hypothesis, predicted effect, evidence references, and intended falsifier\. The bounded view𝒱⁡\(Mt\)\\mathcal\{V\}\(M\_\{t\}\)exposes relevant prior evidence without rewriting the ledger\. Each observation records artifact and evaluator hashes, score, correctness, resource use, failure attribution, and rejection reason\. Scientific failure can therefore constrain a later proposal, whereas an infrastructure incident can trigger bounded recovery without masquerading as evidence against the method\.

A challenge targets the stated mechanism rather than merely repeating the objective\. Examples include semantic boundary inputs, an algebraic coefficient mismatch, a cokernel witness, counterexample search, or a proof obligation\. Passing a finite challenge supports only its declared coverage\. The controller chooses among explore, refine, recover, and finalize; it does not imply an unreported learned optimal schedule\. If𝒜t\\mathcal\{A\}\_\{t\}contains candidates whose applicable gates pass, the retained endpoint satisfiesct∗∈arg⁡maxc∈𝒜t​q𝒞​\(c\)c\_\{t\}^\{\*\}\\in\\arg\\max\_\{c\\in\\mathcal\{A\}\_\{t\}\}q\_\{\\mathcal\{C\}\}\(c\)\. With a verified fallback, this gives a protocol\-level safety invariant, not correctness beyond evaluator coverage\.

### 3\.3Replay and claim sealing

Terminal replay evaluates a frozen selected endpoint and cannot feed back into selection\. A sealed result binds the contract, endpoint, ledger, evidence, claim, and scope:

Seal=h⁡\(𝒞,c∗,MT,ξ∗,σ∗,S\)\.\\operatorname\{Seal\}=h\(\\mathcal\{C\},c^\{\*\},M\_\{T\},\\xi^\{\*\},\\sigma^\{\*\},S\)\.\(3\)Independent implementations may reconstruct semantics rather than rerun the same checker\. For mathematical outputs, the bundle distinguishes finite computation, general argument, formal kernel, and missing bridge\.

## 4Evaluation

We first compare endpoint quality and held\-out behavior, then examine component removals and the distribution of performance across tasks\. The discovery audit in Section[5](https://arxiv.org/html/2610.06986#S5)asks a separate question: what reusable objects and bounded claims emerge from this process?

### 4\.1Benchmarks and Estimands

We evaluateEPOCHin three complementary settings: AlgoTune for constrained algorithmic search, Math14 for diverse mathematical objectives with exact endpoint checkers, and six AgentHPOBench tasks for component ablations\([AlgoTune contributors, 2026](https://arxiv.org/html/2610.06986#bib.bib1);[OpenMOSS, 2026](https://arxiv.org/html/2610.06986#bib.bib22)\)\. On a frozen 12\-task AlgoTune subset, five methods receive the same budget of 48 semantic calls and are run with three seeds; we report mean task scores and their macro\-average\. To test whether search\-time gains transfer beyond development data, we freeze each eligible final program and replay it, without further search or adaptation, on 32 previously unused official test inputs\. This replay reruns correctness checks and fresh\-process timing\. Math14 evaluates performance across 14 mathematical tasks, whereas AgentHPO isolates the contribution of EPOCH’s individual components\. Full task\-level results, seeds, measurements, and statistical procedures are provided in the Supplement\.

### 4\.2Search Performance and Held\-Out Robustness

EPOCHachieves the highest AlgoTune development mean \(Table[1](https://arxiv.org/html/2610.06986#S4.T1)\), reaching 0\.65 and surpassing the strongest baseline, AdaEvolve, by22\.60%22\.60\\%\. It also exceeds both AI\-Scientist variants and OpenEvolve by margins ranging from24\.80%24\.80\\%to30\.90%30\.90\\%, establishing the strongest aggregate performance among the evaluated methods\. This advantage extends to the held\-out official\-test replay: after endpoints are frozen and evaluated without further search or adaptation, EPOCH has positive mean effects against all four baselines\. Maximum common subgraph retains a\+0\.48\+0\.48normalized\-score advantage and Convolve2D a\+0\.24\+0\.24advantage, although NMF reverses to−0\.27\-0\.27\. The largest development gains occur on Convolve2D, maximum common subgraph, Robertson ODE, NMF, and zeta\-zero count, reflecting task\-specific improvements to the evaluated executable endpoints under the benchmark protocol\.

Table 1:AlgoTune scores\. Development uses 12 tasks and three seeds per method; replay effects use seven official\-test tasks\. Higher scores are better\. Relative gain is measured against the named method’s development score\. Replay effects areEPOCHminus the named baseline in normalized\-score units; the development and replay columns use distinct endpoint populations\.On Math14 \(Table[2](https://arxiv.org/html/2610.06986#S4.T2)\),EPOCHachieves the highest mean score of 0\.57, outperforming every evaluated baseline\. Its relative improvement ranges from0\.60%0\.60\\%over OpenEvolve to10\.90%10\.90\\%over AI\-Scientist v1, demonstrating that EPOCH’s evidence\-governed search architecture transfers effectively from executable optimization to diverse mathematical objectives\.

Table 2:Math14 internal transfer scores over 14 objectives\. Higher scores are better; relative gains are measured against the named baseline\.
### 4\.3Component contributions and task\-level trade\-offs

Whereas the main benchmarks compare complete systems, six AgentHPOBench tasks allow us to isolate the contributions ofEPOCH’s major components\. Because these tasks use heterogeneous metrics, task\-level raw scores remain the primary results\. For descriptive cross\-task comparison, we normalize each task\-level meanzt​vz\_\{tv\}within its task, accounting for whether the task metric is maximized or minimized:

Nt​v=100​zt​v−minv′⁡zt​v′maxv′⁡zt​v′−minv′⁡zt​v′,N¯v=16​∑tNt​v\.N\_\{tv\}=100\\frac\{z\_\{tv\}\-\\min\_\{v^\{\\prime\}\}z\_\{tv^\{\\prime\}\}\}\{\\max\_\{v^\{\\prime\}\}z\_\{tv^\{\\prime\}\}\-\\min\_\{v^\{\\prime\}\}z\_\{tv^\{\\prime\}\}\},\\qquad\\bar\{N\}\_\{v\}=\\frac\{1\}\{6\}\\sum\_\{t\}N\_\{tv\}\.\(4\)Thus,N¯v\\bar\{N\}\_\{v\}summarizes the relative performance of each variant across the six tasks without conflating their native metrics\.

Table 3:Ablations on six AgentHPOBench tasks\. FullEPOCHachieves the highest descriptive normalized mean\. Removing any component reduces this mean by 13\.17–55\.59 points\. W/T/L denotes the task\-level record of FullEPOCHagainst each ablation in the paired report\.FullEPOCHachieves both the highest normalized mean \(Table[3](https://arxiv.org/html/2610.06986#S4.T3)\) and the best mean task rank \(1\.67\)\. Removing memory lowers the normalized mean by 13\.17 points, while removing proof admission, falsification, or phase control produces larger reductions of 37\.28, 41\.75, and 55\.59 points, respectively\. The paired comparisons likewise favor the complete system over every ablation, including a 6/0/0 record against the variant without proof admission\. The no\-memory variant performs better on ART and ModernBERT, consistent with an exploration–exploitation trade\-off: unconstrained proposals can benefit short\-horizon tuning on individual tasks, whereas memory improves performance across the broader suite by preserving evidence and steering search away from previously unsuccessful regions\. This pattern highlights the complementary roles of EPOCH’s components rather than a uniform per\-task effect\. The broader findings are supported independently: AlgoTune and Math14 evaluate the complete architecture end to end, while the case\-study results are established through task\-specific certificates and replay\. Overall, the complete architecture achieves the strongest performance across the broadest range of tasks\.

Figure 2:Performance trade\-offs across AgentHPOBench ablations\.a, FullEPOCHachieves the highest normalized mean, whereas the no\-memory variant attains the highest minimum task score; the dashed segment connects the observed nondominated variants\.b, Task\-level decomposition of the 13\.17\-point normalized\-mean gap between FullEPOCHand the no\-memory variant\. Contributions sum to the aggregate gap\.##### From average performance to task coverage\.

Performance profiles test whether aggregate gains extend across tasks rather than arising from a small number of outliers\. On AlgoTune,EPOCHscores at least0\.600\.60on five of twelve tasks, compared with at most one task for any baseline\. On AgentHPOBench, it reaches a normalized score of at least8080on three of six tasks, compared with at most two for any ablation\. The advantage of the complete system therefore extends beyond its mean score to broader coverage of high\-performing tasks\.

Figure 3:Empirical performance profiles,Pv​\(τ\)=\|\{t:st​v≥τ\}\|/TP\_\{v\}\(\\tau\)=\|\\\{t:s\_\{tv\}\\geq\\tau\\\}\|/T, showing the fraction of tasks on which variantvvreaches thresholdτ\\tau\. Higher curves indicate broader coverage at a given performance level\. Left, twelve AlgoTune development tasks\. Right, six AgentHPOBench tasks, using task\-level means normalized as in Eq\. \(4\)\. The panels use different score scales\.

## 5From Search to Discovery: Case Studies

The benchmark results establish EPOCH’s search performance; we next examine the discoveries that this search produces\. The following ten case studies span executable optimization, algorithmic construction, formal statements, and counterexamples, illustrating how EPOCH couples candidate generation with task\-specific evidence\. Figure[4](https://arxiv.org/html/2610.06986#S5.F4)highlights four representative outcomes, while Table[4](https://arxiv.org/html/2610.06986#S5.T4)summarizes the retained results, their supporting evidence, and the scope of each claim\. We begin with executable constructions and repair, and then turn to formal results and counterexamples; complete derivations are provided in the supplementary\.

Figure 4:Four discovery cases, left to right\. Hyperfactor reuses one factor across outputs, reducing circuit cost\. The median has eleven smaller and eleven larger elements; branch repair yields the comparison bound\. Full cube support gives a strict inequality; facet support gives equality \(filled vertices: positive weight\)\. H\-beta violates the proposed coefficient ordering\. Schematics are not emitted circuits or decision trees; Table[4](https://arxiv.org/html/2610.06986#S5.T4)records evidence boundaries\.Table 4:Documented discovery outcomes and their evidential scope\.### 5\.1Constructive Discoveries and Algorithmic Optimization

##### Characteristic\-two tensor transfer\.

Low\-border\-rank decompositions are fundamental building blocks for fast bilinear algorithms: each explicit construction provides a concrete certificate of reduced algebraic complexity\. A central difficulty is that rational decompositions can collapse after reduction to characteristic two, preventing their direct use over the target field\.EPOCHturns this obstruction into a constructive search signal: it extracts the incompatible coefficient constraints, uses their witnesses to select a new degeneration chart, and searches for a valid characteristic\-two replacement\. Across the audit, this procedure transfers all 43 directly applicable formulas and covers 24 coordinate\-distinct targets, yielding eleven improved border bounds\. In particular, it discovers a 30\-path construction forTss444T\_\{\\rm ss444\}, establishingR¯⁡\(Tss444\)≤30\\brank\(T\_\{\\rm ss444\}\)\\leq 30\. The result contributes explicit low\-complexity decompositions in a regime where naïve transfer fails, expanding the constructive toolkit available for algebraic\-complexity and fast\-algorithm design\.

##### Uniform Big\-centroid construction\.

Big\-centroid constructions are particularly valuable when they extend across a family of dimensions: unlike an isolated decomposition, a uniform family can serve as a reusable object for asymptotic border\-rank and algebraic\-complexity analysis\.EPOCHdiscovers such a family, deriving an explicitq\+u1q\+u\_\{1\}\-term construction, whereq=∏s=2dusq=\\prod\_\{s=2\}^\{d\}u\_\{s\}, from a reusable left\-inverse identity rather than repeated ambient linear solves\. The resulting formula applies throughout the stated parameter and field regimes, replacing a sequence of instance\-specific searches with a single dimension\-general construction\. This shift from individual examples to an explicit scalable family provides a concrete foundation for studying the associated complexity bounds and for developing subsequent centroid\-based tensor constructions\.

##### Improved median\-of\-23 selection\.

Median selection is a fundamental problem in comparison complexity, and the classical Hadian–Sobel construction gives a 55\-comparison upper bound for selecting the median of 23 elements\([Hadian & Sobel, 1969](https://arxiv.org/html/2610.06986#bib.bib11)\)\.EPOCHimproves on this benchmark by treating over\-budget execution paths as reusable counterexamples: it organizes 1,454 difficult cases into sixteen repair policies that eliminate the remaining excess comparisons\. The resulting executable decision procedure has worst\-case cost at most 54 comparisons, establishingV12​\(23\)≤54V\_\{12\}\(23\)\\leq 54and improving the classical bound by one comparison\. This result demonstrates that failure\-guided search can produce a concrete improvement to a long\-standing constructive benchmark in exact selection\.

##### Reversible circuit factor sharing\.

T gates are a dominant resource in fault\-tolerant quantum computation, making T\-count reduction a central objective in reversible\-circuit optimization\([Kissinger & van de Wetering, 2020](https://arxiv.org/html/2610.06986#bib.bib15)\)\. In the evaluated AES construction, common intermediate factors are computed independently for multiple outputs, introducing substantial redundant non\-Clifford cost\.EPOCHidentifies these factors and restructures the circuit so that each is computed once, shared across the relevant outputs, and subsequently uncomputed\. Figure[5](https://arxiv.org/html/2610.06986#S5.F5)illustrates this mechanism and shows how the relative saving increases with the number of factor uses\. Under matched PyZX synthesis, the resulting circuit reduces the T\-count from 10,746 to 9,234, eliminating 1,512 T gates and lowering the non\-Clifford cost by14\.10%14\.10\\%, while preserving all 256 input\-output cases and restoring every ancilla\. This result provides a substantial resource reduction for a cryptographically relevant reversible circuit under the stated library and synthesis model\.

![Refer to caption](https://arxiv.org/html/2610.06986v1/case_hyperfactor_model.png)Figure 5:Factor sharing and its cost scaling\. A shared factor is computed once, reused acrosskkoutputs, and then uncomputed\. With opening costccand per\-use costuu, the relative saving is\(k−1\)​c/\[k⁡\(c\+u\)\]\(k\-1\)c/\[k\(c\+u\)\]and increases with the number of uses\. The pseudocode preserves the input and restores the ancilla\.

### 5\.2Mathematical Discoveries

The remaining cases distinguish a checked general statement, an explicit counterexample, and theorem candidates with open proof bridges\.

##### A sharp hypercube inequality with equality characterization\.

Letwv≥0w\_\{v\}\\geq 0assign weights to the verticesv∈\{0,1\}dv\\in\\\{0,1\\\}^\{d\}, letW=∑vwvW=\\sum\_\{v\}w\_\{v\}, and letmi,b=∑vi=bwvm\_\{i,b\}=\\sum\_\{v\_\{i\}=b\}w\_\{v\}denote the mass on thebb\-facet in coordinateii\. For the unordered weighted sumSD⁡\(w\)\\operatorname\{SD\}\(w\)of absolute affine simplex determinants, EPOCH establishes

SD⁡\(w\)​Wd−1≤∏i=1dmi,0​mi,1\.\\operatorname\{SD\}\(w\)W^\{d\-1\}\\leq\\prod\_\{i=1\}^\{d\}m\_\{i,0\}m\_\{i,1\}\.\(5\)
Ford≥3d\\geq 3, equality holds exactly when all mass is supported on a facet\. Thus coordinate marginals sharply bound the global determinant quantity and characterize its degeneracies\. Relating this finite\-polynomial theorem to the source geometric statement still requires the stated normalization bridge\([Averkov et al\., 2026](https://arxiv.org/html/2610.06986#bib.bib4)\)\.

##### A stable counterexample toHβH\_\{\\beta\}front\-loading\.

The proposed rank\-fiveHβH\_\{\\beta\}front\-loading property requiresh2β≥h3βh\_\{2\}^\{\\beta\}\\geq h\_\{3\}^\{\\beta\}\. EPOCH discovers a nine\-element matroid with

H0=\(1,9,27,27,9,1\),Hβ=\(1,9,31,32,9,1\),H\_\{0\}=\(1,9,27,27,9,1\),\\qquad H\_\{\\beta\}=\(1,9,31,32,9,1\),\(6\)and henceh2β−h3β=−1h\_\{2\}^\{\\beta\}\-h\_\{3\}^\{\\beta\}=\-1, directly refuting the ordering\. A two\-line principal\-extension mechanism preserves the defect for every nonnegative extension count, producing an infinite family while leaving neighboring conjectures unresolved\([Sinclair, 2026](https://arxiv.org/html/2610.06986#bib.bib26)\)\.

##### Additional Mathematical Results and Verification Boundaries\.

Four further candidates concern a three\-state kernel, Full Perazzo ranks, a Heisenberg limit\([Kammeyer, 2026](https://arxiv.org/html/2610.06986#bib.bib13)\), and online\-embedding asymptotics\([Altschuler et al\., 2026](https://arxiv.org/html/2610.06986#bib.bib2)\)\. Table[4](https://arxiv.org/html/2610.06986#S5.T4)summarizes their verified cores and the remaining bridges: boundary certificates, interpolation and rank arguments, representation limits, and recurrence asymptotics\. Full details appear in the supplement\.

## 6Discussion and Limitations

The benchmarks and portfolio support complementary conclusions\. Aggregate gains show that contracts, typed memory, falsification, admission, and replay can guide search, while the cases show how failures become repair strategies and verification turns candidates into scoped research artifacts\. This evidence discipline is particularly relevant to AI4Math and AI4Science workflows combining code, symbolic reasoning, simulation, and formal methods\.

Two limitations define the next frontier\. First, larger paired evaluations with fixed budgets and comprehensive resource accounting are needed\. Second, although EPOCH makes evidential gaps explicit, it does not resolve them all; specialist claims still require external review, statement alignment, and priority assessment\. Extending the protocol to simulations, experiments, databases, scientific instruments, and expert interaction remains an important direction\.

## 7Conclusion

EPOCHreframes AI research agents from candidate generators into systems for evidence\-guided discovery\. By combining typed memory, active falsification, admission, and independent replay, EPOCH turns successful, failed, and repaired search trajectories into retained results with explicit supporting evidence\. Across ten discovery problems, this process yields concrete advances: eleven improved tensor border bounds, a 1,512\-T\-gate reduction in an AES reversible circuit, a 54\-comparison median\-of\-23 procedure that improves the classical 55\-comparison Hadian–Sobel bound\([Hadian & Sobel, 1969](https://arxiv.org/html/2610.06986#bib.bib11)\), a sharp all\-dimensional hypercube inequality with an equality characterization, and an infinite family refuting the proposedHβH\_\{\\beta\}front\-loading property\. Together with state\-of\-the\-art aggregate results on AlgoTune and leading performance on Math14 and AgentHPO, these outcomes show that evidence\-governed search can do more than optimize benchmark scores: it can generate substantive algorithmic and mathematical discoveries\.

## AI Use Statement

Generative AI tools were used to assist with manuscript polishing and with the development of candidate programs, constructions, mathematical arguments, and proofs\. The authors reviewed all AI\-assisted outputs\. Executable results were checked through task\-specific evaluators and independent replay; finite mathematical claims were verified by exact or exhaustive computation; and formal results were checked in Lean where indicated\. The authors take full responsibility for the final text, claims, code, and mathematical artifacts\.

## Reproducibility Statement

The supplementary material provides the information needed to audit and reproduce our reported results\. For the empirical evaluations, it records frozen implementation status, task cohorts and data splits, model and seed identifiers, search budgets, correctness and timing procedures, endpoint\-selection and held\-out replay protocols, and task\-level results\. For the discovery cases, it includes detailed derivations, exact or exhaustive verification procedures, formalization scopes, outstanding proof obligations, and documented replay interfaces\. All claims are restricted to the scope established by the corresponding evidence; in particular, finite certificates and formally verified kernels are not presented as establishing broader results\.

## References

- AlgoTune contributors \(2026\)AlgoTune contributors\.AlgoTune: Official task repository, 2026\.URL[https://github\.com/oripress/AlgoTune](https://github.com/oripress/AlgoTune)\.Pinned task and data revisions are reported in the supplementary material; accessed September 17, 2026\.
- Altschuler et al\. \(2026\)Dylan J\. Altschuler, Quentin Dubroff, and Konstantin Tikhomirov\.Online permutation embedding: Optimal stopping and scaling laws\.*arXiv preprint arXiv:2608\.19050*, 2026\.URL[https://arxiv\.org/abs/2608\.19050](https://arxiv.org/abs/2608.19050)\.
- Anthropic \(2026\)Anthropic\.Learning more about Claude’s mathematical capabilities, August 2026\.URL[https://www\.anthropic\.com/research/riemann\-zeta](https://www.anthropic.com/research/riemann-zeta)\.Primary research announcement, August 10; revised August 13, 2026\. Reports a lower bound for the proportion of critical\-line zeros, not a proof of the Riemann hypothesis\. Accessed September 18, 2026\.
- Averkov et al\. \(2026\)Gennadiy Averkov, Katherina von Dichter, and Ivan Soprunov\.On the log\-submodularity for zonoids: from mixed volume inequalities to the hypercube\.*arXiv preprint arXiv:2608\.14909*, 2026\.URL[https://arxiv\.org/abs/2608\.14909](https://arxiv.org/abs/2608.14909)\.
- Cemri et al\. \(2026\)Mert Cemri, Shubham Agrawal, Akshat Gupta, Shu Liu, Audrey Cheng, Qiuyang Mang, Ashwin Naren, Lutfi Eren Erdogan, Koushik Sen, Matei Zaharia, Alex Dimakis, and Ion Stoica\.AdaEvolve: Adaptive LLM driven zeroth\-order optimization\.*arXiv preprint arXiv:2602\.20133*, 2026\.URL[https://arxiv\.org/abs/2602\.20133](https://arxiv.org/abs/2602.20133)\.
- Dörrer et al\. \(2025\)Josua Dörrer, Konrad Gendle, Johanna Betz, Julius von Smercek, Andreas Steding, and Florian Stober\.Exact lower bounds for the number of comparisons in selection\.In*23rd International Symposium on Experimental Algorithms \(SEA 2025\)*, 2025\.doi:10\.4230/LIPIcs\.SEA\.2025\.16\.URL[https://drops\.dagstuhl\.de/entities/document/10\.4230/LIPIcs\.SEA\.2025\.16](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2025.16)\.
- Fawzi et al\. \(2022\)Alhussein Fawzi et al\.Discovering faster matrix multiplication algorithms with reinforcement learning\.*Nature*, 610:47–53, 2022\.doi:10\.1038/s41586\-022\-05172\-4\.URL[https://doi\.org/10\.1038/s41586\-022\-05172\-4](https://doi.org/10.1038/s41586-022-05172-4)\.
- Google DeepMind \(2022\)Google DeepMind\.AlphaTensor: Published algorithms and verification artifacts, 2022\.URL[https://github\.com/google\-deepmind/alphatensor](https://github.com/google-deepmind/alphatensor)\.Accessed September 18, 2026\.
- Google DeepMind \(2023\)Google DeepMind\.Materials discovery: GNoME research artifacts, 2023\.URL[https://github\.com/google\-deepmind/materials\_discovery](https://github.com/google-deepmind/materials_discovery)\.Accessed September 18, 2026\.
- Google DeepMind \(2024\)Google DeepMind\.AlphaGeometry: Code and model artifacts, 2024\.URL[https://github\.com/google\-deepmind/alphageometry](https://github.com/google-deepmind/alphageometry)\.Accessed September 18, 2026\.
- Hadian & Sobel \(1969\)Abdollah Hadian and Milton Sobel\.Selecting thett\-th largest using binary errorless comparisons\.Technical Report Technical Report 121, School of Statistics, University of Minnesota, 1969\.URL[https://hdl\.handle\.net/11299/199105](https://hdl.handle.net/11299/199105)\.
- Hubert et al\. \(2025\)Thomas Hubert et al\.Olympiad\-level formal mathematical reasoning with reinforcement learning\.*Nature*, 2025\.doi:10\.1038/s41586\-025\-09833\-y\.URL[https://www\.nature\.com/articles/s41586\-025\-09833\-y](https://www.nature.com/articles/s41586-025-09833-y)\.
- Kammeyer \(2026\)Holger Kammeyer\.A counterexample to the determinant approximation conjecture\.*arXiv preprint arXiv:2609\.15567*, 2026\.URL[https://arxiv\.org/abs/2609\.15567](https://arxiv.org/abs/2609.15567)\.
- Kassabov et al\. \(2026\)Martin Kassabov, J\. M\. Landsberg, Victor Souza, and Philip Speegle\.Disjoint and nearly disjoint sums of matrix multiplication tensors and their centroids\.*arXiv preprint arXiv:2608\.27434*, 2026\.URL[https://arxiv\.org/abs/2608\.27434](https://arxiv.org/abs/2608.27434)\.
- Kissinger & van de Wetering \(2020\)Aleks Kissinger and John van de Wetering\.Reducing T\-count with the ZX\-calculus\.*Physical Review A*, 102\(2\):022406, 2020\.doi:10\.1103/PhysRevA\.102\.022406\.
- Li et al\. \(2022\)Yujia Li et al\.Competition\-level code generation with AlphaCode\.*Science*, 378:1092–1097, 2022\.doi:10\.1126/science\.abq1158\.URL[https://arxiv\.org/abs/2203\.07814](https://arxiv.org/abs/2203.07814)\.
- Lu et al\. \(2024\)Chris Lu et al\.The AI Scientist: Towards fully automated open\-ended scientific discovery\.*arXiv preprint arXiv:2408\.06292*, 2024\.URL[https://arxiv\.org/abs/2408\.06292](https://arxiv.org/abs/2408.06292)\.
- Merchant et al\. \(2023\)Amil Merchant, Simon Batzner, Samuel S\. Schoenholz, Muratahan Aykol, Gowoon Cheon, and Ekin Dogus Cubuk\.Scaling deep learning for materials discovery\.*Nature*, 624:80–85, 2023\.doi:10\.1038/s41586\-023\-06735\-9\.URL[https://www\.nature\.com/articles/s41586\-023\-06735\-9](https://www.nature.com/articles/s41586-023-06735-9)\.
- Novikov et al\. \(2025\)Alexander Novikov et al\.AlphaEvolve: A coding agent for scientific and algorithmic discovery\.*arXiv preprint arXiv:2506\.13131*, 2025\.URL[https://arxiv\.org/abs/2506\.13131](https://arxiv.org/abs/2506.13131)\.
- OpenAI \(2026\)OpenAI\.On the Navier–Stokes millennium prize problem, September 2026\.URL[https://openai\.com/index/navier\-stokes\-solution/](https://openai.com/index/navier-stokes-solution/)\.Primary research announcement, September 8, 2026, with linked mathematical writeup and Lean formalization\. Smooth\-forcing formulations C and D\. Accessed September 18, 2026\.
- OpenEvolve contributors \(2026\)OpenEvolve contributors\.OpenEvolve: Open\-source evolutionary program optimization, 2026\.URL[https://github\.com/algorithmicsuperintelligence/openevolve](https://github.com/algorithmicsuperintelligence/openevolve)\.Pinned experimental revision is reported in the supplementary material; accessed September 17, 2026\.
- OpenMOSS \(2026\)OpenMOSS\.AgentHPOBench: A benchmark for evaluating llm agents as sequential hyperparameter optimizers, 2026\.URL[https://github\.com/OpenMOSS/AgentHPOBench](https://github.com/OpenMOSS/AgentHPOBench)\.Official task repository; accessed September 17, 2026\.
- Romera\-Paredes et al\. \(2024\)Bernardino Romera\-Paredes et al\.Mathematical discoveries from program search with large language models\.*Nature*, 625:468–475, 2024\.doi:10\.1038/s41586\-023\-06924\-6\.URL[https://doi\.org/10\.1038/s41586\-023\-06924\-6](https://doi.org/10.1038/s41586-023-06924-6)\.
- Schrittwieser et al\. \(2020\)Julian Schrittwieser, Ioannis Antonoglou, Thomas Hubert, et al\.Mastering Atari, Go, chess and shogi by planning with a learned model\.*Nature*, 588:604–609, 2020\.doi:10\.1038/s41586\-020\-03051\-4\.URL[https://arxiv\.org/abs/1911\.08265](https://arxiv.org/abs/1911.08265)\.
- Silver et al\. \(2018\)David Silver, Thomas Hubert, Julian Schrittwieser, et al\.A general reinforcement learning algorithm that masters chess, shogi, and Go through self\-play\.*Science*, 362\(6419\):1140–1144, 2018\.doi:10\.1126/science\.aar6404\.URL[https://doi\.org/10\.1126/science\.aar6404](https://doi.org/10.1126/science.aar6404)\.
- Sinclair \(2026\)Thomas Sinclair\.The radial derivative on the graded Möbius algebra\.*arXiv preprint arXiv:2608\.18519*, 2026\.URL[https://arxiv\.org/abs/2608\.18519](https://arxiv.org/abs/2608.18519)\.
- Trinh et al\. \(2024\)Trieu H\. Trinh, Yuhuai Wu, Quoc V\. Le, He He, and Thang Luong\.Solving olympiad geometry without human demonstrations\.*Nature*, 625:476–482, 2024\.doi:10\.1038/s41586\-023\-06747\-5\.URL[https://www\.nature\.com/articles/s41586\-023\-06747\-5](https://www.nature.com/articles/s41586-023-06747-5)\.
- Yamada et al\. \(2025\)Yutaro Yamada et al\.The AI Scientist\-v2: Workshop\-level automated scientific discovery via agentic tree search\.*arXiv preprint arXiv:2504\.08066*, 2025\.URL[https://arxiv\.org/abs/2504\.08066](https://arxiv.org/abs/2504.08066)\.

## Appendix AEvidence Inventory and Reporting Conventions

This supplement distinguishes among original runs, the official replay, mechanism diagnostics, and documented discovery artifacts\. Across the registered development matrix, EPOCH achieves the highest mean score \(0\.65\), compared with 0\.53 for the strongest baseline\. In the official replay, its mean effect is positive against all four baselines, with a maximum task\-level gain of approximately 0\.48\. On AgentHPO, the full system attains a normalized mean score of 77\.48—13\.17 points above the strongest component\-removal variant—and proof admission is favorable on all six reported tasks\. The discovery portfolio further contributes exact tensor constructions, circuit reductions, finite counterexamples, and formal kernels\. The remainder of this supplement explains how these advantages arise and how each mathematical conclusion is established\.

##### How to read the figures\.

Benchmark plots reproduce the supplied aggregate records\. Circuit and proof diagrams explain dependencies; they are not additional measured results\. Curves in Figures[S9](https://arxiv.org/html/2610.06986#A10.F9)–[S11](https://arxiv.org/html/2610.06986#A10.F11)are evaluations of the explicitly stated formulas, with hypotheses and proof status preserved\. They should not be counted as independent confirmation of those formulas\. Exact numerical results remain in the adjacent tables\.

### A\.1Pre\-registered Evaluation Protocol and Reproducibility Controls

All compared systems, adapters, task definitions, and official data were frozen before evaluation\. The registered main schedule used the model labelDeepSeek\-V4\-Flashand seeds2026081901,2026081902, and2026081903\.

AlgoTune public search uses the first eight official train rows, a single editable task\-local program, the original correctness verifier, and a 48\-semantic\-call ceiling\. Timing runs in a fresh process with one warmup and three measured repetitions per public instance\. Official replay uses the first 32 test rows for scheduled original endpoints\.

### A\.2Evaluation Metrics and Comparison Conventions

For a complete taskttand methodmm, letqt​m​sq\_\{tms\}be its frozen normalized evaluator score\. The development task mean isq¯t​m=\|S\|−1​∑s∈Sqt​m​s\\bar\{q\}\_\{tm\}=\|S\|^\{\-1\}\\sum\_\{s\\in S\}q\_\{tms\}, and the cross\-task effect against baselinebbis\|T\|−1​∑t\(q¯t,EPOCH−q¯t​b\)\|T\|^\{\-1\}\\sum\_\{t\}\(\\bar\{q\}\_\{t,\\textsc\{EPOCH\}\}\-\\bar\{q\}\_\{tb\}\)\. The balanced development matrix has\|S\|=3\|S\|=3,\|T\|=12\|T\|=12\. Official replay uses the analogous effect on the reported official\-replay cohort\. Development recovery and original replay do not share an identical endpoint population\.

For heterogeneous AgentHPO metrics, letdt=1d\_\{t\}=1for higher\-is\-better metrics anddt=−1d\_\{t\}=\-1for lower\-is\-better metrics\. Task\-level means are

y¯t​v=1\|St​v\|​∑s∈St​vyt​v​s\.\\bar\{y\}\_\{tv\}=\\frac\{1\}\{\|S\_\{tv\}\|\}\\sum\_\{s\\in S\_\{tv\}\}y\_\{tvs\}\.\(S1\)A paired effect uses the shared evaluation schedulePt​b=St,EPOCH∩St​bP\_\{tb\}=S\_\{t,\\textsc\{EPOCH\}\}\\cap S\_\{tb\}:

δt​b=1\|Pt​b\|​∑s∈Pt​bdt​\(yt,EPOCH,s−yt​b​s\)\.\\delta\_\{tb\}=\\frac\{1\}\{\|P\_\{tb\}\|\}\\sum\_\{s\\in P\_\{tb\}\}d\_\{t\}\(y\_\{t,\\textsc\{EPOCH\},s\}\-y\_\{tbs\}\)\.\(S2\)The supplied paired report gives W/T/L and sign\-test results separately from task\-level means\.

## Appendix BDataset Construction, Task Selection, and Data Splits

This section distinguishes four objects that are easy to conflate: a benchmark’s native data, the task subset registered for this study, the public observations available during search, and the terminal observations reserved for endpoint evaluation\. The supplied artifacts do not describe a newly crowdsourced dataset\. Rather, they freeze task subsets and views from existing benchmark repositories\. Table[S1](https://arxiv.org/html/2610.06986#A2.T1)gives the resulting analysis units\.

Table S1:Construction and split summary\. “Cell” denotes one task–method–seed execution\. Certificate cases are not treated as sampled benchmark rows\.### B\.1Task Cohort and Evaluation Data Separation

The experimental cohort comprises the twelve\-task schedule reported in Table[S1](https://arxiv.org/html/2610.06986#A2.T1): affine transform, communicability, Convolve2D, zeta\-zero count, cyclic independent set, real eigenvalues, FFT convolution, maximum common subgraph, NMF, Robertson ODE, real polynomial, and SVM\. The supplied record identifies this set as a frozen benchmark subset\.

For each task, search is restricted to the first eight rows of the official training data\. These rows may influence code proposals, public correctness feedback, and endpoint selection\. The first 32 rows of the official test data are reserved exclusively for scheduled replay of the already selected original endpoint; their outcomes are not fed back into that endpoint’s search history\. If a test failure prompts a new proposal, the resulting artifact constitutes a separate experiment and must not be reported as part of the original held\-out replay\. Row order and membership follow the frozen official\-data revision documented in Table S1; no reshuffling, stratification, or cross\-validation is reported\.

### B\.2Math14 Suite Construction and Staged Evaluation

Math14 is a project\-frozen suite of fourteen mathematical objectives\. Its registered design forms a balanced factorial matrix of14×5×3=21014\\times 5\\times 3=210cells, corresponding to fourteen objectives, five compared systems, and three registered seeds per objective–system pair\. The suite was assembled and evaluated in stages: the objective list, system variants, seed schedule, and evaluation rules were fixed first; executable cells were then completed under the registered protocol; and the resulting records were frozen before aggregate analysis\.

### B\.3AgentHPO Tasks and Native Evaluation Splits

The reported AgentHPO ablation analysis covers the full EPOCH system and four component\-removal variants targeting memory, the falsifier, proof admission, and the phase controller\. The six reported environments span heterogeneous domains: game\-playing reinforcement learning \(ART 2048\), natural\-language inference \(ModernBERT MNLI\), noisy graph learning \(NoisyGL Cora\), semi\-supervised facial\-age regression \(RankUp UTKFace\), long\-horizon time\-series forecasting \(SparseTSF ETTm1\), and tabular regression \(TabM California\)\. Their target metrics are, respectively, win rate, classification accuracy, node\-classification accuracy, mean absolute error \(MAE\), mean squared error \(MSE\), and root mean squared error \(RMSE\)\. Each environment’s native optimization direction is preserved\.

### B\.4How discovery\-case evidence is constructed

The mathematical and algorithmic cases do not use a statistical train/test split\. Each begins with a frozen problem statement, comparator, editable object, and claim boundary\. Search may inspect public algebraic identities, source constructions, or finite instances; admission then binds the selected object to exact verification obligations\. Evidence is constructed in four noninterchangeable layers:

1. 1\.Semantic reconstruction:rebuild the target independently from its definition \(for example, tensor coordinates, AES truth tables, or selection ranks\)\.
2. 2\.Exact or exhaustive replay:check every coordinate or every member of the declared finite universe when the claim is finite\.
3. 3\.Mutation controls:corrupt a factor, coefficient, gate, recurrence term, or certificate field and require the verifier to reject it\.
4. 4\.Formal or analytic bridge:prove the reusable implication connecting the checked finite object to the stated theorem, while listing any remaining source\-specific or representation\-specific bridge\.

Figure S1:Evidence construction from claim definition to the final theorem bridge\. Exact replay establishes the declared finite object; mutation controls test sensitivity to selected errors; only the final bridge transfers those facts to the stated mathematical claim\. The diagram is logical, not a count of experiments\.Discovery examples may guide the search, but the admitted statement is determined by the replay domain, not by how many exploratory examples happened to succeed\. A finite exhaustive certificate and a sampled numerical check therefore receive different labels throughout Sections[I](https://arxiv.org/html/2610.06986#A9)–[K](https://arxiv.org/html/2610.06986#A11)\.

##### Finite\-certificate sufficiency\.

LetUUbe the finite universe named by a claim, letCCbe the admitted candidate, and letP⁡\(C,u\)P\(C,u\)be the semantic property to be established for everyu∈Uu\\in U\. Suppose an independent constructor enumeratesUUwithout omission or duplication, and a sound exact checker returns true exactly whenP⁡\(C,u\)P\(C,u\)holds\. Then

\(\|U^\|=\|U\|∧U^=U∧⋀u∈U^P⁡\(C,u\)\)⟹∀u∈U,P⁡\(C,u\)\.\\left\(\|\\widehat\{U\}\|=\|U\|\\ \\wedge\\ \\widehat\{U\}=U\\ \\wedge\\ \\bigwedge\_\{u\\in\\widehat\{U\}\}P\(C,u\)\\right\)\\Longrightarrow\\forall u\\in U,\\ P\(C,u\)\.\(S3\)
###### Proof\.

Take arbitraryu∈Uu\\in U\. Completeness of the independent enumeration givesu∈U^u\\in\\widehat\{U\}, and the accepted checker result for that element givesP⁡\(C,u\)P\(C,u\)\. Sinceuuwas arbitrary, the universal finite claim follows\. Soundness of the checker and equalityU^=U\\widehat\{U\}=Uare premises, not consequences of a large pass count; mutation controls can expose violations of soundness but cannot prove those premises by themselves\. ∎

### B\.5Exclusions, deduplication, and contamination controls

A task–method–seed key is counted once in a benchmark matrix\. Retries caused by transport failure retain the same key and provenance; endpoint replays do not become new observations\. Correct but non\-improving proposals retain the endpoint selected by the frozen rule\. Incorrect proposals are recorded as rejected trials, and an available verified fallback remains the method outcome when the contract provides one\. In case studies, coordinate symmetries and isomorphism reductions may compress a search, but reported coverage is expanded back to the full declared universe before admission\.

## Appendix CExperimental Configuration and Execution Details

Table[S2](https://arxiv.org/html/2610.06986#A3.T2)consolidates the settings that are otherwise distributed across the supplied audit documents\.

Table S2:Frozen execution configuration recoverable from the supplied artifacts\.### C\.1Common execution lifecycle

Every registered cell begins from the method\-specific frozen revision and the same task contract\. The runner records the initial artifact and verifier result before model interaction\. At interventiontt, the method receives only the public task view and the information permitted by its variant\. A proposal must parse into the expected schema and stay within the editable surface\. Candidate execution then records correctness, objective value, resource use, and any task\-specific challenge\. EPOCH additionally records evidence references, falsifier outcome, phase, and admission status\. The event is appended even when rejected\.

Endpoint replacement is separate from proposal evaluation\. A higher public score cannot replace a verified incumbent if correctness or another required gate fails\. At the budget boundary, the runner serializes the selected endpoint and its evidence root\. Scheduled replay reconstructs precisely this serialization in a clean process\. The replay result is linked to, but does not rewrite, the search record\. This lifecycle also explains the ablations: each removal changes a declared part of the proposal or admission interface, rather than merely hiding a column during analysis\.

### C\.2Evaluation Details for AlgoTune and Math14

For each public AlgoTune instance, correctness is evaluated before timing\. Timing is measured in a fresh process after one warmup run and aggregated across three measured repetitions according to the benchmark’s frozen evaluator\. Task\-level means are computed by first averaging the three registered seeds, after which all tasks receive equal weight\.

Math14 reports the project\-normalized endpoint score returned by each objective\-specific evaluator\. Verification status is recorded separately from method failure: a failed method may still retain a task\-defined fallback score\.

### C\.3AgentHPO evaluation details

AgentHPO preserves raw task units: win rate and accuracy are maximized, whereas MAE, MSE, and RMSE are minimized\. The registered paired report orients each full\-versus\-removal difference so that positive favors full EPOCH, collapses to a task direction under its frozen tie rule, and applies an exact two\-sided sign test across non\-tied tasks\.

Behavior diagnostics are computed from trace events rather than endpoint scores\. Evidence\-reference rate asks whether a decision cites a nonbaseline prior event; duplicate\-configuration rate asks whether the emitted configuration exactly matches the baseline or an earlier configuration in the same cell; rejection rate recordsadmitted=false\. The alternative macro report aggregates within each task and then averages six tasks equally\.

## Appendix DDetailed Architecture and Evidence Protocol

This section translates the main\-text contract into protocol\-level operations\. The mathematical notation defines the quantities to preserve and verify, while the implementation details specify the concrete settings through which the architecture enforces its invariants\.

### D\.1The research task as an executable contract

A task is more than an objective function\. It specifies an initial artifact, editable scope, allowed observations, correctness conditions, resource limits, and an endpoint rule\. For a code task, the artifact may be a Python implementation of a function with a fixed input/output interface\. For a tensor task, it may be a list of rank\-one paths and a target\-coordinate generator\. For a mathematical statement, it includes the hypotheses and the meaning of any finite or formal evidence used to justify the conclusion\. Without this surrounding contract, a high score is compatible with changing the problem rather than solving it\.

The public view and terminal view have different roles\. Public instances can influence proposal generation\. A terminal view can evaluate the selected endpoint only under the declared protocol\. If official test feedback is used to generate a new candidate, that candidate belongs to a new search experiment; it is not the original endpoint’s replay\. Similarly, a certificate verifier may expose a precise failed coordinate during search, whereas a held\-out benchmark evaluation must not silently become an additional optimization loop\.

A resource envelope has both accounting and attribution semantics\. Candidate execution consumes task resources; proposal generation consumes semantic calls and associated model resources\. A candidate that exceeds a valid registered time limit has failed within the method contract\. An evaluator that cannot launch because a required device is unavailable creates a different state\. The experiment must identify which boundary failed before deciding whether the cell has a score, or a fallback\. This distinction is particularly consequential when comparing methods with different orchestration patterns\.

### D\.2Evidence records and information exposed to generation

An event should be interpretable independently of the model’s narrative\. It identifies the exact executable or symbolic candidate, evaluator version, and input version; metric and correctness fields record different outcomes; and attribution explains why the result can or cannot be used\. An evidence reference points to this immutable event, not to a mutable natural\-language statement such as “the previous attempt worked\.” A subsequent claim can therefore be traced back to a specific observation without printing storage\-level identifiers in the paper\.

The bounded memory view is a projection of a longer evidence history\. A projection can contain successful trials, rejected proposals, baseline observations, and relevant counterexamples without reproducing an entire transcript\. This distinction matters because a context\-window summary may omit details while the underlying record still retains them\. The architecture’s auditability claim concerns preservation of the full record and stable identifiers, not an assertion that the model always receives every historical event\.

A useful proposal has at least four interpretable parts\. Its hypothesis describes the mechanism intended to improve the objective\. Its expected effect states the direction or observable change\. Its evidence references identify earlier observations supporting the intervention\. Its falsifier specifies a condition under which the mechanism should be rejected\. For example, a faster convolution implementation may predict identical zero\-padded linear convolution on rectangular shapes; a wraparound mismatch is a falsifier even when timing improves\. An algebraic lift may predict a specified coefficient identity; a single mismatching semantic coordinate refutes that proposal\.

Evidence can be useful without being positive\. A tensor\-chart obstruction excludes an entire local representation\. A failure at a boundary input shows which invariant an optimization omitted\. A repaired parser incident explains why a method appeared to produce no candidates\. These observations should be stored with different types because they imply different next actions\. Treating them all as low rewards loses both scientific information and the ability to diagnose the evaluation itself\.

### D\.3Admission as a three\-valued decision

Figure S2:EPOCH’s three\-valued admission gate\. Passing proposals add verified gains; failed proposals retain the correct incumbent and contribute a falsifier; unresolved checks preserve the claim as pending\. This separation lets EPOCH learn from adverse evidence while protecting an already verified endpoint\.Figure[S2](https://arxiv.org/html/2610.06986#A4.F2)makes the three outcomes explicit\. Retention depends on the conjunction of the applicable gates, not a numerical average of their statuses\.

For each applicable gategg, writeg⁡\(c\)∈\{𝗉𝖺𝗌𝗌,𝖿𝖺𝗂𝗅,𝗎𝗇𝗋𝖾𝗌𝗈𝗅𝗏𝖾𝖽\}g\(c\)\\in\\\{\\mathsf\{pass\},\\mathsf\{fail\},\\mathsf\{unresolved\}\\\}\. Conjunction passes only if every required gate passes\. Any demonstrated contract violation fails admission\. An infrastructure incident that prevents a required check leaves admission unresolved; it does not establish either candidate correctness or candidate incorrectness\. This gives an operational form to the main\-text admission predicate\.

The gates are logically heterogeneous\. Parsing checks that the proposed artifact can be interpreted\. Scope checks that changes remain within the task\. Budget checks enforce the candidate’s resource contract\. Correctness checks the task semantics\. Challenges test declared weak points or adverse cases\. Replay checks reproducibility of the selected object\.

A benchmark search endpoint and a theorem statement may require different final gates\. A code endpoint can be admitted as correct on the registered validation instances without being admitted as universally correct on all inputs\. A polynomial identity checked symbolically can support all values covered by its algebraic hypotheses\. A finite certificate for 1,600 coordinates can support the whole finite tensor identity because those coordinates span the target object\. The same number of sampled random matrices would have a different evidential meaning\.

The word “proof” in proof admission therefore refers to the required justification, not to one proof technology\. A Lean receipt can be a very strong terminal object, but only if the formal statement has been connected to the concrete candidate and task\. Conversely, an exhaustive executable verifier can completely establish a finite property without a Lean translation\.

### D\.4Protocol\-level discovery loop

The following pseudocode exposes the sequence of decisions without adding an unreported search heuristic\.

> Input:frozen contract, initial verified fallback when supplied, resource ledger, and empty append\-only trial history\. Initialize:record the baseline, its verification receipt, and its resource use\. Whilean intervention remains allowed: Choose the current phase using the registered controller\. Construct the bounded evidence view and request a proposal\. Validate its schema, editable scope, and required evidence fields\. Evaluate correctness, objective, and the applicable challenge\. Attribute failures before deciding score eligibility\. Append the candidate, observations, and gate reasons to history\. Replace the endpoint only if admission and the comparison rule permit\. Finalize:reconstruct and replay the exact selected artifact\. Seal:bind the final claim, scope, contract, history, and replay receipts\.

The pseudocode deliberately separates evaluator observations from endpoint replacement\. A candidate can be informative and still be ineligible for replacement\.

### D\.5Endpoint safety and provenance invariants

Suppose the baseline is verified under contract𝒞\\mathcal\{C\}and every endpoint replacement requires all applicable gates to pass\. By induction on the number of interventions, the retained endpoint always has a passing receipt under that contract\. At the base step this is the registered baseline\. At a later step, a failed or unresolved candidate does not replace it, while an admitted replacement has its own passing receipt\. This invariant explains why a misleading public score need not corrupt the endpoint\.

The invariant is intentionally relative\. If the correctness checker misses a class of inputs, a passing endpoint may still fail outside its registered coverage\. If the checker itself is wrong, the invariant establishes protocol compliance rather than external truth\. This is why the artifact must preserve the evaluator identity and why independent semantic reconstruction provides information beyond repeated execution of the same checker\.

Append\-only history gives a second invariant\. A new event extends the history fromMtM\_\{t\}to\(Mt,et\+1\)\(M\_\{t\},e\_\{t\+1\}\); it does not change the candidate or attribution of earlier events\.

Claim sealing adds a binding invariant rather than a theorem of correctness\. If the candidate, evaluator, inputs, or claim text changes, the archival record must create a distinct version\. This versioning rule does not validate a theorem; it only ensures that a receipt cannot silently migrate to a different claim or artifact\.

### D\.6Falsification, duplicates, and phase changes

A repeated configuration can indicate useful replication, accidental repetition, or a failure to incorporate evidence\. The AgentHPO trace metric counts equality with an earlier emitted configuration; it does not by itself distinguish those motivations\. Consequently, a lower repetition rate is an operational signal, not a standalone measure of scientific efficiency\. In the deterministic traps, the intended repeated behavior is specified by construction; in external tasks, endpoint outcomes remain necessary to interpret it\.

A falsifier differs from an ordinary correctness test by being directed at the proposal’s mechanism\. A factor\-sharing proposal must preserve ANF coverage and return ancillas; a certificate compression proposal must preserve all represented cases; a conjectured inequality must survive degenerate and equality regimes\. The same challenge can discover a scientific failure and produce a useful input for the next proposal\.

Phase changes organize how these observations affect search\. Exploration seeks materially different hypotheses\. Refinement invests in supported mechanisms\. Finalization stops search and concentrates on replay and claim scope\.

### D\.7Independent replay and trusted boundaries

Replay independence has several levels\. Process independence reconstructs the same candidate in a clean process\. Implementation independence reconstructs the mathematical or executable target using another program\. Representation independence uses a different computational model, such as multiplication\-matrix norms versus resultants, or one irreducible finite\-field model versus another\. Formal reflection moves selected finite checks into a proof assistant\. These levels can be complementary rather than interchangeable\.

A strong replay package makes the interfaces explicit: exact input object, output statement, invariant checked, failure code, and resource boundary\. For example, a QASM truth\-table replay checks an emitted circuit; it does not verify the optimizer’s claim of global minimality\. A Lean determinant kernel proves an implication from a characteristic\-polynomial hypothesis; it does not supply the representation\-theoretic hypothesis\. An exhaustive graph\-catalogue pass verifies every listed record; it does not prove the catalogue contains every possible graph\.

This layered view is also how the supplementary catalogue should be read\. Each entry identifies the mathematical object and the strongest retained statement, then distinguishes construction, exhaustive finite checks, analytic arguments, and formal kernels\. Results that are locally complete but globally unresolved remain useful evidence when their boundary is preserved\.

## Appendix EEngineering Endpoints Behind the AlgoTune Gains

These cases connect benchmark gains to executable mechanisms\. They are not counted among the four new algorithmic discovery candidates, because the core numerical and graph algorithms are established techniques\. Their role is to show that high public scores correspond to recognizable task\-solving strategies and to document the controls used to check them\.

### E\.1Convolve2D: generic zero\-padded real FFT

The retained Convolve2D endpoint replaces the relevant direct computation with a generic zero\-padded real FFT convolution\. Zero padding must prevent circular aliasing, and the output slice must match the task’s shape convention\. A faster transform that returns a wrapped or shifted result would fail the semantic contract even if its timing is favorable\.

The supplied audit records six shape controls and relative error below9×10−169\\times 10^\{\-16\}\. The public score moves from 0\.5 to 1\.0\. These checks support the registered endpoint on the tested shape family and numerical tolerance; they do not make FFT convolution a new algorithm\. AdaEvolve also later produced a clean generic solution, and the complete development table has a Convolve2D tie with AdaEvolve\. The official\-replay advantage against that baseline is correspondingly zero in the supplied task\-effect table\.

### E\.2Robertson ODE: selecting an appropriate stiff solver

The Robertson endpoint uses LSODA with task\-appropriate tolerances\. The mechanism is solver and tolerance selection for the stiff system, rather than invention of a new integration method\. Correctness depends on agreement with the task’s solution accuracy and conservation behavior, not merely on returning a trajectory more quickly\.

Six rate/time\-horizon controls report mass error below2×10−122\\times 10^\{\-12\}and maximum error below7\.2×10−87\.2\\times 10^\{\-8\}\. The public score moves from 0\.5 to 1\.0\.

### E\.3Maximum common subgraph: association graph and bitset clique search

The retained implementation represents compatible vertex matches through an association graph and solves the corresponding clique problem with bitset operations\. The correctness\-critical interface is the correspondence between cliques and valid common\-subgraph mappings: adjacency and injectivity restrictions must agree with the original task\. Established association\-graph and Bron–Kerbosch ideas supply the algorithmic basis\.

The supplied independent checks include 145 optimum comparisons through size eight\. The public score reaches 1\.0 from a 0\.5 baseline, and official replay retains a large positive task effect against every baseline\. The evidence supports a successful implementation choice under the benchmark contract\.

### E\.4NMF and zeta\-zero count: scope of task\-specific optimization

NMF has development mean 0\.70, while zeta\-zero count has mean 0\.68\. Their evaluator\-checked scores are reported at the task level and contribute to EPOCH’s strong aggregate development result\.

## Appendix FAlgoTune Development and Official Replay

### F\.1Development Coverage and Aggregate Effects

Table[S3](https://arxiv.org/html/2610.06986#A6.T3)summarizes the complete development matrix\. Each method contributes 36 evaluated cells, corresponding to twelve tasks and three registered seeds\. EPOCH achieves the highest mean normalized score, 0\.65, compared with 0\.53 for the strongest baseline\.

Table S3:Complete descriptive development coverage\.Table[S4](https://arxiv.org/html/2610.06986#A6.T4)distinguishes the supplied original reported effects from effects computed over the complete development matrix\. EPOCH has a positive mean effect against every baseline under both summaries\. The win/tie/loss profiles further indicate that the aggregate advantage varies across tasks rather than arising from a uniform improvement\.

Table S4:Distinct AlgoTune development summaries\. Original reported effects are supplied aggregates from a separate cohort, whereas complete development effects and win/tie/loss counts are computed over the complete development matrix\.
### F\.2Official\-Replay Task Effects

Figure[S3](https://arxiv.org/html/2610.06986#A6.F3)presents the reported task\-level official\-replay effects\. EPOCH achieves its largest transferable gains on maximum common subgraph and Convolve2D, together with consistent positive effects on eigenvalue computation\. These gains outweigh the reversal on NMF, yielding a positive mean replay effect against every baseline\. The resulting profile reflects substantial task\-specific improvements rather than a uniform shift across all tasks\.

![Refer to caption](https://arxiv.org/html/2610.06986v1/supp_02_replay_tasks.png)Figure S3:Reported official\-replay task effects using the original frozen endpoints\. Each value is the score ofEPOCHminus that of the corresponding baseline, rounded to three decimal places; signed zeros preserve the direction of effects that round to zero\. The largest gains occur on maximum common subgraph and Convolve2D, while NMF exhibits a consistent reversal\.

## Appendix GMath14 Evaluation and Transfer

Math14 is a project\-frozen suite of fourteen mathematical objectives evaluated across five methods and three registered seeds, yielding a balanced design of14×5×3=21014\\times 5\\times 3=210cells\. Each objective reports a project\-normalized endpoint score through its task\-specific evaluator\.

Table S5:Aggregate Math14 results\.EPOCH achieves the highest aggregate Math14 score, with a mean of 0\.57\. Its pairwise win/tie/loss records are 7/4/3 against AI\-Scientist v1, 7/5/2 against AI\-Scientist v2, 4/3/7 against OpenEvolve, and 5/3/6 against AdaEvolve\. Although the task\-level comparisons are mixed, EPOCH’s larger gains on several objectives produce the strongest overall mean\. The discovery portfolio below presents the exact constructions, counterexamples, reductions, and proofs underlying documented outcomes\.

## Appendix HAgentHPO Ablation and Mechanism Behavior

### H\.1Ablation Results

The reported AgentHPO analysis covers six tasks across the full system and its four component\-removal variants\.

Table S6:Task\-level means on the native task metrics\. Full, M, F, P, and C denote fullEPOCH, no memory, no falsifier, no proof admission, and no phase controller, respectively\. MAE, MSE, and RMSE denote mean absolute error, mean squared error, and root mean squared error\.Table S7:Paired task\-level comparisons between the full system and each component\-removal variant\. W/T/L denotes the number of task\-level wins, ties, and losses for fullEPOCH\.The full system outperforms the no\-proof\-admission variant on all six tasks and the no\-phase\-controller variant on five of six tasks\. It also records four task\-level wins against both the no\-memory and no\-falsifier variants\. These comparisons identify proof admission and phase control as the most consistently beneficial components, while the effects of memory and falsification vary more strongly across environments\.

### H\.2Observed Mechanism Behavior

A prior\-evidence citation is a decision whoseevidence\_refsincludes an identifier greater than zero, with identifier zero reserved for the baseline observation\. A repeated configuration is anew\_configidentical to the baseline or to an earlier configuration within the same task\-seed run\. Admission rejection corresponds toadmitted=false\.

Table S8:Matched mechanism\-behavior comparisons\. Differences are reported in percentage points \(pp\), and favorable tasks indicate agreement with the intended behavior of the corresponding component\.Memory increases the use of prior evidence by 37\.50 percentage points\. The falsifier, proof\-admission module, and phase controller each reduce repeated configurations, while proof admission introduces selective rejection across all six tasks\. Together, these patterns show that the components influence both the information used to generate proposals and the mechanisms governing their acceptance and progression\.

## Appendix IFour Algorithmic Discovery Cases

The following are documented research outcomes with heterogeneous budgets and verification layers\. Border rank is denotedR¯\\brank, ordinary tensor rankRR, and Waring rankRWR\_\{\\mathrm\{W\}\}\. General constructions are stated only under the field, invertibility, and nonzero\-denominator conditions required by their certificates\. External record priority remains a separate question\.

Each proof is organized as a chain rather than a single undifferentiated “verified” label\. The following subsections give the equations, constructions, exhaustive counts, corruption tests, and unresolved links\. Their common coverage and remaining bridges are summarized together with the mathematical cases in Table[S9](https://arxiv.org/html/2610.06986#A9.T9)\.

Table S9:Cross\-case evidence coverage and remaining theorem bridges\.### I\.1Reverse 2\-adic transfer and obstruction\-guided Hasse lifting

Figure S4:Reverse transfer as an evidence\-guided construction\. \(a\) At each active Hasse order, an exact linear solve either installs a jet or returns a checkable cokernel obstruction\. A changed chart may then yield a different solve\. \(b\) The supplied ss444 certificate has coefficient support weights\(0,0,64,314,291,190,96\)\(0,0,64,314,291,190,96\)\. The dashed line separates the verified target coefficient at order two from higher\-order terms\.Figure[S4](https://arxiv.org/html/2610.06986#A9.F4)links the algebraic control loop to the concrete coefficient profile\.

##### Problem and mechanism\.

A rational rank\-rrtensor decomposition can fail to reduce directly modulo two because its factors contain powers of two in their denominators\. Suppose clearing the first\-mode denominators gives integral factors satisfying

∑q=1rAq⊗Vq⊗Wq=2​T\.\\sum\_\{q=1\}^\{r\}A\_\{q\}\\otimes V\_\{q\}\\otimes W\_\{q\}=2T\.\(S4\)Reduction modulo two yields a zero\-fiber pointp=\(\(,,,,,\)\)p=\(\(a\_\{q\},b\_\{q\},c\_\{q\}\)\)of the Segre\-sum parametrization\. Its differential is

d​Φp​\(a˙,b˙,c˙\)=∑q\(a˙q⊗bq⊗cq\+aq⊗b˙q⊗cq\+aq⊗bq⊗c˙q\)\.d\\Phi\_\{p\}\(\\dot\{a\},\\dot\{b\},\\dot\{c\}\)=\\sum\_\{q\}\(\\dot\{a\}\_\{q\}\\otimes b\_\{q\}\\otimes c\_\{q\}\+a\_\{q\}\\otimes\\dot\{b\}\_\{q\}\\otimes c\_\{q\}\+a\_\{q\}\\otimes b\_\{q\}\\otimes\\dot\{c\}\_\{q\}\)\.\(S5\)IfTmod2T\\bmod 2lies in this image, the factor paths satisfy

∑q\(aq\+ε​a˙q\)⊗\(bq\+ε​b˙q\)⊗\(cq\+ε​c˙q\)=ε​T\(modε2\)\.\\sum\_\{q\}\(a\_\{q\}\+\\varepsilon\\dot\{a\}\_\{q\}\)\\otimes\(b\_\{q\}\+\\varepsilon\\dot\{b\}\_\{q\}\)\\otimes\(c\_\{q\}\+\\varepsilon\\dot\{c\}\_\{q\}\)=\\varepsilon T\\pmod\{\\varepsilon^\{2\}\}\.\(S6\)Expanding the product proves the assertion and givesR¯𝔽¯2⁡\(T\)≤r\\brank\_\{\\overline\{\\mathbb\{F\}\}\_\{2\}\}\(T\)\\leq r\. A mechanized kernel proves the first\-order expansion over a commutative ring\. The arithmetic reduction and concrete tensor binding remain explicit obligations outside the generic identity\.

##### Higher\-order search\.

Different valuation strata require Hasse jets\. The algorithm installs lower\-order coefficients, builds the remaining linear tangent map, and tests the residual for membership in its image\. Failure produces a cokernel functionalω\\omegawithω⁡\(residual\)=1\\omega\(\\mathrm\{residual\}\)=1, which constrains a change of chart or support\. All retained coefficients are replayed exactly\. This converts an unsuccessful lifting attempt into a reusable algebraic obstruction\.

> Clear denominators and assign each term its activation height\. For each coefficient order, subtract contributions already fixed by lower jets\. Solve the exact linear residual equation when feasible; otherwise retain a separating cokernel witness and revise the chart\. After completing the jets, replay every coefficient and tensor coordinate before admission\.

##### Flagship certificate\.

For the10×10×1610\\times 10\\times 16structure tensor of multiplying two symmetric4×44\\times 4matrices, 30 rank\-one polynomial paths satisfy

∑q=130Aq​\(ε\)⊗Bq​\(ε\)⊗Cq​\(ε\)=ε2​Tss444\(modε3\)\.\\sum\_\{q=1\}^\{30\}A\_\{q\}\(\\varepsilon\)\\otimes B\_\{q\}\(\\varepsilon\)\\otimes C\_\{q\}\(\\varepsilon\)=\\varepsilon^\{2\}T\_\{\\mathrm\{ss444\}\}\\pmod\{\\varepsilon^\{3\}\}\.\(S7\)The valuation strata have sizes 4/13/13\. The first\-order map has rank 68 and the second\-order system rank 328\. The known second\-order nonlinear contribution has weight 234\. Truncated coefficient weights are\(0,0,64\)\(0,0,64\); full polynomial weights are\(0,0,64,314,291,190,96\)\(0,0,64,314,291,190,96\)\. The target has 64 nonzero coordinates among 1,600 ambient coordinates\. The mechanized certificate checks all ambient coordinates and the semantic target, and rejects corrupted factor data\.

Across 86 scanned rational formulas, 43 are directly applicable and all 43 transfer, spanning 24 coordinate\-distinct targets and 45,242 independently replayed coordinates\. Eleven strict border improvements are reported internally, includingR¯⁡\(Tst444\)≤20\\brank\(T\_\{\\mathrm\{st444\}\}\)\\leq 20\. The denominator is applicable formulas, not all scanned formulas\. Bini interpolation gives the retained scalar\-count bound

R⁡\(Tss444⊗N\)≤\(4​N\+1\)​30N\.R\(T\_\{\\mathrm\{ss444\}\}^\{\\otimes N\}\)\\leq\(4N\+1\)30^\{N\}\.\(S8\)It first beats32N32^\{N\}atN=92N=92in that model; the retained extension\-field descent model gives a crossover atN=170N=170\. Neither number is a runtime benchmark\.

#### I\.1\.1Coefficient\-level derivation and obstruction certificates

For clarity, write a trilinear factor path asa⁡\(ε\)=a0\+ε​a1\+ε2​a2\+⋯a\(\\varepsilon\)=a\_\{0\}\+\\varepsilon a\_\{1\}\+\\varepsilon^\{2\}a\_\{2\}\+\\cdots, and similarly forb,cb,c\. The coefficient of orderkkin a rank\-one path is

\[εk\]​\(a⊗b⊗c\)=∑i\+j\+ℓ=kai⊗bj⊗cℓ\.\[\\varepsilon^\{k\}\]\(a\\otimes b\\otimes c\)=\\sum\_\{i\+j\+\\ell=k\}a\_\{i\}\\otimes b\_\{j\}\\otimes c\_\{\\ell\}\.\(S9\)At order one, exactly three terms occur, giving the Segre differential\. At order two, the terms involving a new second jet are linear in that jet, while products of first jets are already known\. This is why each lifting stage separates into a known nonlinear contribution and an exact linear residual problem\. The decomposition is structural, not an approximation to the coefficient equations\.

Suppose a stage asks forL​x=rLx=rover a finite field\. If no solution exists, row reduction can produce a functionalω\\omegasatisfyingω​L=0\\omega L=0butω​r≠0\\omega r\\neq 0; rescale toω​r=1\\omega r=1when applicable\. Anyone can verify this witness by multiplication\. It proves that the current residual is outside the active tangent image\. It does not prove that the tensor has no decomposition of the desired rank, since a new base point, chart, support, or higher\-order ansatz changesLLand possiblyrr\.

This distinction is central to the search loop\. A witness excludes a precise local proposal family and can constrain the next representation\. It cannot be admitted as a global tensor\-rank lower bound\. Repeatedly increasing a solver timeout would not resolve an exact cokernel obstruction within the same chart; changing the chart is a mathematically different intervention\.

#### I\.1\.2From a truncated identity to a border upper bound

Let the full polynomial rank\-one sum beF⁡\(ε\)F\(\\varepsilon\)and suppose coefficient verification establishes

F⁡\(ε\)=εh​T\+εh\+1​E1\+⋯\+εh\+e​Ee\.F\(\\varepsilon\)=\\varepsilon^\{h\}T\+\\varepsilon^\{h\+1\}E\_\{1\}\+\\cdots\+\\varepsilon^\{h\+e\}E\_\{e\}\.\(S10\)For nonzeroε\\varepsilon, the rescaled tensorε−h​F​\(ε\)\\varepsilon^\{\-h\}F\(\\varepsilon\)has rank at most the number of paths, because the scalar can be absorbed into one factor of each term\. Asε\\varepsilontends formally or algebraically to zero, its limit isTT\. This supplies the border upper bound over the stated closure\. It says nothing about whetherTTitself has a rank decomposition of that same length without a limiting parameter\.

For a tensor powerNN, the error degree is at moste​NeN\. Interpolating ate​N\+1eN\+1suitable field points recovers the constant coefficient of the powered rescaled expression, giving the retained\(e​N\+1\)​rN\(eN\+1\)r^\{N\}exactification pattern\. Availability of interpolation points and extension\-field descent costs must be accounted for separately\. The ss444 result usese=4e=4, yielding\(4​N\+1\)​30N\(4N\+1\)30^\{N\}; the later tail\-elimination cases improveeewithout necessarily changingrr\.

#### I\.1\.3Semantic reconstruction and negative controls

A certificate must be checked against the intended matrix operation, not only against a tensor imported from the same optimizer\. The independent route reconstructs the operation tensor from input/output matrix entries, decodes the official rational factors, and checks every coefficient against those semantics\. This separates factor parsing, target construction, and polynomial expansion as possible error sources\.

The ss444 coefficient weights are useful compact diagnostics, but weights alone cannot prove identity: two different tensors can have the same number of nonzero coordinates\. Admission therefore uses the full 1,600\-coordinate comparison, with the weights serving only as a support\-count summary\. The one\-bit corruption test demonstrates sensitivity to a chosen factor error\. It complements, rather than replaces, the complete coordinate proof\.

### I\.2Hyperfactor and cross\-output AES sharing

![Refer to caption](https://arxiv.org/html/2610.06986v1/x1.png)Figure S5:Factor\-sharing mechanism and an illustrative cost model\. The pseudocode keepsxxunchanged, computes a factor into a zero ancilla, reuses it, and uncomputes it\. If compute/uncompute costsccand each use costsu\>0u\>0, separate uses costk⁡\(c\+u\)k\(c\+u\)and shared uses costc\+k​uc\+ku\. The plotted relative saving is\(k−1\)​c/\[k⁡\(c\+u\)\]\(k\-1\)c/\[k\(c\+u\)\], for integerkk\. This simplified surface is not fitted to AES measurements and ignores allocation, routing, and factor\-dependent use costs; it is not the emitted circuit\.Figure[S5](https://arxiv.org/html/2610.06986#A9.F5)explains why cross\-output factor selection can change compute/uncompute cost\. Its model isolates reuse count and the opening\-to\-use cost ratio; the recorded AES reduction from 10,746 to 9,234 T gates is a separate matched measurement, not a point calibrated on that surface\. The identity, schedule, and complete circuit each require their own checks\.

##### Optimization problem\.

LetGGbe residual groups andFFthe frozen factor library\. Opening factorffcostscfc\_\{f\}; assigning residualggto it costsrg​fr\_\{gf\}\. Solve

min⁡∑fx,y⁡cf​yf\+∑g,frg​f​xg​f,∑fxg​f=1,xg​f≤yf,xg​f,yf∈\{0,1\}\.\\min\_\{x,y\}\\sum\_\{f\}c\_\{f\}y\_\{f\}\+\\sum\_\{g,f\}r\_\{gf\}x\_\{gf\},\\qquad\\sum\_\{f\}x\_\{gf\}=1,\\quad x\_\{gf\}\\leq y\_\{f\},\\quad x\_\{gf\},y\_\{f\}\\in\\\{0,1\\\}\.\(S11\)A selected factor is computed into an ancilla, reused for assigned outputs, and uncomputed\. The Boolean kernel is\(a∧h\)⊕\(b∧h\)=\(a⊕b\)∧h\(a\\wedge h\)\\oplus\(b\\wedge h\)=\(a\\oplus b\)\\wedge h, mechanized together with its output\-family lifting\. Circuit equivalence requires additional execution checks\.

Table S10:AES T\-counts under the frozen representation and cost model\. The last two rows share the same PyZX post\-processing pass\.The construction covers 1,013 ANF occurrences, shares 37 repeated nonzero\-cost factors, and uses 1,528 CCX gates and 23 qubits in the reported pre\-PyZX circuit\. HiGHS and an independent SCIP implementation agree on the fixed\-charge objective\. An independent verifier reconstructs AES inversion and affine\-output ANFs, checks exact monomial coverage, and simulates all 256 inputs through QASM while checking ancilla restoration\. Removing a CCX is a negative control\. Matched post\-processing saves 1,512 T gates; the comparison against the frozen pair baseline saves 15,190 T gates\.

The independent optimization replay, ANF reconstruction, and circuit receipt agree on the registered construction\. Optimality applies only to the registered factor library and cost model\. Global AES circuit optimality, routing, depth, and noisy hardware performance are not established\.

#### I\.2\.1Why arbitrary\-arity sharing differs from pair matching

A pairwise optimizer considers sharing between two residual expressions at a time\. A factor that benefits three or more groups can be unprofitable in every locally selected pair and still profitable when its opening cost is paid only once for the whole group\. The binary variableyfy\_\{f\}represents this global activation decision, while thexg​fx\_\{gf\}variables assign residual use\. Their coupling captures a cost that cannot be represented by independent residual choices alone\.

For a factor used ink≥2k\\geq 2outputs, letc\>0c\>0be its registered compute–uncompute cost andu\>0u\>0the per\-output use cost\. Separate realization costsk⁡\(c\+u\)k\(c\+u\), whereas a legal shared schedule costsc\+k​uc\+ku\. Hence

k⁡\(c\+u\)−\(c\+k​u\)=\(k−1\)​c\>0,k⁡\(c\+u\)−\(c\+k​u\)k⁡\(c\+u\)=\(k−1\)​ck⁡\(c\+u\)\.k\(c\+u\)\-\(c\+ku\)=\(k\-1\)c\>0,\\qquad\\frac\{k\(c\+u\)\-\(c\+ku\)\}\{k\(c\+u\)\}=\\frac\{\(k\-1\)c\}\{k\(c\+u\)\}\.\(S12\)This establishes the saving claimed by the schematic whenever the same factor remains live across all uses and the final inverse computation restores the ancilla\. It does not establish that a factor is semantically common to those outputs or that routing preserves the same cost; those are separate certificate obligations\.

The optimization model also distinguishes logical sharing from reversible execution\. A classical expression DAG may reuse a value without specifying how temporary storage is restored\. A reversible circuit must include the computation of the factor, the uses that leave it available, and the inverse computation returning the temporary register to its initial value\. The opening costcfc\_\{f\}therefore includes the registered compute/uncompute expense\. A model that omits the inverse computation would optimize the wrong cost contract\.

#### I\.2\.2Constructing a circuit from a selected assignment

For each opened factor, construct its value on a designated ancilla using the registered factor implementation\. Apply the residual\-specific controlled operations to the assigned outputs in the scheduled order\. Because the factor register is used as a control and its input data remain available under the contract, run the inverse factor computation to reset that ancilla\. The emitted schedule is then translated to QASM and checked as a complete circuit\.

This procedure requires more than an optimal integer\-program objective\. The assignment must correspond to the intended ANF occurrences; every occurrence must be accounted for under the representation’s cancellation convention; control dependencies must be legal; and uncomputation must preserve outputs\. A solver can be correct while the schedule generator is wrong\. The independent ANF and QASM layers address these different interfaces\.

The Boolean identity follows by distributivity in the two\-element Boolean ring\. For bits, XOR is addition and AND is multiplication, so\(a\+b\)​h=a​h\+b​h\(a\+b\)h=ah\+bh\. Applying the identity at each output index justifies shared algebraic factors\. The formal identity does not encode the entire ancilla schedule or a decomposition of every CCX into T gates, which is why the full\-circuit and cost checks remain separate\.

#### I\.2\.3Interpreting the cost comparisons

The first comparison, 25,886 to 10,696 T gates, measures the combined effect of moving from the frozen pair baseline to the shared construction\. The intermediate 12,362 value reveals an additional reduction of 1,666 T gates from cross\-output merging after independent\-output Hyperfactor optimization\. The matched PyZX comparison isolates a shared\-versus\-independent contrast under the same post\-processing pass: 10,746 versus 9,234, a difference of 1,512\.

These numbers should not be combined as if they were measurements of the same single intervention\. The matched post\-processing comparison provides the cleanest evidence that sharing remains advantageous after that specific optimizer\. The larger pair\-baseline difference reflects a broader change of construction\. Neither establishes minimal T count among all AES circuits, because the factor library, ancilla budget, synthesis basis, and permitted schedules delimit the search space\.

Finally, enumerating all 256 inputs is exhaustive for the registered eight\-bit input contract\. It checks the implemented truth table and ancilla restoration under that contract\. It does not directly measure routing overhead, depth under a physical architecture, or behavior under noise\. The contribution is a verifiable circuit construction and a cost comparison in a fixed model\.

### I\.3All\-parameter Big\-centroid constructor

Ford≥3d\\geq 3and ordered dimensionsu1≤⋯≤udu\_\{1\}\\leq\\cdots\\leq u\_\{d\}, setq=∏s=2dusq=\\prod\_\{s=2\}^\{d\}u\_\{s\}\. Choose full\-column\-rank matricesV\(s\)∈𝔽us×u1V^\{\(s\)\}\\in\\mathbb\{F\}^\{u\_\{s\}\\times u\_\{1\}\}with nonzero entries and left inversesL\(s\)​V\(s\)=IL^\{\(s\)\}V^\{\(s\)\}=I\. This existence condition is part of the construction contract; a finite set of field tests does not prove existence over every small field\.

ForJ=\(j2,…,jd\)J=\(j\_\{2\},\\ldots,j\_\{d\}\), define first\-mode coordinatesaJ​\(t\)=∏s=2dVjs,t\(s\)a\_\{J\}\(t\)=\\prod\_\{s=2\}^\{d\}V^\{\(s\)\}\_\{j\_\{s\},t\}\. The perturbation for modei≥2i\\geq 2uses

Lt,ji\(i\)∏s≥2,s≠iVjs,t\(s\)\.\\frac\{L^\{\(i\)\}\_\{t,j\_\{i\}\}\}\{\\prod\_\{s\\geq 2,\\,s\\neq i\}V^\{\(s\)\}\_\{j\_\{s\},t\}\}\.\(S13\)Summing overjij\_\{i\}yields∑jLt,j\(i\)​Vj,t′\(i\)=δt​t′\\sum\_\{j\}L^\{\(i\)\}\_\{t,j\}V^\{\(i\)\}\_\{j,t^\{\\prime\}\}=\\delta\_\{tt^\{\\prime\}\}\. Thus target linear coordinates appear with the required coefficients and unwanted coordinates cancel\. Subtractingu1u\_\{1\}constant correction tensors yields aq\+u1q\+u\_\{1\}\-term first\-order degeneration\. The retained flattening lower bound matchesq\+u1q\+u\_\{1\}in the stated Big\-centroid family\.

The generic mechanized first\-order kernel proves constant cancellation and the tangent coefficient identity\. The constructor separately checks matrix inverses, denominators, and coordinates\. The supplied audit records 390 parameter/field controls and 278,904 exact identities, including odd prime fields andGF⁡\(2k\)\\mathrm\{GF\}\(2^\{k\}\)for testedk≥2k\\geq 2\. The\(2,2,2,3\)\(2,2,2,3\)example over𝔽5\\mathbb\{F\}\_\{5\}has 14 terms, 30,184 ambient coordinates, and degree\-0–4 support weights\(0,44,288,240,64\)\(0,44,288,240,64\)\.

The result is a symbolic constructor with an independent exact verifier under the stated assumptions, not an improvement in the matrix\-multiplication exponent\. Related tensor\-centroid theory supplies context\([Kassabov et al\., 2026](https://arxiv.org/html/2610.06986#bib.bib14)\)\.

#### I\.3\.1The left\-inverse identity as a certificate generator

The constructor’s core operation is local cancellation\. Fix modeiiand all indices exceptjij\_\{i\}\. Multiplying the perturbation coefficient by the base\-coordinate factors cancels every denominator from the modes held fixed\. The remaining sum overjij\_\{i\}is exactly an entry ofL\(i\)​V\(i\)L^\{\(i\)\}V^\{\(i\)\}\. It equals one when the two first\-mode labels coincide and zero otherwise\. Thus the same small\-matrix identity both selects desired coordinates and annihilates undesired ones\.

This is more informative than solving the full ambient tangent system independently for each dimension tuple\. The latter can certify one instance but hides why the instance works\. The left\-inverse construction exposes a dimension\-parametric algebraic mechanism and emits witnesses whose validation reduces to matrix products, nonzero\-denominator checks, and coordinate expansion\. Its usefulness is not tied to one unusually favorable numerical seed\.

Theqqbase paths contribute a constant term\. The retained construction expresses that constant asu1u\_\{1\}correction tensors, so adding their negatives produces zero constant coefficient\. The prescribed first\-order perturbations then yield the target\. This is the reason for theq\+u1q\+u\_\{1\}term count; it is not inferred from a numerical fit\. The matching flattening argument is needed to call the bound minimal within the stated family\.

Concretely, letFlat⁡\(T\)\\mathrm\{Flat\}\(T\)be the registered linear flattening of the Big\-centroid tensor\. A rank\-one tensor maps to a matrix of rank at most one, so subadditivity givesrank⁡Flat⁡\(T′\)≤r\\operatorname\{rank\}\\mathrm\{Flat\}\(T^\{\\prime\}\)\\leq rfor every tensorT′T^\{\\prime\}of rank at mostrr\. Matrix rank is upper semicontinuous under specialization; hence the same inequality holds for every tensor of border rank at mostrr\. Once the displayed block structure is shown to have

rank⁡Flat⁡\(T\)=q\+u1,\\operatorname\{rank\}\\mathrm\{Flat\}\(T\)=q\+u\_\{1\},\(S14\)it follows thatR¯⁡\(T\)≥q\+u1\\brank\(T\)\\geq q\+u\_\{1\}\. The first\-order construction gives the reverse inequality, and therefore equality\. The remaining obligation is to prove that block\-rank identity uniformly under the stated field hypotheses; checking finitely many parameter tuples alone would not suffice\.

#### I\.3\.2Field assumptions and small\-field controls

A formula containing division is meaningful only when its denominators are nonzero\. The constructor therefore supplies the actual coefficient matrices and their left inverses rather than merely stating that suitable matrices should exist\. In finite fields, the matrix\-existence step needs a field\-aware construction\. A characteristic\-zero interpolation formula cannot automatically be reduced modulo a prime that collapses distinct parameters or makes denominators vanish\.

The supplied source claims a uniform field construction over odd prime fields and binary extension fields of degree at least two\. Its 390 controls and 278,904 identities provide a finite audit of the implementation\. The generic first\-order Lean kernel does not formalize this full existence theorem\. In this manuscript the explicit left\-inverse hypotheses are retained in the displayed construction so that the general algebraic implication is not confused with the separate existence and instantiation layer\.

The example’s 30,184 ambient coordinates illustrate another distinction: a sparse target can require checking many zero coordinates\. Support weights\(0,44,288,240,64\)\(0,44,288,240,64\)summarize the polynomial path by degree, but complete verification must check where those coefficients occur\. A correct target weight with an incorrect coordinate assignment would not establish the intended tensor degeneration\.

#### I\.3\.3Algorithmic and mathematical roles of the result

As an algorithmic result, Big\-centroid is a deterministic generator producing factor paths and a checkable payload from a dimension tuple and an admitted field\. As a mathematical result, its correctness is a symbolic implication from the matrix identities, constant cancellation, and flattening lower bound\. These roles are related but not identical: a general proof without an implementation does not provide an executable artifact, while finite implementation tests without the general argument do not establish all parameters\.

The symmetric Full Perazzo case developed later uses a different interpolation organization and has additional Waring\-rank and geometric conclusions\. We keep the two case identities distinct to avoid counting one formula twice as unrelated evidence\. They demonstrate a shared transition from pattern observation to explicit construction, but their targets, assumptions, and lower\-bound arguments differ\.

### I\.4Median\-of\-23 in 54 comparisons

LetVi​\(n\)V\_\{i\}\(n\)denote the minimum worst\-case comparisons needed to select theiith smallest ofnndistinct totally ordered elements\. The retained candidate isV12​\(23\)≤54V\_\{12\}\(23\)\\leq 54\. The supplied comparison point is a 55\-comparison Hadian–Sobel construction; external selection\-literature review remains separate from the certificate\([Dörrer et al\., 2025](https://arxiv.org/html/2610.06986#bib.bib6)\)\.

An early local candidate was falsified by paths requiring 56 comparisons\. The retained construction freezes those failures, classifies the over\-budget frontier by poset structure, and synthesizes budget\-specific continuations\. The exact path decomposition is

1,439,190,016=1,427,981,824\+11,208,192\.1\{,\}439\{,\}190\{,\}016=1\{,\}427\{,\}981\{,\}824\+11\{,\}208\{,\}192\.\(S15\)The first summand already fits budget 54\. The remaining occurrences form 1,454 classes:

Table S11:Repaired median frontier\. Every base depth plus continuation budget equals 54\.The dispatcher runs the frozen median\-17 base strategy, inserts six new items relative to the selected median, and invokes a seven\-item prefix policy\. If three new items lie below the selected item, it returns that item\. Otherwise it selects the relevant side, constructs the residual poset, removes elements certified outside the target rank, canonically relabels the state, and executes a budget\-decreasing residual DAG\. Sixteen policies cover the classes\.

The reported Lean layers cover transitive bitmask insertion, rank semantics of leaves, rank\-preserving removal/reduction, bijective relabeling, preservation of distinguished index zero, and well\-founded policy termination\. They also check 4,100 prefix nodes, 9,200 residual nodes, 84,894 transfers, class counts, and global path arithmetic\. Negative controls corrupt rank decrements, relabeling, residual ranks, solved leaves, class coverage, and semantic guards\.

Two headline bridges remain: instantiating every field of the common\-order criterion for each concrete V279 state, and binding the generated census to a formal decision tree on 23 items\. Therefore the result is an internal exact\-computation upper\-bound candidate, not a fully formalized theorem or a proof that 54 is optimal\.

#### I\.4\.1Decision\-tree correctness versus path\-count arithmetic

A path count is not a decision\-tree correctness proof\. Every comparison branch must represent the corresponding order relation, every terminal return must have the requested rank in every total order extending that relation, and every dispatch must preserve the target rank\. The global count becomes meaningful only after these semantic conditions are attached to the enumerated states\.

Write a residual state as\(P,r,b\)\(P,r,b\), wherePPis the current comparison poset,rrthe requested zero\-based rank, andbbthe remaining comparison budget\. Define𝒞⁡\(P,r,b\)\\mathcal\{C\}\(P,r,b\)recursively: a leaf is valid when its returned element has rankrrin every linear extension ofPP; an internal comparison of incomparablex,yx,yis valid when both child states extendPPby the corresponding relation and satisfy𝒞\\mathcal\{C\}with budget at mostb−1b\-1\. Induction onbbthen gives

𝒞⁡\(P,r,b\)⟹every total order extendingPreaches a correct leaf in at mostbcomparisons\.\\mathcal\{C\}\(P,r,b\)\\Longrightarrow\\text\{every total order extending $P$ reaches a correct leaf in at most $b$ comparisons\}\.\(S16\)The base case is the universal\-rank condition at a leaf\. For the inductive step, every total order satisfies exactly one ofx<yx<yory<xy<x, so execution enters the matching child; its budget is smaller, and the induction hypothesis supplies correctness and termination\. Thus the semantic theorem depends on child\-state validity and leaf ranks, not on the number of enumerated paths\.

A residual problem can be represented by a finite poset and a target rank\. Removing an element certified below the target decrements the target rank; removing an element certified above it leaves the rank unchanged\. Canonical relabeling is valid only when it is a bijection preserving order constraints and transporting the selected item and target correctly\. These simple rules explain why rank\-decrement and relabel corruptions are important negative controls: either mistake can preserve graph sizes and node counts while changing the selection problem\.

For a policy node with remaining budgetbb, each comparison child must have a smaller budget, and its state must extend the parent’s comparison outcome\. A solved leaf must satisfy the registered rank criterion\. Induction on the budget then verifies termination and correctness of the residual policy\. The supplied Lean stack formalizes these semantic ingredients and a large generated policy library; it does not allow the remaining concrete census\-binding obligations to be omitted\.

#### I\.4\.2Why classification compresses the difficult frontier

The 11,208,192 repaired occurrences do not require that many separately synthesized strategies\. Many residual states are equivalent after valid reduction and relabeling\. Compressing them into 1,454 classes exposes a much smaller policy\-design problem\. The dispatcher certificate must nevertheless account for every original occurrence and verify the transport into its assigned class\.

The three base\-depth groups show how the resource bound composes\. Depth 32 allows a 22\-comparison continuation; depth 33 allows 21; depth 34 allows 20\. Each composition is bounded by 54\. The 15, 422, and 1,017 class counts sum to 1,454, and their occurrences sum to the repaired frontier\. These equalities audit coverage and arithmetic; they do not establish the semantics of a single class transfer, which is checked separately\.

Sixteen reusable policies are a further level of compression\. They are not equivalent to sixteen original task instances, and their generated DAG nodes are not independent experiments\. The contribution is the combination of a census, equivalence\-preserving reduction, a small policy library, and a verified dispatch map\. Each layer removes a different obstacle to independent replay\.

## Appendix JSix Mathematical Discovery Cases

This section presents the six mathematical discoveries as explicit statements with their hypotheses, constructions, lower bounds, equality conditions, and analytic completion steps\. Exact finite certificates handle the large algebraic expansions, while the written arguments below supply the reusable theorem bridges\. The result is a proof\-oriented account of what EPOCH discovered and how each conclusion follows\.

The logical spine of each argument is stated directly in its subsection so that an identity, finite census, analytic limit, or formal theorem cannot silently substitute for another\. Table[S9](https://arxiv.org/html/2610.06986#A9.T9)gives the cross\-case comparison without repeating those derivations\.

### J\.1Hypercube determinant inequality and equality classification

Figure S6:An exact two\-parameter slice of the Hypercube inequality\. In dimension three take independent coordinate masses\(p,q,1/2\)\(p,q,1/2\), soW=1W=1\. The plot shows10310^\{3\}times the slackG=∏imi,0​mi,1−SD⁡\(w\)G=\\prod\_\{i\}m\_\{i,0\}m\_\{i,1\}\-\\operatorname\{SD\}\(w\)\. Direct expansion givesG=\[p⁡\(1−p\)​q​\(1−q\)\]2/4G=\[p\(1\-p\)q\(1\-q\)\]^\{2\}/4: positive in the interior and zero on the boundary, where support lies in a facet\. This formula\-derived slice illustrates the all\-weight, all\-dimensional theorem\.Figure[S6](https://arxiv.org/html/2610.06986#A10.F6)provides a geometric reading of the polynomial statement and its equality condition\. The support drawings illustrate the hypotheses rather than sample experimental outcomes\. For this product\-weight slice, an exact expansion over the\(84\)=70\\binom\{8\}\{4\}=70unordered vertex subsets gives the displayed slack polynomial\. Atp=q=1/2p=q=1/2, the two sides are15/102415/1024and16/102416/1024\. We checked the expansion with rational arithmetic on the 25\-point gridp,q∈\{0,1/4,1/2,3/4,1\}p,q\\in\\\{0,1/4,1/2,3/4,1\\\}; this is a consistency check of the visual, not a new execution of the reported Lean proof\. The general statement below does not assume product weights\.

Letwv≥0w\_\{v\}\\geq 0forv∈\{0,1\}dv\\in\\\{0,1\\\}^\{d\},W=∑vwvW=\\sum\_\{v\}w\_\{v\}, andmi,b=∑v:vi=bwvm\_\{i,b\}=\\sum\_\{v:v\_\{i\}=b\}w\_\{v\}\. Define the unordered determinant polynomial explicitly by

SD⁡\(w\)=∑U⊆\{0,1\}d\|U\|=d\+1\|det\(1⋯1v0⋯vd\)\|​∏v∈Uwv,\\operatorname\{SD\}\(w\)=\\sum\_\{\\begin\{subarray\}\{c\}U\\subseteq\\\{0,1\\\}^\{d\}\\\\ \|U\|=d\+1\\end\{subarray\}\}\\left\|\\det\\begin\{pmatrix\}1&\\cdots&1\\\\ v\_\{0\}&\\cdots&v\_\{d\}\\end\{pmatrix\}\\right\|\\prod\_\{v\\in U\}w\_\{v\},\(S17\)where the absolute determinant makes the ordering ofU=\{v0,…,vd\}U=\\\{v\_\{0\},\\ldots,v\_\{d\}\\\}immaterial\. The retained finite\-polynomial theorem is

SD⁡\(w\)​Wd−1≤∏i=1dmi,0​mi,1\(d≥1\)\.\\operatorname\{SD\}\(w\)W^\{d\-1\}\\leq\\prod\_\{i=1\}^\{d\}m\_\{i,0\}m\_\{i,1\}\\qquad\(d\\geq 1\)\.\(S18\)Ford≥3d\\geq 3, equality holds exactly when at least one facet mass is zero\. Ford=1d=1,W0W^\{0\}is interpreted as the polynomial constant 1, includingW=0W=0\.

##### Proof mechanism\.

IfW\>0W\>0, normalize to a cube\-valued random vectorXX\. LetΔ\\Deltabe the affine determinant ofd\+1d\+1independent draws\. Then

SD⁡\(w\)=Wd\+1\(d\+1\)\!​𝔼​\|Δ\|,𝔼​Δ2=\(d\+1\)\!​detCov⁡\(X\)\.\\operatorname\{SD\}\(w\)=\\frac\{W^\{d\+1\}\}\{\(d\+1\)\!\}\\mathbb\{E\}\|\\Delta\|,\\qquad\\mathbb\{E\}\\Delta^\{2\}=\(d\+1\)\!\\det\\Cov\(X\)\.\(S19\)Integrality gives\|Δ\|≤Δ2\|\\Delta\|\\leq\\Delta^\{2\}, while positive semidefiniteness and Hadamard’s inequality give

detCov⁡\(X\)≤∏iVar⁡\(Xi\)=W−2​d​∏imi,0​mi,1\.\\det\\Cov\(X\)\\leq\\prod\_\{i\}\\operatorname\{Var\}\(X\_\{i\}\)=W^\{\-2d\}\\prod\_\{i\}m\_\{i,0\}m\_\{i,1\}\.\(S20\)Combining the identities and restoring homogeneity proves the inequality\. TheW=0W=0case is immediate\. Equality requires determinants in\{0,±1\}\\\{0,\\pm 1\\\}on positive\-probability tuples and diagonal covariance\. The supplied formal proof excludes simultaneous equality with all facet masses positive ford≥3d\\geq 3, using rational pivots, integer clearing, and a two\-level separating construction\. A zero facet confines the support to a hyperplane and gives equality directly\.

The reported Lean 4\.19 chain proves the finite\-polynomial inequality and equality characterization, including rejection of an incorrect equality mutation\. The relation to the geometric conjecture of[Averkov et al\. \(2026\)](https://arxiv.org/html/2610.06986#bib.bib4)still requires the complete zonoid/mixed\-volume bridge and external statement\-alignment review; we do not silently promote the polynomial result to every geometric formulation\.

#### J\.1\.1Deriving the determinant second\-moment identity

LetZ=\(1,X⊤\)⊤Z=\(1,X^\{\\top\}\)^\{\\top\}and letZ0,…,ZdZ\_\{0\},\\ldots,Z\_\{d\}be independent copies\. Write the affine determinant as the determinant of the matrix with these columns\. Expanding its square produces a double sum over permutations\. Independence lets each term factor into entries of the second\-moment matrixG=𝔼⁡\[Z​Z⊤\]G=\\mathbb\{E\}\[ZZ^\{\\top\}\]\. Regrouping the permutation sums yields

𝔼​det\(Z0,…,Zd\)2=\(d\+1\)\!​detG\.\\mathbb\{E\}\\det\(Z\_\{0\},\\ldots,Z\_\{d\}\)^\{2\}=\(d\+1\)\!\\det G\.\(S21\)The block matrix has the form

G=\(1μ⊤μ𝔼⁡\[X​X⊤\]\),μ=𝔼​X\.G=\\begin\{pmatrix\}1&\\mu^\{\\top\}\\\\ \\mu&\\mathbb\{E\}\[XX^\{\\top\}\]\\end\{pmatrix\},\\qquad\\mu=\\mathbb\{E\}X\.\(S22\)Subtracting the mean contribution through the Schur complement givesdetG=det\(𝔼⁡\[X​X⊤\]−μ​μ⊤\)=detCov⁡\(X\)\\det G=\\det\(\\mathbb\{E\}\[XX^\{\\top\}\]\-\\mu\\mu^\{\\top\}\)=\\det\\Cov\(X\)\. This establishes the stated identity without requiring a dimension\-specific polynomial expansion\.

The conversion from the ordered random sample to the unordered simplex polynomial also has a precise multiplicity\. Tuples with repeated vertices contribute zero determinant\. Each\(d\+1\)\(d\+1\)\-element vertex set appears in\(d\+1\)\!\(d\+1\)\!orders with equal absolute determinant and product weight\. Dividing by this factorial is therefore required; omitting it would alter the theorem’s normalization\. The powers ofWWthen restore the degree\-2​d2dhomogeneous inequality\.

#### J\.1\.2Equality requires two simultaneous rigidities

The integrality step is sharp exactly when every positive\-probability determinant has absolute value zero or one\. The covariance step is sharp when the relevant covariance matrix satisfies the equality condition of Hadamard’s inequality\. If a facet mass is zero, the support lies in a coordinate hyperplane, so all full\-dimensional determinants vanish and both sides are zero\.

The difficult direction is excluding equality when all facet masses are positive in dimension at least three\. The first inequality constrains affine determinants of the support, while the second constrains its mixed moments\. Neither condition alone excludes many nondegenerate distributions\. The formal equality argument connects them through the supplied rational\-pivot and separator construction\. This is a separate proof component, not an automatic corollary of writing down the covariance inequality\.

The low\-dimensional cases are deliberately outside the statedd≥3d\\geq 3iff classification\. The inequality holds for all positive dimensions, but equality can have a different structure in dimensions one and two\. Preserving the dimension qualifier prevents a true general inequality from carrying an overgeneralized equality statement\.

#### J\.1\.3Formal statement alignment and geometric interpretation

The Lean result checks a finite polynomial built from cube vertices, weights, and determinant coefficients\. The source geometric question involves zonoids and mixed\-volume formulations\. Even if the finite inequality is the central algebraic obstruction, transferring the formal theorem to an external geometric claim requires the exact reduction, its normalization, and its hypotheses\. A proof assistant cannot fill that bridge merely because both discussions use the word “Hypercube\.”

This case therefore has two distinct strengths: a short reusable proof mechanism for the inequality, and a reported complete formal chain for the finite statement including equality\. Its remaining external gate is alignment and priority, rather than an unproved finite polynomial calculation\. That status differs substantially from the kernel\-only formalizations in the later analytic cases\.

### J\.2H\-beta front\-loading: a nine\-element counterexample

Figure S7:The H\-beta counterexample and its family mechanism\. \(a\) Exact supplied graded dimensions show the middle coefficients changing from\(27,27\)\(27,27\)to\(31,32\)\(31,32\), violating the registered front\-loading inequality\. \(b\) Subtraction in the retained family formula givesh2β−h3β=−1h\_\{2\}^\{\\beta\}\-h\_\{3\}^\{\\beta\}=\-1for everya,d≥0a,d\\geq 0; the plotted parameter range is an illustration of that identity, not an exhaustive experimental verification of the infinite family\.Figure[S7](https://arxiv.org/html/2610.06986#A10.F7)shows why the counterexample is structurally persistent: both middle coefficients grow by the same extension term, preserving a one\-unit defect\.

For the registered rank\-five convention, the tested front\-loading condition ish2β≥h3βh\_\{2\}^\{\\beta\}\\geq h\_\{3\}^\{\\beta\}\. The retained simple nine\-element matroidM​195313M195313has

flat\-layer counts=\(1,9,32,49,27,1\),\\displaystyle=\(1,9,32,49,27,1\),\#​bases\\displaystyle\\\#\\text\{bases\}=67,\\displaystyle=67,\(S23\)H0\\displaystyle H\_\{0\}=\(1,9,27,27,9,1\),\\displaystyle=\(1,9,27,27,9,1\),Hβ\\displaystyle H\_\{\\beta\}=\(1,9,31,32,9,1\),\\displaystyle=\(1,9,31,32,9,1\),\(S24\)Hβ−H0\\displaystyle H\_\{\\beta\}\-H\_\{0\}=\(0,0,4,5,0,0\)\.\\displaystyle=\(0,0,4,5,0,0\)\.\(S25\)Thush2β−h3β=−1h\_\{2\}^\{\\beta\}\-h\_\{3\}^\{\\beta\}=\-1, and the corresponding difference\-vector defect is also−1\-1\. The source’s differential\-degree conventions must be matched explicitly when relating this computation to the conjectures of[Sinclair \(2026\)](https://arxiv.org/html/2610.06986#bib.bib26); the counterexample does not refute adjacent log\-concavity statements\.

Eight ranked cyclic flats determine all 512 subset ranks\. The verification chain checks rank normalization, monotonicity, all submodularity inequalities, simplicity, flats and covers, and an independent reconstruction of the 67 bases\. Exact rational atom spaces andDβD\_\{\\beta\}cover matrices produce the graded dimensions through column\-space recursion\. DisablingDβD\_\{\\beta\}changes the dimensions and is rejected\. The concrete finite statement is reported in two independently structured mechanized developments\.

Principal extensions along two cyclic rank\-two lines produce parametersa,d≥0a,d\\geq 0with retained formula

Hβ=\(CLOSE1,9\+a\+d,31\+6​\(a\+d\)\+a​d,OPEN32\+6​\(a\+d\)\+a​d,9\+a\+d,1\)\.\\begin\{split\}H\_\{\\beta\}=\\big\(&1,9\+a\+d,31\+6\(a\+d\)\+ad,\\\\ &32\+6\(a\+d\)\+ad,9\+a\+d,1\\big\)\.\\end\{split\}\(S26\)The middle defect remains−1\-1throughout the family\. Two exact implementations support the family formula, which is not covered by the concrete Lean counterexample\.

#### J\.2\.1From a combinatorial object to a Hilbert\-series counterexample

The counterexample begins with a matroid, not with an arbitrary proposed coefficient sequence\. A sequence violating front\-loading is relevant only if it is produced by the radial construction applied to a valid matroid\. The verifier therefore starts with the subset\-rank function and checks the matroid axioms before building the graded operators\. The 512\-subset domain is exhaustive for a nine\-element ground set\.

Rank normalization, monotonicity, and submodularity serve different purposes\. Normalization fixes the empty\-set rank and basic bounds; monotonicity controls inclusions; submodularity ensures the rank function has the required exchange structure\. Simplicity excludes loops and parallel elements under the stated convention\. The independent basis reconstruction checks that the resulting combinatorial object agrees with the reported 67 bases rather than only with a cached list of flats\.

The algebraic stage builds rational atom spaces and the radial lowering operator\. Its exact column\-space recursion computes dimensions, which are integers but can be sensitive to a single omitted operator or an incorrect cover relation\. Floating rank estimates near singularity would be inappropriate here\. Exact rational arithmetic and the formal finite calculation support the displayedH0H\_\{0\},HβH\_\{\\beta\}, and their difference\.

#### J\.2\.2Which conjectural property fails?

The registered middle comparison is31≥3231\\geq 32, which is false by one\. In the difference vector the analogous entries are four and five, also separated by one\. These two numerical defects should not be collapsed into a claim that every proposed positivity property of the Hilbert series fails\. A sequence can violate a front\-loading or symmetry\-related comparison while remaining log\-concave\.

For the concreteHβH\_\{\\beta\}, the neighboring log\-concavity checks include92\>1⋅319^\{2\}\>1\\cdot 31,312\>9⋅3231^\{2\}\>9\\cdot 32,322\>31⋅932^\{2\}\>31\\cdot 9, and92\>32⋅19^\{2\}\>32\\cdot 1\. Thus the supplied coefficients themselves separate the failed middle comparison from log\-concavity\. The external source uses differential\-degree language, so the map between that convention and the coefficient indexing in this manuscript remains an explicit alignment requirement\.

#### J\.2\.3Why the infinite family adds information

Writes=a\+ds=a\+d\. The middle entries of the extension\-family formula are31\+6​s\+a​d31\+6s\+adand32\+6​s\+a​d32\+6s\+ad\. Subtracting cancels every parameter\-dependent contribution and leaves−1\-1\. The defect is therefore structurally stable under the registered principal extensions\. This is stronger evidence about the failure mechanism than a single exceptional catalogue entry\.

The two\-parameter formula follows inductively from the extension increments\. Increasingaaby one changes the coefficient vector by

\(0,1,6\+d,6\+d,1,0\),\(0,1,6\+d,6\+d,1,0\),\(S27\)while increasingddby one changes it by\(0,1,6\+a,6\+a,1,0\)\(0,1,6\+a,6\+a,1,0\)\. Starting fromHβ​\(0,0\)=\(1,9,31,32,9,1\)H\_\{\\beta\}\(0,0\)=\(1,9,31,32,9,1\), summing the first recurrenceaatimes and the secondddtimes gives

Hβ​\(a,d\)=\(1,9\+a\+d,31\+6​\(a\+d\)\+a​d,32\+6​\(a\+d\)\+a​d,9\+a\+d,1\)\.H\_\{\\beta\}\(a,d\)=\\bigl\(1,9\+a\+d,31\+6\(a\+d\)\+ad,32\+6\(a\+d\)\+ad,9\+a\+d,1\\bigr\)\.\(S28\)Both middle coordinates receive exactly the same increment at every extension step, so their difference is the invariant−1\-1\. This proves persistence once the principal\-extension recurrences are established from the matroid construction\.

The family formula and its construction are nevertheless different evidence obligations from the concrete nine\-element case\. One must show that every permitted extension produces the claimed matroid structure and that the radial Hilbert computation obeys the stated formulas\. The concrete Lean theorem does not quantify over these extension parameters\. The manuscript attributes the family to the supplied exact implementations and written argument, while reserving full formal status for the finite counterexample\.

### J\.3A nonnegative functional for reversible three\-state kernels

Figure S8:Boundary\-to\-interior proof of the three\-state functional\. Exact rational charts and the spectral tail establish boundary positivity; the mixing identity and nonnegative even traces lift it through the interior\. Together the two branches establishK⁡\(W\)≥0K\(W\)\\geq 0on the registered reversible three\-state domain\.Figure[S8](https://arxiv.org/html/2610.06986#A10.F8)separates the two proof interfaces\. This decomposition makes it possible to inspect large exact certificates while keeping their analytic coverage obligations visible\.

LetJJbe a symmetric nonnegative3×33\\times 3coupling of total mass one with positive row sumsπi\\pi\_\{i\}\. DefinePi​j=Ji​j/πiP\_\{ij\}=J\_\{ij\}/\\pi\_\{i\}andA=P−𝟏​π⊤A=P\-\\mathbf\{1\}\\pi^\{\\top\}\. The retained theorem is

K⁡\(J\)=2​∑i,jJi​jπj2​\(A3\)i​j​\(A5\)i​j\+13​tr⁡\(A8\)\+16​tr⁡\(A4\)2\+252​tr⁡\(A6\)≥0\.\\begin\{split\}K\(J\)=\{\}&2\\sum\_\{i,j\}\\frac\{J\_\{ij\}\}\{\\pi\_\{j\}^\{2\}\}\(A^\{3\}\)\_\{ij\}\(A^\{5\}\)\_\{ij\}\+13\\tr\(A^\{8\}\)\\\\ &\+16\\tr\(A^\{4\}\)^\{2\}\+252\\tr\(A^\{6\}\)\\geq 0\.\\end\{split\}\(S29\)For strictly positiveJJand nonconstant normalized kernelWi​j=Ji​j/\(πi​πj\)W\_\{ij\}=J\_\{ij\}/\(\\pi\_\{i\}\\pi\_\{j\}\), the retained claim is strict positivity\. Related sharp\-10 stability results in the source material apply to its centered rank\-one and lumpable families; they are not generalized here without their full functional definitions\.

##### Mixing reduction\.

Letm=mini​j⁡Wi​jm=\\min\_\{ij\}W\_\{ij\}andλ=1−m\\lambda=1\-m\. Forλ\>0\\lambda\>0, writeW=\(1−λ\)\+λ​W0W=\(1\-\\lambda\)\+\\lambda W\_\{0\}, whereW0W\_\{0\}is nonnegative with a zero entry and the same weighted normalization\. The exact identity is

K⁡\(W\)=λ9​K​\(W0\)\+\(1−λ\)​λ8​\{15​tr⁡\(A08\)\+16​tr⁡\(A04\)2\}\+252​\(λ6−λ9\)​tr⁡\(A06\)\.\\begin\{split\}K\(W\)=\{\}&\\lambda^\{9\}K\(W\_\{0\}\)\+\(1\-\\lambda\)\\lambda^\{8\}\\\{15\\tr\(A\_\{0\}^\{8\}\)\+16\\tr\(A\_\{0\}^\{4\}\)^\{2\}\\\}\\\\ &\+252\(\\lambda^\{6\}\-\\lambda^\{9\}\)\\tr\(A\_\{0\}^\{6\}\)\.\\end\{split\}\(S30\)HereK⁡\(W\)K\(W\)denotes the coupling functional expressed through its normalized kernel\. Reversibility makes the spectrum real, so the even\-power traces are nonnegative\. The constant\-kernel endpoint is handled separately\. The mechanized mixing kernel verifies this closure argument and endpoint algebra\.

##### Boundary certificate\.

For the zero\-diagonal boundary chart, use homogeneous parameters\(0,x,y,u,1−u,z\)\(0,x,y,u,1\-u,z\)withx=u2​\(r\+s\)2x=u^\{2\}\(r\+s\)^\{2\},y=\(1−u\)2​s2y=\(1\-u\)^\{2\}s^\{2\}after the stated chart choice\. Set

L=2​u​\(1−u\)​s​\(r\+s\),U=u⁡\(1−u\)​\(\(r\+s\)2\+s2\)\.L=2u\(1\-u\)s\(r\+s\),\\qquad U=u\(1\-u\)\(\(r\+s\)^\{2\}\+s^\{2\}\)\.\(S31\)For0≤z≤L0\\leq z\\leq L, a 62,151\-term polynomial certificate uses 4,478 exact pairings to absorb 3,583 negative monomials\. ForL≤z≤UL\\leq z\\leq U, a 29,864\-term source polynomial transforms to 141,621 positive nonzero coefficients\. Thez≥Uz\\geq Uspectral tail uses

K≥250​tr⁡\(A6\)\+15​tr⁡\(A8\)\+16​tr⁡\(A4\)2≥0\.K\\geq 250\\tr\(A^\{6\}\)\+15\\tr\(A^\{8\}\)\+16\\tr\(A^\{4\}\)^\{2\}\\geq 0\.\(S32\)Independent implementations vary homogenization, substitution, coordinate ordering, and transforms\. Corrupting pairings or a spectral coefficient is rejected\. The chart discussion here is a proof outline; the supplied exact boundary package carries the full case coverage, including remaining boundary configurations\. The draft does not have those complete certificate files embedded\.

The result concerns three states, not arbitrary graphons or arbitrary\-state rank\-two kernels\. Large rational boundary certificates remain outside full Lean reflection\.

#### J\.3\.1Reversibility and spectral nonnegativity

LetD=diag⁡\(π\)D=\\operatorname\{diag\}\(\\pi\)\. Reversibility givesD​P=P⊤​DDP=P^\{\\top\}D, soD1/2PD−1/2D^\{1/2\}PD^\{\-1/2\}is symmetric\. The centered matrixA=P−𝟏​π⊤A=P\-\\mathbf\{1\}\\pi^\{\\top\}is similar to a symmetric matrix as well\. Its eigenvalues are real, and for every positive integerrr,tr⁡\(A2​r\)\\tr\(A^\{2r\}\)is the sum of nonnegative even powers\. This is the spectral input used by the mixing and tail arguments\.

The normalizationWi​j=Ji​j/\(πi​πj\)W\_\{ij\}=J\_\{ij\}/\(\\pi\_\{i\}\\pi\_\{j\}\)satisfies∑jπj​Wi​j=1\\sum\_\{j\}\\pi\_\{j\}W\_\{ij\}=1\. Hence the minimum entrymmcannot exceed one\. Subtractingmmfrom every entry and dividing by1−m1\-mwhenm<1m<1gives another nonnegative normalized kernel with a zero entry\. Whenm=1m=1, weighted row normalization forces the constant kernel, which is handled as the endpoint rather than through division by zero\.

Under the mixtureW=\(1−λ\)\+λ​W0W=\(1\-\\lambda\)\+\\lambda W\_\{0\}, the centered operator scales asA=λ​A0A=\\lambda A\_\{0\}\. Most terms inKKtherefore scale by their matrix degree\. The term containingJi​jJ\_\{ij\}separates into a constant\-kernel contribution and aW0W\_\{0\}contribution, producing the degree\-eight and degree\-nine pieces in the exact formula\. Tracking these degrees explains why an incorrect coefficient or exponent would invalidate the closure argument\.

#### J\.3\.2Strictness and the limited graph\-density bridge

For a fully positive nonconstant kernel,0<λ<10<\\lambda<1andA0≠0A\_\{0\}\\neq 0\. Similarity to a symmetric matrix impliestr⁡\(A06\)\>0\\tr\(A\_\{0\}^\{6\}\)\>0\. The last mixing term is then strictly positive becauseλ6​\(1−λ3\)\>0\\lambda^\{6\}\(1\-\\lambda^\{3\}\)\>0\. Once boundary nonnegativity is established, this yields strict interior positivity\. This is a precise sufficient chain, not an appeal to numerical positivity at sampled interior points\.

The supplied source relatesKKto a particular coefficient in a graph\-density expansion forK5,5−C10K\_\{5,5\}\-C\_\{10\}\. Nonnegativity of that coefficient is not automatically nonnegativity of the whole graph\-density difference on every kernel\. The sharp\-10 results use additional structure on centered rank\-one or lumpable families\. The manuscript preserves this boundary to avoid promoting a complete three\-state coefficient theorem into general Sidorenko\.

#### J\.3\.3What an exact positivity certificate must establish

A rational certificate has three independent obligations\. First, reconstruct the correct numerator from the original functional after clearing only denominators known to be positive in the chart\. Second, prove the chart and its inequalities cover the assigned boundary region\. Third, expand the proposed nonnegative blocks exactly and show that their sum equals that numerator\. Positive coefficients in a polynomial produced by an incorrect substitution would not establish the theorem\.

The supplied boundary proof separates zero\-off\-diagonal and zero\-diagonal faces, then treats bounded algebraic regions and an unbounded spectral tail\. The detailed sizes quoted earlier concern the zero\-diagonal branch, not every face\. The lower thresholdLLand upper thresholdUUsatisfyU−L=u⁡\(1−u\)​r2≥0U\-L=u\(1\-u\)r^\{2\}\\geq 0in the registered nonnegative chart, so the middle interval is well ordered\. Coverage atu=0,1u=0,1and other degenerate denominators must be handled by the branch contract rather than silently removed\.

Weighted pairings and Bernstein transformations are certificates only after exact reconstruction\. Floating optimization may find promising nonnegative block coefficients; rationalization can change identities or positivity\. The independent expansion and deleted\-pairing control check precisely this transition from a numerical proposal to an exact object\. Full Lean reflection of these large branch certificates is still outstanding\.

### J\.4Symmetric Big\-centroid and Full Perazzo ranks

Figure S9:Consequences of the retained Full Perazzo formulas over an algebraically closed characteristic\-zero field, withq=\(n\+d−2d−1\)q=\\binom\{n\+d\-2\}\{d\-1\}\. \(a\) The ordinary\-to\-border ratiod​q/\(q\+n\)dq/\(q\+n\)approaches the degreedd\(dashed lines\) asnngrows\. \(b\) For cubics, the formulas give distinct border and ordinary rank growth\. Curves are calculated from the stated candidate formulas, not independently measured ranks; their validity depends on the construction and matching lower\-bound arguments\.Figure[S9](https://arxiv.org/html/2610.06986#A10.F9)visualizes the quantitative gap that the two different rank proofs imply\. The border degeneration and the ordinary\-rank decomposition cannot be counted as the same object\.

Over an algebraically closed field of characteristic zero, taken≥2n\\geq 2,d≥3d\\geq 3, and

q=\(n\+d−2d−1\),Bn,d​\(X,Y\)=∑\|α\|=d−1Xα​Yα\.q=\\binom\{n\+d\-2\}\{d\-1\},\\qquad B\_\{n,d\}\(X,Y\)=\\sum\_\{\|\\alpha\|=d\-1\}X\_\{\\alpha\}Y^\{\\alpha\}\.\(S33\)The retained rank formulas are

R¯⁡\(Bn,d\)=R¯W⁡\(Bn,d\)=q\+n,RW​\(Bn,d\)=dq\.\\brank\(B\_\{n,d\}\)=\\brank\_\{\\mathrm\{W\}\}\(B\_\{n,d\}\)=q\+n,\\qquad R\_\{\\mathrm\{W\}\}\(B\_\{n,d\}\)=dq\.\(S34\)Ordinary tensor border rank and symmetric Waring border rank are distinguished in the notation; the shared upper bound follows from a symmetric degeneration, with a matching flattening lower bound\.

##### Cauchy\-star interpolation\.

Choose pairwise distinct scalarsc1,…,cn,t1,…,tn\+d−2c\_\{1\},\\ldots,c\_\{n\},t\_\{1\},\\ldots,t\_\{n\+d\-2\}\. Setg⁡\(z\)=∏i\(z−ci\)g\(z\)=\\prod\_\{i\}\(z\-c\_\{i\}\),p⁡\(z\)=∏j\(z−tj\)p\(z\)=\\prod\_\{j\}\(z\-t\_\{j\}\), andAj​\(Z\)=∑iZi/\(tj−ci\)A\_\{j\}\(Z\)=\\sum\_\{i\}Z\_\{i\}/\(t\_\{j\}\-c\_\{i\}\)\. For an\(n−1\)\(n\-1\)\-subsetIIof thettindices, define

\(vI\)i=∏j∈I\(ci−tj\)g′​\(ci\),ℓI​\(Y\)=∑i\(vI\)i​Yi,HI​\(Z\)=∏j∉IAj​\(Z\)\.\(v\_\{I\}\)\_\{i\}=\\frac\{\\prod\_\{j\\in I\}\(c\_\{i\}\-t\_\{j\}\)\}\{g^\{\\prime\}\(c\_\{i\}\)\},\\quad\\ell\_\{I\}\(Y\)=\\sum\_\{i\}\(v\_\{I\}\)\_\{i\}Y\_\{i\},\\quad H\_\{I\}\(Z\)=\\prod\_\{j\\notin I\}A\_\{j\}\(Z\)\.\(S35\)Partial fractions give

∑i\(vI\)iz−ci=∏j∈I\(z−tj\)g⁡\(z\)\.\\sum\_\{i\}\\frac\{\(v\_\{I\}\)\_\{i\}\}\{z\-c\_\{i\}\}=\\frac\{\\prod\_\{j\\in I\}\(z\-t\_\{j\}\)\}\{g\(z\)\}\.\(S36\)HenceHI​\(vJ\)=0H\_\{I\}\(v\_\{J\}\)=0forI≠JI\\neq J, whileHI​\(vI\)≠0H\_\{I\}\(v\_\{I\}\)\\neq 0\. TheqqpowersℓId−1\\ell\_\{I\}^\{d\-1\}form a basis\. Withfi=p⁡\(ci\)/g′​\(ci\)f\_\{i\}=p\(c\_\{i\}\)/g^\{\\prime\}\(c\_\{i\}\)andλI=\(−1\)d−1/HI​\(vI\)\\lambda\_\{I\}=\(\-1\)^\{d\-1\}/H\_\{I\}\(v\_\{I\}\), the retained interpolation identity is

∑IλI​ℓI​\(Y\)d=∑ifi​Yid\.\\sum\_\{I\}\\lambda\_\{I\}\\ell\_\{I\}\(Y\)^\{d\}=\\sum\_\{i\}f\_\{i\}Y\_\{i\}^\{d\}\.\(S37\)Solving the first\-order coefficient identity for linear formsδI​\(X\)\\delta\_\{I\}\(X\)yields

Bn,d=limε→0ε−1​\[∑IλI​\(ℓI\+ε​δI\)d−∑ifi​Yid\]\.B\_\{n,d\}=\\lim\_\{\\varepsilon\\to 0\}\\varepsilon^\{\-1\}\\left\[\\sum\_\{I\}\\lambda\_\{I\}\(\\ell\_\{I\}\+\\varepsilon\\delta\_\{I\}\)^\{d\}\-\\sum\_\{i\}f\_\{i\}Y\_\{i\}^\{d\}\\right\]\.\(S38\)TheqqindependentXαX\_\{\\alpha\}derivatives andnnindependentYiY\_\{i\}derivatives give catalecticant rankq\+nq\+n: the former lie in pureYYdegree, while the latter contain distinctX\(d−1\)​ei​Yid−2X\_\{\(d\-1\)e\_\{i\}\}Y\_\{i\}^\{d\-2\}terms\.

##### Ordinary Waring rank\.

The retained Schur–Kneser argument forF=∑iXi​Qi​\(Y\)\+G⁡\(Y\)F=\\sum\_\{i\}X\_\{i\}Q\_\{i\}\(Y\)\+G\(Y\)givesRW​\(F\)≥d​ρR\_\{\\mathrm\{W\}\}\(F\)\\geq d\\rho, whereρ=dimspan⁡\{Qi\}\\rho=\\dim\\operatorname\{span\}\\\{Q\_\{i\}\\\}\. It uses vanishing secondXXderivatives, orthogonality of coordinatewise product spaces, simultaneous stabilizer blocks, and a Kneser dimension bound in each block\. For Full Perazzo,ρ=q\\rho=q\. The matching upper bound decomposes each binary tangent form as

W​Ld−1=∑j=1dμj​\(L\+tj​W\)dWL^\{d\-1\}=\\sum\_\{j=1\}^\{d\}\\mu\_\{j\}\(L\+t\_\{j\}W\)^\{d\}\(S39\)under the corresponding moment equations\. A mechanized binary\-tangent kernel proves that algebraic identity over a characteristic\-zero field; it does not formalize the full Schur–Kneser lower\-bound chain or guarantee every interpolation hypothesis automatically\. The resulting ratiod​q/\(q\+n\)→ddq/\(q\+n\)\\to dfor fixedddgives the stated obstruction to a smaller universal linear debordering coefficient on this family\. External algebraic\-geometric and priority review remains necessary; full border\-VSP classification is not claimed\.

#### J\.4\.1Why the interpolation family has exactly the required size

There are\(n\+d−2n−1\)=q\\binom\{n\+d\-2\}\{n\-1\}=qsubsetsIIof sizen−1n\-1, matching the dimension of homogeneous degree\-d−1d\-1forms innnvariables\. EachHIH\_\{I\}also has degreed−1d\-1, because its product containsd−1d\-1omittedttindices\. The diagonal evaluation matrixHI​\(vJ\)H\_\{I\}\(v\_\{J\}\)therefore witnesses interpolation rather than merely supplying many candidate linear forms\.

IfI≠JI\\neq Jhave equal size, some index inJJis absent fromII\. That index occurs in the product definingHIH\_\{I\}, and the partial\-fraction identity makes the corresponding factor vanish atvJv\_\{J\}\. On the diagonal, the pairwise\-distinct parameter condition prevents the necessary factors from vanishing\. This explains the off\-diagonal zero pattern and the nonzero diagonal without relying on a finite symbolic example\.

The basis property ofℓId−1\\ell\_\{I\}^\{d\-1\}lets theXα​YαX\_\{\\alpha\}Y^\{\\alpha\}target be expressed in the tangent span of theddth powers\. The constant identity then cancels the degree\-zero part\. The field must allow the scalar operations and degree factors used in the tangent construction; the displayed Waring statement is therefore made in characteristic zero rather than casually transferred to small characteristic\.

#### J\.4\.2Flattening lower bound and ordinary rank are different arguments

The first derivative space ofBn,dB\_\{n,d\}has dimensionq\+nq\+n\. Derivatives with respect to theXXvariables span all degree\-d−1d\-1monomials inYY\. Derivatives with respect to theYYvariables have positiveXXdegree and are independent through the distinguished terms specified above\. The two subspaces have differentXXdegrees and intersect trivially\. A rank\-one symmetric tensor contributes at most one dimension to this flattening, so the dimension gives a border\-rank lower bound\.

That lower bound does not produce the larger ordinary Waring rankd​qdq\. Ordinary rank needs the stronger product\-space argument\. In any proposed decomposition, vanishing second derivatives in theXXvariables creates algebraic relations among coordinatewise products of coefficient vectors\. The retained Schur–Kneser proof organizes these relations by stabilizer blocks and sums the resulting block lower bounds\. Its dependencies and equality hypotheses require specialist verification; the binary tangent identity alone cannot establish the lower bound\.

The upper ordinary\-rank construction uses a different count: each of theqqtangent monomials is expressed usingddpowers, yieldingd​qdqterms\. Matching this explicit upper bound with the independent lower bound yields equality\. Distinguishing the two proofs prevents the border construction from being mistaken for a finite exact decomposition of lengthq\+nq\+n\.

#### J\.4\.3Binary tangent identity and debordering interpretation

Expanding a proposed block gives

∑jμj​\(L\+tj​W\)d=∑k=0d\(dk\)​Ld−k​Wk​∑jμj​tjk\.\\sum\_\{j\}\\mu\_\{j\}\(L\+t\_\{j\}W\)^\{d\}=\\sum\_\{k=0\}^\{d\}\\binom\{d\}\{k\}L^\{d\-k\}W^\{k\}\\sum\_\{j\}\\mu\_\{j\}t\_\{j\}^\{k\}\.\(S40\)To obtainW​Ld−1WL^\{d\-1\}, its moments must satisfyd​∑jμj​tj=1d\\sum\_\{j\}\\mu\_\{j\}t\_\{j\}=1and make every other relevant moment vanish\. The Lean kernel checks this implication from the supplied moment conditions\. Existence of a suitable choice of weights and parameters is a separate algebraic construction, not a consequence of the implication alone\.

Over an algebraically closed characteristic\-zero field, that existence can be written explicitly\. Letζ\\zetabe a primitiveddth root of unity and settj=ζjt\_\{j\}=\\zeta^\{j\}andμj=ζ−j/d2\\mu\_\{j\}=\\zeta^\{\-j\}/d^\{2\}for0≤j<d0\\leq j<d\. Orthogonality of roots of unity gives

∑j=0d−1μj​tjk=1d2​∑j=0d−1ζj⁡\(k−1\)=\{1/d,k=1,0,0≤k≤d,k≠1\.\\sum\_\{j=0\}^\{d\-1\}\\mu\_\{j\}t\_\{j\}^\{k\}=\\frac\{1\}\{d^\{2\}\}\\sum\_\{j=0\}^\{d\-1\}\\zeta^\{j\(k\-1\)\}=\\begin\{cases\}1/d,&k=1,\\\\ 0,&0\\leq k\\leq d,\\ k\\neq 1\.\\end\{cases\}\(S41\)Substitution into the binomial expansion leaves exactly

W​Ld−1=1d2​∑j=0d−1ζ−j​\(L\+ζj​W\)d\.WL^\{d\-1\}=\\frac\{1\}\{d^\{2\}\}\\sum\_\{j=0\}^\{d\-1\}\\zeta^\{\-j\}\(L\+\\zeta^\{j\}W\)^\{d\}\.\(S42\)Thus every binary tangent block has an explicitdd\-term Waring decomposition\. Applying the identity to theqqindependent tangent blocks givesRW​\(Bn,d\)≤d​qR\_\{\\mathrm\{W\}\}\(B\_\{n,d\}\)\\leq dqwith no interpolation limit in this final ordinary\-rank step\.

For the matching lower bound, write a putative decomposition asF=∑s=1rLsdF=\\sum\_\{s=1\}^\{r\}L\_\{s\}^\{d\}and split eachLsL\_\{s\}into itsXXandYYparts\. The vanishing of every secondXXderivative gives, for allXX\-directionsa,ba,b,

∑s=1ra⁡\(Ls\)​b​\(Ls\)​Lsd−2=0\.\\sum\_\{s=1\}^\{r\}a\(L\_\{s\}\)b\(L\_\{s\}\)L\_\{s\}^\{d\-2\}=0\.\(S43\)The firstXXderivatives span theqq\-dimensional space generated by the formsQα​\(Y\)=YαQ\_\{\\alpha\}\(Y\)=Y^\{\\alpha\}\. Grouping equalYY\-directions into stabilizer blocks turns the displayed quadratic relations into orthogonality constraints on coordinatewise\-product subspaces\. The source Schur–Kneser lemma bounds each block byddtimes the dimension it contributes tospan⁡\{Qα\}\\operatorname\{span\}\\\{Q\_\{\\alpha\}\\\}; summing the blocks yieldsr≥d​qr\\geq dq\. Together with the explicit root\-of\-unity construction, this closesRW​\(Bn,d\)=d​qR\_\{\\mathrm\{W\}\}\(B\_\{n,d\}\)=dqunder the lemma’s stated characteristic\-zero hypotheses\.

For fixedd≥3d\\geq 3,qqgrows as a polynomial of degreed−1d\-1innn, son/q→0n/q\\to 0\. Consequentlyd​q/\(q\+n\)→ddq/\(q\+n\)\\to d\. The interpretation is a family\-specific obstruction to universally replacing border decompositions by ordinary Waring decompositions with a coefficient belowdd\. It does not classify every minimal limiting support\. The non\-CB boundary counterexample in the auxiliary catalogue illustrates why that stronger geometric inference would be false\.

### J\.5Heisenberg determinant limits and chain dependence

Figure S10:Formula\-level illustration of the Heisenberg limit candidate atm=2m=2\. \(a\) Each point is21/\(p\+1\)2^\{1/\(p\+1\)\}for a different odd\-prime principal chain; the dashed line is the infinite Fuglede–Kadison determinant, 2\. \(b\) The corresponding log defect isp​log⁡\(2\)/\(p\+1\)p\\log\(2\)/\(p\+1\)\. Lines connect selected prime parameters only as visual guides\. These are candidate limiting values, not finite\-qqmeasurements or a numerical convergence test\.Figure[S10](https://arxiv.org/html/2610.06986#A10.F10)exposes the claimed chain dependence without extrapolating the small finite determinant controls\. Establishing each limit still requires uniform packet estimates\.

In the integer Heisenberg group, setAm=1−m​a\+m​bA\_\{m\}=1\-ma\+mbfor integerm≥2m\\geq 2\. For finite principal quotients atq=piq=p^\{i\}, define the reported normalization byDq​\(Am\)=\|detAm,q\|1/q3D\_\{q\}\(A\_\{m\}\)=\|\\det A\_\{m,q\}\|^\{1/q^\{3\}\}when the finite determinant is nonzero\. Under the retained principal\-chain hypotheses with odd primepp, the candidate limit is

Dq​\(Am\)⟶m1/\(p\+1\),D\_\{q\}\(A\_\{m\}\)\\longrightarrow m^\{1/\(p\+1\)\},\(S44\)whereas the cited infinite Fuglede–Kadison determinant ismm\. The logarithmic defect isp​log⁡m/\(p\+1\)p\\log m/\(p\+1\)\. The designated\(p,m\)=\(3,2\)\(p,m\)=\(3,2\)special case gives21/42^\{1/4\}\. This is presented as an exact\-limit follow\-up to the determinant\-approximation counterexample of[Kammeyer \(2026\)](https://arxiv.org/html/2610.06986#bib.bib13), not as rediscovery of that original counterexample\.

##### Finite representation packets\.

For exact central orderd\|qd\\mid q, putn=q/dn=q/d\. Irreducible packets have dimensionddand parameters\(u,v\)∈μn2\(u,v\)\\in\\mu\_\{n\}^\{2\}, with regular\-representation dimension check

∑d\|qφ⁡\(d\)​n2​d2=q3\.\\sum\_\{d\\mid q\}\\varphi\(d\)n^\{2\}d^\{2\}=q^\{3\}\.\(S45\)For odd\-order packets, the quantum\-binomial and trace identities forT=ρ⁡\(a\)−ρ⁡\(b\)T=\\rho\(a\)\-\\rho\(b\)giveTd=\(u−v\)​IT^\{d\}=\(u\-v\)Iand the reverse characteristic polynomial, yielding

det\(I−m​T\)=1−md​\(u−v\)\.\\det\(I\-mT\)=1\-m^\{d\}\(u\-v\)\.\(S46\)The mechanized finite\-packet kernel proves the implication from the reverse characteristic polynomial to this determinant identity\. Representation classification, multiplicities, packet hypotheses, and the complete resultant product remain external to that kernel\.

##### Limit mechanism and controls\.

Complete Galois packets combine all central orders\. Smalldduse a nonzero integer norm for a lower bound; largedduse main\-term dominance and root\-of\-unity spacing\. Uniform normalized error estimates then supply the asserted limit\. These analytic estimates are a necessary proof layer; finite determinant agreement alone does not establish convergence\.

Direct integer matrices and resultant controls include\(q,m\)=\(3,2\),\(3,3\),\(5,2\),\(9,2\),\(2,2\),\(4,2\),\(6,2\),\(8,2\)\(q,m\)=\(3,2\),\(3,3\),\(5,2\),\(9,2\),\(2,2\),\(4,2\),\(6,2\),\(8,2\), with largest matrix dimension 729\. The determinant is 1,729 at\(3,2\)\(3,2\)and−735\-735at the even control\(2,2\)\(2,2\), requiring an absolute\-determinant convention\. Even controls use their appropriate packet rules, not an unchecked extension of the odd\-order identity\. Follow\-up chain classifications, nonconvergence constructions, and cofinal recovery claims remain within this specialist research line; the current manuscript does not treat them as additional independent discoveries\.

#### J\.5\.1Regular\-representation multiplicities and determinant products

The finite quotient has orderq3q^\{3\}\. Its regular representation contains each irreducible representation with multiplicity equal to its dimension\. Therefore an irreducible packet determinant must be raised to that multiplicity when reconstructing the full determinant\. The identity∑d\|qφ⁡\(d\)​n2​d2=q3\\sum\_\{d\\mid q\}\\varphi\(d\)n^\{2\}d^\{2\}=q^\{3\}checks the dimension accounting, but a complete reconstruction must also ensure that the packets are neither omitted nor duplicated\.

Writing𝒫d\\mathcal\{P\}\_\{d\}for the packets of exact central orderddandΔd,u,v=1−md​\(u−v\)\\Delta\_\{d,u,v\}=1\-m^\{d\}\(u\-v\), the regular determinant has the product form

\|detAm,q\|=∏d\|q∏\(u,v\)∈𝒫d\|Δd,u,v\|d\.\|\\det A\_\{m,q\}\|=\\prod\_\{d\\mid q\}\\prod\_\{\(u,v\)\\in\\mathcal\{P\}\_\{d\}\}\|\\Delta\_\{d,u,v\}\|^\{d\}\.\(S47\)Consequently its normalized logarithm is

log⁡Dq​\(Am\)=1q3​∑d\|qd​∑\(u,v\)∈𝒫dlog⁡\|1−md​\(u−v\)\|\.\\log D\_\{q\}\(A\_\{m\}\)=\\frac\{1\}\{q^\{3\}\}\\sum\_\{d\\mid q\}d\\sum\_\{\(u,v\)\\in\\mathcal\{P\}\_\{d\}\}\\log\|1\-m^\{d\}\(u\-v\)\|\.\(S48\)This formula identifies exactly what the limit proof must control: packet multiplicities, the maind​log⁡md\\log mcontribution, and the logarithmic error caused by possible proximity ofu−vu\-vtom−dm^\{\-d\}\.

The scalar identitydet\(I−m​T\)=1−md​\(u−v\)\\det\(I\-mT\)=1\-m^\{d\}\(u\-v\)simplifies each packet dramatically\. It does not itself determine how frequently a given\(d,u,v\)\(d,u,v\)occurs\. This is why packet algebra and representation classification are listed as separate verification layers\. Incorrect multiplicities can preserve each packet identity while giving the wrong normalized finite determinant and limiting exponent\.

The reverse characteristic polynomial is convenient because it encodesdet\(I−z​T\)\\det\(I\-zT\)directly\. If it equals1−c​zd1\-cz^\{d\}, substitutingz=mz=mproves the packet formula\. The Lean kernel formalizes this algebraic implication\. The quantum\-binomial relation and vanishing lower traces are the mathematical route to its hypothesis in the registered representation family; they remain to be connected formally for the full theorem\.

#### J\.5\.2Why exact finite controls do not establish the limit

Agreement between direct integer determinants and resultants atq≤9q\\leq 9tests packet reconstruction, signs, and normalization in concrete cases\. It cannot prove convergence asi→∞i\\to\\infty\. A limiting formula needs an error estimate that remains valid over all packets and all levels in the chain\. Near\-cancellation in factors of the form1−md​\(u−v\)1\-m^\{d\}\(u\-v\)is especially relevant after taking logarithms\.

The retained proof divides the packets into small and large central orders\. Complete Galois products at small orders are nonzero integers, giving a lower bound that would not be available for an isolated small complex factor\. At large orders, dominant terms and spacing among roots of unity control the normalized error\. The cutoff and uniform estimates are part of the analytic proof, not parameters chosen to fit the finite determinant values\.

More explicitly, choose a cutoffD=D⁡\(q\)D=D\(q\)withD→∞D\\to\\inftyandD=o⁡\(q\)D=o\(q\)\. Ford≤Dd\\leq D, combine every Galois orbit before taking logarithms\. Nonvanishing of the resulting integer norm prevents an individual near\-zero complex factor from producing an uncontrolled negative contribution; the total small\-order contribution iso⁡\(q3\)o\(q^\{3\}\)after normalization\. Ford\>Dd\>D, factor

1−md​\(u−v\)=md​\(u−v\)​\(1−1md​\(u−v\)\)\.1\-m^\{d\}\(u\-v\)=m^\{d\}\(u\-v\)\\left\(1\-\\frac\{1\}\{m^\{d\}\(u\-v\)\}\\right\)\.\(S49\)The first factor suppliesd​log⁡md\\log mplus the root\-of\-unity termlog⁡\|u−v\|\\log\|u\-v\|\. The spacing estimate controls the latter after complete packet summation, whilem−dm^\{\-d\}makes the last logarithm uniformly summable away from the paired zero modes\. Under the retained packet\-counting lemma, the coefficient oflog⁡m\\log mconverges to1/\(p\+1\)1/\(p\+1\)and every residual sum iso⁡\(1\)o\(1\)after division byq3q^\{3\}\. Exponentiating therefore givesDq​\(Am\)→m1/\(p\+1\)D\_\{q\}\(A\_\{m\}\)\\to m^\{1/\(p\+1\)\}\.

Taking logarithms of the claimed limit gives\(log⁡m\)/\(p\+1\)\(\\log m\)/\(p\+1\), while the infinite determinant has logarithmlog⁡m\\log m\. Their difference isp​log⁡m/\(p\+1\)p\\log m/\(p\+1\)\. This elementary consequence makes the size of the defect explicit but does not replace the convergence argument\. It also emphasizes chain dependence: a different quotient chain may have a different packet distribution and a different limit or no limit\.

#### J\.5\.3Sign conventions and specialist review

The negative even\-level determinant−735\-735is a useful convention check\. A normalized determinant intended to compare with a positive Fuglede–Kadison determinant must use the registered absolute or appropriate singular\-value convention\. Copying the odd\-order packet formula into an even\-level test without adjusting its hypotheses would be a separate error\. The manuscript reports the even controls precisely to make such convention failures visible\.

The source counterexample demonstrates the failure of determinant approximation\. The exact limit and chain classifications are subsequent results that call for an independent operator\-algebraic analysis\. Although the formal determinant identity provides substantial and reusable evidence, the principal analytical challenge lies beyond the identity itself\.

### J\.6Online permutation embedding: alternating\-family asymptotics

Figure S11:Analytic structure of the alternating\-family expansion\. \(a\) The critical equationsinh⁡\(2​u∗\)−2​u∗=1\\sinh\(2u\_\{\*\}\)\-2u\_\{\*\}=1determinesa=cosh2⁡\(u∗\)/4a=\\cosh^\{2\}\(u\_\{\*\}\)/4and the logarithmic coefficient\. \(b\) The plotted quantity is only the explicit correctionb​log⁡\(k\)/kb\\log\(k\)/ktoβ⁡\(Altk\)/k2\\beta\(\\operatorname\{Alt\}\_\{k\}\)/k^\{2\}, whereb=sinh2⁡\(u∗\)/6b=\\sinh^\{2\}\(u\_\{\*\}\)/6; the unknownO⁡\(k\)O\(k\)remainder in the unnormalized expansion is not plotted\. These are formula illustrations, separate from the reported Arb dynamic\-programming checks\.Figure[S11](https://arxiv.org/html/2610.06986#A10.F11)connects the scalar critical point to the scale of the logarithmic term\. It does not plot new dynamic\-programming observations or assert global optimality of the alternating family\.

LetAltk\\operatorname\{Alt\}\_\{k\}denote the alternating increasing family andβ\\betathe objective of the source online embedding problem\([Altschuler et al\., 2026](https://arxiv.org/html/2610.06986#bib.bib2)\)\. Letu∗\>0u\_\{\*\}\>0solvesinh⁡\(2​u∗\)−2​u∗=1\\sinh\(2u\_\{\*\}\)\-2u\_\{\*\}=1\. The retained asymptotic candidate is

β⁡\(Altk\)k2⟶cosh2⁡u∗4≈0\.49\.\\frac\{\\beta\(\\operatorname\{Alt\}\_\{k\}\)\}\{k^\{2\}\}\\longrightarrow\\frac\{\\cosh^\{2\}u\_\{\*\}\}\{4\}\\approx 0\.49\.\(S50\)More precisely, for parity constantsC0,C1C\_\{0\},C\_\{1\},

β⁡\(Altk\)=cosh⁡u∗2​k\+sinh2⁡u∗6coshu∗​log⁡k\+Ckmod2\+o⁡\(1\),β⁡\(Altk\)=cosh2⁡u∗4​k2\+sinh2⁡u∗6​k​log⁡k\+O⁡\(k\)\.\\begin\{split\}\\sqrt\{\\beta\(\\operatorname\{Alt\}\_\{k\}\)\}=\{\}&\\frac\{\\cosh u\_\{\*\}\}\{2\}k\+\\frac\{\\sinh^\{2\}u\_\{\*\}\}\{6\\cosh u\_\{\*\}\}\\log k\+C\_\{k\\bmod 2\}\+o\(1\),\\\\ \\beta\(\\operatorname\{Alt\}\_\{k\}\)=\{\}&\\frac\{\\cosh^\{2\}u\_\{\*\}\}\{4\}k^\{2\}\+\\frac\{\\sinh^\{2\}u\_\{\*\}\}\{6\}k\\log k\+O\(k\)\.\\end\{split\}\(S51\)
##### Recurrence mechanism\.

The alternating\-tree root splits into one singleton and an alternating subtree of sizek−2k\-2, givingSk=Φ⁡\(Sk−2\)S\_\{k\}=\\Phi\(S\_\{k\-2\}\)forSk=β⁡\(Altk\)S\_\{k\}=\\sqrt\{\\beta\(\\operatorname\{Alt\}\_\{k\}\)\}\. The retained Bellman\-residual expansion is

P1,s2​\(u\)=sinh⁡\(2​u\)−2​u−8​sinh3⁡u3​s\+O⁡\(s−2\)\.P\_\{1,s^\{2\}\}\(u\)=\\sinh\(2u\)\-2u\-\\frac\{8\\sinh^\{3\}u\}\{3s\}\+O\(s^\{\-2\}\)\.\(S52\)The root condition yieldsus=u∗\+2​sinh⁡\(u∗\)/\(3​s\)\+O⁡\(s−2\)u\_\{s\}=u\_\{\*\}\+2\\sinh\(u\_\{\*\}\)/\(3s\)\+O\(s^\{\-2\}\), and hence

Φ⁡\(s\)−s=cosh⁡u∗\+sinh2⁡u∗6​s\+O⁡\(s−2\)\.\\Phi\(s\)\-s=\\cosh u\_\{\*\}\+\\frac\{\\sinh^\{2\}u\_\{\*\}\}\{6s\}\+O\(s^\{\-2\}\)\.\(S53\)Summation along each parity class gives the linear and logarithmic terms\. This step requires uniform error control in the Bellman expansion, beyond the formal algebraic kernel\.

Withx=e−2​ux=e^\{\-2u\}, the variational objective becomesH⁡\(u\)=\(1\+2​u\)​coth⁡\(u\)/8H\(u\)=\(1\+2u\)\\coth\(u\)/8\. Its derivative has the sign ofsinh⁡\(2​u\)−2​u−1\\sinh\(2u\)\-2u\-1, giving a unique minimizeru∗u\_\{\*\}andH⁡\(u∗\)=cosh2⁡u∗/4H\(u\_\{\*\}\)=\\cosh^\{2\}u\_\{\*\}/4\. A mechanized scalar kernel proves the critical\-equation rewrite and coefficient normalization\. Root uniqueness and recurrence asymptotics are not included in that scope\.

Two outward\-rounded Arb dynamic programs support finite optimality of the alternating family within the frozen finite problem fork≤5000k\\leq 5000\. The reported finite second\-order estimates both round to 0\.11 and approach the exact expressionsinh2⁡\(u∗\)/\(6​cosh⁡\(u∗\)\)≈0\.11\\sinh^\{2\}\(u\_\{\*\}\)/\(6\\cosh\(u\_\{\*\}\)\)\\approx 0\.11, the logarithmic coefficient inβ\\sqrt\{\\beta\}; thek​log⁡kk\\log kcoefficient inβ\\betais insteadsinh2⁡\(u∗\)/6≈0\.16\\sinh^\{2\}\(u\_\{\*\}\)/6\\approx 0\.16\. This agreement links the finite dynamic programs to the analytic expansion\.

#### J\.6\.1The critical equation and its unique positive solution

Definef⁡\(u\)=sinh⁡\(2​u\)−2​u−1f\(u\)=\\sinh\(2u\)\-2u\-1foru≥0u\\geq 0\. Thenf⁡\(0\)=−1f\(0\)=\-1,f⁡\(u\)→∞f\(u\)\\to\\infty, andf′​\(u\)=2​cosh⁡\(2​u\)−2\>0f^\{\\prime\}\(u\)=2\\cosh\(2u\)\-2\>0foru\>0u\>0\. Thus continuity and strict monotonicity give exactly one positive root\. This elementary argument is a written derivation here; the supplied Lean kernel is reported only for the critical identity and coefficient normalization\.

ForH⁡\(u\)=\(1\+2​u\)​coth⁡\(u\)/8H\(u\)=\(1\+2u\)\\coth\(u\)/8, differentiation gives

H′​\(u\)=sinh⁡\(2​u\)−2​u−18​sinh2⁡u\.H^\{\\prime\}\(u\)=\\frac\{\\sinh\(2u\)\-2u\-1\}\{8\\sinh^\{2\}u\}\.\(S54\)The denominator is positive foru\>0u\>0, soHHdecreases beforeu∗u\_\{\*\}and increases after it\. At the root,1\+2u∗=2sinhu∗coshu∗1\+2u\_\{\*\}=2\\sinh u\_\{\*\}\\cosh u\_\{\*\}, and substitution yieldsH⁡\(u∗\)=cosh2⁡u∗/4H\(u\_\{\*\}\)=\\cosh^\{2\}u\_\{\*\}/4\. This connects the scalar equation, the variational minimizer, and the leading scaling coefficient\.

#### J\.6\.2Extracting the logarithmic correction from the recurrence

Leta=cosh⁡u∗a=\\cosh u\_\{\*\}andb=sinh2⁡u∗/6b=\\sinh^\{2\}u\_\{\*\}/6\. The registered expansion has the formSk−Sk−2=a\+b/Sk−2\+O⁡\(Sk−2−2\)S\_\{k\}\-S\_\{k\-2\}=a\+b/S\_\{k\-2\}\+O\(S\_\{k\-2\}^\{\-2\}\)\. On either parity class, setxj=S2​j\+ηx\_\{j\}=S\_\{2j\+\\eta\}\. Then

xj\+1−xj=a\+bxj\+O⁡\(xj−2\)\.x\_\{j\+1\}\-x\_\{j\}=a\+\\frac\{b\}\{x\_\{j\}\}\+O\(x\_\{j\}^\{\-2\}\)\.\(S55\)Once the recurrence establishesxj∼a​jx\_\{j\}\\sim aj, the reciprocal term contributes\(b/a\)​log⁡j\(b/a\)\\log jon summation\. The quadratic error is summable\. Controlling the difference between1/xj1/x\_\{j\}and1/\(a​j\)1/\(aj\)refines the result toxj=a​j\+\(b/a\)​log⁡j\+Cη\+o⁡\(1\)x\_\{j\}=aj\+\(b/a\)\\log j\+C\_\{\\eta\}\+o\(1\)under the uniform expansion hypotheses\.

Here is the summation step in detail\. The recurrence first gives constantsc1,c2\>0c\_\{1\},c\_\{2\}\>0withc1​j≤xj≤c2​jc\_\{1\}j\\leq x\_\{j\}\\leq c\_\{2\}jfor all largejj, hencexj=a​j\+O⁡\(log⁡j\)x\_\{j\}=aj\+O\(\\log j\)by summingb/xj\+O⁡\(xj−2\)b/x\_\{j\}\+O\(x\_\{j\}^\{\-2\}\)\. Therefore

1xj=1a​j\+O⁡\(log⁡jj2\)\.\\frac\{1\}\{x\_\{j\}\}=\\frac\{1\}\{aj\}\+O\\\!\\left\(\\frac\{\\log j\}\{j^\{2\}\}\\right\)\.\(S56\)Defineyj=xj−a​j−\(b/a\)​log⁡jy\_\{j\}=x\_\{j\}\-aj\-\(b/a\)\\log j\. Using

log⁡\(j\+1\)−log⁡j=1j\+O⁡\(j−2\),\\log\(j\+1\)\-\\log j=\\frac\{1\}\{j\}\+O\(j^\{\-2\}\),\(S57\)the recurrence givesyj\+1−yj=O⁡\(\(log⁡j\)/j2\)y\_\{j\+1\}\-y\_\{j\}=O\(\(\\log j\)/j^\{2\}\)\. The series of these increments converges absolutely, soyjy\_\{j\}converges to a parity\-dependent constantCηC\_\{\\eta\}\. This proves

xj=a​j\+ba​log⁡j\+Cη\+o⁡\(1\)x\_\{j\}=aj\+\\frac\{b\}\{a\}\\log j\+C\_\{\\eta\}\+o\(1\)\(S58\)from the uniform one\-step expansion, rather than inferring the logarithmic term from numerical fitting\.

Returning tokkgivesSk=\(a/2\)​k\+\(b/a\)​log⁡k\+Ckmod2\+o⁡\(1\)S\_\{k\}=\(a/2\)k\+\(b/a\)\\log k\+C\_\{k\\bmod 2\}\+o\(1\), with the parity\-dependent constants absorbing fixed logarithmic shifts\. Squaring produces the cross termb​k​log⁡kb\\,k\\log k, while the squared logarithm and constant interactions areO⁡\(k\)O\(k\)\. This recovers exactly the coefficientsinh2⁡u∗/6\\sinh^\{2\}u\_\{\*\}/6in the displayed expansion forβ\\beta\.

The derivation clarifies which parts are formal algebra and which parts require asymptotic control\. The critical\-value simplification is a finite identity\. Establishing the Bellman residual expansion uniformly, selecting the appropriate root branch, provingSk→∞S\_\{k\}\\to\\infty, and summing errors are analytic obligations\. They cannot be discharged merely by checking the coefficient identity in Lean\.

#### J\.6\.3Finite optimality, family asymptotics, and global extremality

The Arb calculations address the frozen finite optimization problem through horizon 5,000, using outward rounding so that numerical comparisons are certified as intervals\. The two implementations reduce the chance of a shared dynamic\-programming error\. Their agreement on a finite range does not show that the alternating family is globally optimal at every larger size\.

The asymptotic statement concerns the alternating family itself\. Even a complete proof of that family recurrence and its limit would not establish that no other family has a smaller limiting objective\. The global extremal question requires a comparison principle over all allowed permutations or trees\. The manuscript keeps these three levels distinct: finite certified comparisons, the family’s analytic expansion, and the unresolved all\-family extremality claim\.

The second\-order finite estimates approachingsinh2⁡\(u∗\)/\(6​cosh⁡\(u∗\)\)≈0\.11\\sinh^\{2\}\(u\_\{\*\}\)/\(6\\cosh\(u\_\{\*\}\)\)\\approx 0\.11are consistency checks at theβ\\sqrt\{\\beta\}scale\. The separate coefficientsinh2⁡\(u∗\)/6≈0\.16\\sinh^\{2\}\(u\_\{\*\}\)/6\\approx 0\.16belongs to theβ\\betascale\. Keeping the exact symbolic expressions alongside two\-decimal approximations prevents those two coefficients from being conflated\.

## Appendix KAuxiliary Results: Exact Classifications, Reductions, and Obstructions

The thirteen auxiliary groups in this section comprise twenty\-five scoped results that expand the supporting research inventory\. They are not counted as additional independent 4\+6 headline successes\. They include finite classifications, infinite\-family candidates, verification improvements, source\-table corrections, and negative local obstructions\. The statements are reproduced and organized from the supplied research dossier\. When source\-specific notation is not fully defined in that dossier, the statement retains its source convention and identifies the additional definition needed for standalone specialist assessment\.

### K\.1Exact k\-SSD heights and unique extremizers

For a positive\-integerkk\-SSD setA=\{a1,…,an\}A=\\\{a\_\{1\},\\ldots,a\_\{n\}\\\}, all sums∑ici​ai\\sum\_\{i\}c\_\{i\}a\_\{i\}withci∈\{0,…,k\}c\_\{i\}\\in\\\{0,\\ldots,k\\\}are distinct\. In the supplied convention, the height is the largest generator, andhk​\(n\)h\_\{k\}\(n\)minimizes that height\. A candidate upper bound is easy to certify by enumerating coefficient sums\. An exact minimum requires excluding every smaller admissible generator tuple; uniqueness additionally requires showing that no other tuple attains the minimum\.

Table S12:Dual\-verified four\-generator k\-SSD results\.The two verification routes use signed\-difference frontiers and translate\-disjointness enumeration\. Their agreement covers lower slices and extremizer uniqueness, not merely validity of the displayed sets\. The supplied comparator construction gives heights 121, 211, and 337, respectively\. These are scoped finite improvements, not an all\-kkheight formula\.

The primary search also reportsh4​\(5\)=442h\_\{4\}\(5\)=442with unique extremizer\{344,417,427,433,442\}\\\{344,417,427,433,442\\\}after 37,759,246,033 fifth\-value tests\. Its independent Z3 lower exclusion timed out\. This result must remain primary\-complete rather than dual\-verified\. The timeout does not falsify the candidate; it prevents the stronger independent\-exclusion status\. This entry illustrates why construction, lower\-bound exclusion, and uniqueness need separately recorded receipts\.

### K\.2Four\-element sumsets of diameter six and seven

Leth​AhAdenote the set of sums of exactlyhhelements ofAA, with repetition, and defineR\(h,4\)=\{\|hA\|:A⊂ℤ,\|A\|=4\}R\(h,4\)=\\\{\|hA\|:A\\subset\\mathbb\{Z\},\\ \|A\|=4\\\}\. The retained diameter\-six classification states that forh≥4h\\geq 4,

R⁡\(h,4\)∩\[5​h\+2,7​h−6\]=\{∅,h=4,\{6​h−3,6​h−1\},h=5,6,\{6​h−3,6​h−1,6​h\+1\},h≥7\.R\(h,4\)\\cap\[5h\+2,7h\-6\]=\\begin\{cases\}\\varnothing,&h=4,\\\\ \\\{6h\-3,6h\-1\\\},&h=5,6,\\\\ \\\{6h\-3,6h\-1,6h\+1\\\},&h\\geq 7\.\\end\{cases\}\(S59\)The proof reduces to affine\-normalized diameter six and verifies exact complement identities for five reflection representatives\. Affine normalization removes translation and common scaling, while reflection identifies equivalent endpoint patterns\.

The diameter\-seven region has, forh≥6h\\geq 6,

R⁡\(h,4\)∩\[6​h\+2,8​h−9\]=\{\{7​h−4,7​h−3\},h=6,\{7​h−5,7​h−4,7​h−3,7​h−2\},7≤h≤9,\{7​h−5,7​h−4,7​h−3,7​h−2,7​h\+1\},h≥10\.R\(h,4\)\\cap\[6h\+2,8h\-9\]=\\begin\{cases\}\\\{7h\-4,7h\-3\\\},&h=6,\\\\ \\\{7h\-5,7h\-4,7h\-3,7h\-2\\\},&7\\leq h\\leq 9,\\\\ \\\{7h\-5,7h\-4,7h\-3,7h\-2,7h\+1\\\},&h\\geq 10\.\\end\{cases\}\(S60\)Nine normalized reflection representatives cover this second reduction\. Independent Presburger queries verify the arbitrary\-hhinduction steps\. Finite checks through 200 are controls, not the reason the statements quantify over every largerhh\. The important evidence chain is structural diameter reduction, a finite list of normalized forms, and symbolic induction on each form\. External priority for these exact classification windows remains separate\.

### K\.3Rajagopal finite boundary through h\+k at most thirteen

Using the source conventionR\(h,k\)=\{\|hA\|:A⊂ℤ,\|A\|=k\}R\(h,k\)=\\\{\|hA\|:A\\subset\\mathbb\{Z\},\\ \|A\|=k\\\}, the retained constructive verification covers all registered pairsk\>hk\>hwithh\+k≤13h\+k\\leq 13\. The new boundary is

R⁡\(4,9\)\\displaystyle R\(4,9\)=\[33,495\]∖\{34,35,38\},\\displaystyle=\[33,495\]\\setminus\\\{34,35,38\\\},\(S61\)R⁡\(5,8\)\\displaystyle R\(5,8\)=\[36,792\]∖\{37,38,39,42,43,47\},\\displaystyle=\[36,792\]\\setminus\\\{37,38,39,42,43,47\\\},\(S62\)R⁡\(6,7\)\\displaystyle R\(6,7\)=\[37,924\]∖\{38,39,40,41,44,45,46,50,51,56\}\.\\displaystyle=\[37,924\]\\setminus\\\{38,39,40,41,44,45,46,50,51,56\\\}\.\(S63\)The boundary search emits 460, 751, and 878 witnesses\. Their sum is 2,089; this is the new boundary\-layer count, distinct from the broader inventory’s 2,814 witnesses across its registered range\. An independent program reconstructs the sumsets of all 2,089 boundary witnesses and rejects duplicate\-element corruptions\.

Existence witnesses establish every included value\. Exact interval closure and the source’s exclusion argument are separately needed to establish that omitted values are impossible\. The dossier reports the full finite verification, but the raw witness catalogue and exclusion certificates are not embedded in this manuscript\. The claim is a finite boundary theorem, not a proof of the all\-parameter conjecture\. This entry demonstrates the value of retaining constructive witnesses instead of a table of possible cardinalities alone\.

### K\.4Lonely Runner single\-replacement classifications

For the source’s single\-replacement speed families with deleted speedr=4r=4orr=5r=5, the retained classification finds no sporadic tight cases outside the published multiple\-replacement mechanism\. In ther=5r=5reduction, exactly 46 candidate pairs remain with11≤n≤2011\\leq n\\leq 20\. Their exact Breakpoint\-Lemma evaluations satisfyLR\>1/n\\operatorname\{LR\}\>1/n\.

The smallest retained margin is1/421/42, attained at the source parameters\(n,w\)=\(14,14\)\(n,w\)=\(14,14\)withLR=2/21\\operatorname\{LR\}=2/21; indeed2/21−1/14=1/422/21\-1/14=1/42\. This arithmetic is an internal consistency check on the stated margin\. The source definition of the replacement family and the proof that these 46 pairs exhaust its non\-multiple cases remain part of the theorem’s hypotheses and reduction package\.

Combining the finite residual classification with the established multiple case gives the stated fixed\-r=5r=5result\. The finite computations alone would not imply it without that reduction\. Neither classification resolves the general Lonely Runner conjecture\. The separate unresolved 14\-runner solver direction appears in the negative ledger and must not be confused with this admitted fixed\-replacement family\.

### K\.5Fourier principal nonsingularity for orders 10p and 11p

The source lifting theorem reduces two prime\-parameter Fourier nonsingularity families to exact cyclotomic norm data\. For order11​p11p, the retained exception support is\{3,11,23,67,199,419\}\\\{3,11,23,67,199,419\\\}and the aggregate norm factorization is

3220​1128160​231100​67220​199220​419220\.3^\{220\}11^\{28160\}23^\{1100\}67^\{220\}199^\{220\}419^\{220\}\.\(S64\)Thus the stated principal\-minor nonsingularity conclusion holds for primes outside that support under the source theorem’s admissibility hypotheses; order 187 is included\. For order10​p10p, the support is\{2,3,5,11,31\}\\\{2,3,5,11,31\\\}with exponents\(5120,120,5120,240,80\)\(5120,120,5120,240,80\), and order 130 is included\.

Multiplication\-matrix determinants computed by Bareiss elimination and independent resultants agree over all 2,048 order\-11 subsets and 1,024 order\-10 subsets in the retained enumeration\. Their independent representations help detect normalization or cyclotomic arithmetic errors\. An exceptional prime in the norm support means the sufficient lifting conclusion is unavailable there; it should not automatically be described as a proved singular case\.

### K\.6ERG\(3,8\): cycle spectrum and factor\-criticality

Conditional on completeness and correctness of the frozen 477,142\-record catalogue, every listed triangle\-free 27\-vertex graph with independence number at most seven has cycles of every length from 4 through 27 and is factor\-critical\. Here factor\-criticality means that deleting any vertex leaves a graph with a perfect matching, consisting of 13 edges in this case\.

The primary pass constructs cycles and vertex\-deleted matchings\. The independent pass uses generic cycle enumeration and a skew Tutte matrix over𝔽2147483647\\mathbb\{F\}\_\{2147483647\}\. Rank 26 with a full\-support kernel gives the required nonvanishing principal cofactors in the odd\-order skew setting, which certifies the vertex\-deleted matching condition under the checker theorem\. The finite\-field certificate is a witness of nonvanishing, not an inference from a failed search for a matching\.

### K\.7Kasami APN counting identity at n equal to fourteen

For admissiblekkwithgcd⁡\(k,14\)=1\\gcd\(k,14\)=1, the retained finite result verifies the source NSUCRYPTO counting identity for the Kasami powerF⁡\(x\)=x4k−2k\+1F\(x\)=x^\{4^\{k\}\-2^\{k\}\+1\}overGF⁡\(214\)\\mathrm\{GF\}\(2^\{14\}\)\. Frobenius symmetry reduces the new representative computations tok=3k=3andk=5k=5\.

Two different irreducible\-polynomial field models check 16,382 admissibleρ\\rhovalues per representative, giving 32,764 exact identitiesZ⁡\(ρ\)=0Z\(\\rho\)=0in the source notation\. Both derivative images have 8,192 elements with two\-point fibers, and the reported Walsh support has size 3,088\.

The formula definingZZand the symmetry reduction are part of the source problem and must be included with a standalone certificate release\. The present evidence extends a finite verified boundary fromn≤13n\\leq 13ton=14n=14\. It does not establish an arbitrary\-nncounting theorem or a new general APN construction\. The work illustrates exact finite algebra at a new parameter boundary with representation\-independent checks\.

### K\.8ReLU MAX8 certificate compression and subset\-profile dynamic programming

Starting from the public four\-template MAX6 certificate, the local attachment search contains 676 raw candidates, 127 graph\-isomorphism classes, and 125 exact function columns\. The retained combination yields a 25\-template degree\-three MAX8 identity\. The source’s public 69\-template certificate expands to 515,488 symmetric second\-layer atoms, whereas the retained certificate uses 187,460: a reported 63\.63% reduction and 2\.75\-fold compression\.

Full8\!8\!permutation enumeration and subset\-profile dynamic programming agree term by term\. The dynamic program aggregates permutations according to profiles sufficient for the certificate evaluation, so its correctness requires proving that aggregated transitions preserve every evaluated contribution\. Agreement on a complete finite instance checks that reduction against brute\-force enumeration\.

The same generic verifier checks public MAXNcertificates for5≤N≤105\\leq N\\leq 10, reducing the largest replay from approximately 1\.46 billion permutations to 71\.77 million transitions\. This is a verification\-efficiency result as well as a compressed certificate\.

### K\.9AES CNOT Pareto cleanup

A separate local rewrite begins with the source 20\-qubit AES circuit containing 44 Toffoli gates and 197 CNOT gates\. Two identical CNOT pairs can commute through intervening gates and cancel, giving 193 CNOT gates while preserving all 44 Toffolis\. The two retained commutation windows span 22 and 23 gates, and the independent verifier checks all 47 intervening commutations recorded by the certificate\.

All 256 input cases pass the independent truth\-table check\. This validates the finite circuit transformation under the registered input and ancilla contract\. It is a modest Pareto improvement: one gate type decreases while the dominant Toffoli count stays fixed\. It is distinct from the Hyperfactor cross\-output construction and should not be added to its T\-count savings as though both changes were applied to the same baseline\.

Separate exhaustive single\-delete and 10,920 two\-delete/one\-insert affine charts do not reduce the eight\-Toffoli count of the four\-bit inverse\. Those search negatives prove only absence within the explored rewrite neighborhoods\. They are not a global Toffoli lower bound\.

### K\.10Factorwise tail elimination for transferred tensors

For st333, EPOCH identified a retained optimizer in which one derivative mode vanishes in each of ten rank\-one terms, eliminating the cubic derivative product\. An exhaustive search over all310=59,0493^\{10\}=59\{,\}049mode patterns found 1,536 admissible realizations; the selected path has coefficient weights\(0,18,8,0\)\(0,18,8,0\)and gives

R⁡\(T⊗N\)≤\(N\+1\)​10N\.R\(T^\{\\otimes N\}\)\\leq\(N\+1\)10^\{N\}\.\(S65\)Under the supplied scalar\-count model, this lowers the crossover with exact rank\-11 recursion fromN=48N=48toN=39N=39, and the crossover with explicit base\-field recursion fromN=90N=90toN=81N=81\.

The same mechanism transfers to ss333 and to the 35\-term st555 construction\. For st555, the coefficient weights become\(0,75,922,0\)\(0,75,922,0\), improving the two reported crossover thresholds from\(41,78\)\(41,78\)to\(33,70\)\(33,70\)\. This session shows how EPOCH can convert a structural observation about a border construction into a measurable reduction in exactification overhead\.

### K\.11Degree\-eight Smale reductions

EPOCH reduced the nearest\-critical\-point problem to a one\-variable polynomial problem on the unit disk using the Grace–Walsh–Szegő theorem\. Exact Schur and Sturm certificates then establish

\|P⁡\(b\)b\|\>4335000≈0\.09,\\left\|\\frac\{P\(b\)\}\{b\}\\right\|\>\\frac\{433\}\{5000\}\\approx 0\.09,\(S66\)which improves the corresponding general\-degree estimate at degree eight by a factor of approximately4\.314\.31under the same normalization\.

The analysis also isolates the multiple\-critical\-point case and proves the sharp bound

\|P⁡\(b\)b\|≥18,\\left\|\\frac\{P\(b\)\}\{b\}\\right\|\\geq\\frac\{1\}\{8\},\(S67\)with equality attained by\[1−\(1−z\)8\]/8\[1\-\(1\-z\)^\{8\}\]/8\. The session combines a classical reduction with exact region certification, yielding both a stronger numerical bound and a sharper structural description of any remaining counterexample\.

### K\.12A cofinite unfair\-trinomial family

EPOCH turned a finite recurrence pattern into a parameter\-uniform obstruction\. For every integerk≥3,000,001k\\geq 3\{,\}000\{,\}001withgcd⁡\(k,3\)=1\\gcd\(k,3\)=1and every0<a<10<a<1, no nonzero polynomial with nonnegative coefficients can multiply

1\+a​x3\+xk1\+ax^\{3\}\+x^\{k\}\(S68\)into a polynomial whose coefficients all belong to\{0,1\}\\\{0,1\\\}\.

The proof organizes the recurrence into three residue classes and controls the resulting negative\-binomial packets through projective contraction, seam estimates, an antiperiodic theta kernel, and a terminal recurrence\. Exact symbolic and rational replays verify the algebraic identities used throughout\. This case illustrates EPOCH’s capacity to recognize a computational pattern, identify the mechanism behind it, and promote it to an explicit theorem for an infinite family\.

### K\.13Sharp stability and an exact loopless mixing curve

For the loopless three\-state reversible baseW0W\_\{0\}, letWt=\(1−t\)\+t​W0W\_\{t\}=\(1\-t\)\+tW\_\{0\}for0≤t≤10\\leq t\\leq 1, and letH=K5,5−C10H=K\_\{5,5\}\-C\_\{10\}\. EPOCH obtained the exact inequality

t⁡\(H,Wt\)≥c⁡\(t\)​t​\(C4,Wt\)5,c⁡\(t\)=2​h​\(t\)\(8\+t4\)5,t\(H,W\_\{t\}\)\\geq c\(t\)\\,t\(C\_\{4\},W\_\{t\}\)^\{5\},\\qquad c\(t\)=\\frac\{2h\(t\)\}\{\(8\+t^\{4\}\)^\{5\}\},\(S69\)where

h⁡\(t\)=\\displaystyle h\(t\)=\{\}16384\+10240​t4\+7680​t6−1280​t7\+5760​t8−3200​t9\\displaystyle 16384\+10240t^\{4\}\+7680t^\{6\}\-1280t^\{7\}\+5760t^\{8\}\-3200t^\{9\}\+2656​t10−1440​t11\+440​t12−60​t13−t15\.\\displaystyle\+2656t^\{10\}\-1440t^\{11\}\+440t^\{12\}\-60t^\{13\}\-t^\{15\}\.\(S70\)The ratio increases from11to34/2734/27, with equality fort\>0t\>0precisely at the uniform triangle, up to the stated scaling and relabelling convention\.

Global monotonicity is certified by 6,615 positive ordered Bernstein controls, 13,140 positive ratio controls, and a reduced derivative certificate with 14 positive controls\. A complementary sharp\-stability argument is represented by 31,765 rational nonnegative blocks\. This session demonstrates EPOCH’s ability to organize a large exact certificate into a transparent quantitative theorem with a sharp equality case\.

Across these sessions, the advantage of EPOCH is not the volume of computations performed, but the conversion of search output into reusable mathematical structure: optimized constructions, exact inequalities, uniform parameter arguments, and independently replayable certificates\.