PaperlayerView exact revision on arXiv

Source-linked AI summary

EULER: Exploring Underused Links with Evidence-Checked Return for Multi-Agent Mathematical Discovery

Ren Zhenzhuo

arXiv:2609.00032v1cs.AIcs.MA

TL;DR

Mathematical communities use different objects, invariants, and tools, making problem transfer costly to construct and check. EULER searches direct and cross-domain routes while requiring bridges to add executable operations and return checked evidence to the source. Across 120 recent conjectures, it reports proofs and refutations, with safety and operation-set effects alongside an uncertain overall resolution difference.

  • Problem

    Cross-community problem transfer is costly because researchers must map objects, check imported assumptions, and return conclusions to the source statement.

    Source: §1 · p. 1

  • Method

    EULER coordinates competing direct, adjacent-domain, and distant-domain routes, retaining bridges that add executable operations and return evidence through checked implications.

    Source: §1 · p. 2

  • Results

    Across 120 recent open problems, EULER produced 10 proofs, 3 counterexamples, 27 conditional results, and 18 local theorems; the 4.2-percentage-point paired resolution difference had an interval including zero.

    Source: §1 · pp. 2–3, §8 · pp. 26–27

  • Takeaways & Limitations

    Domain distance did not determine route success; useful bridges supplied unavailable operations, passed structural tests, and returned complete evidence to the source.

    Source: §8 · p. 26

    The contamination screen cannot rule out related material in proprietary training data, and novelty claims for natural-language proofs require active literature review.

    Source: §7 · p. 26

Abstract

from arXiv · show

Mathematical communities work with different objects, invariants, and tools, so transferring a problem across them is expensive and often skipped. We present EULER, a multi-agent system that takes such a transfer--a bridge--as its unit of search. Around a fixed conjecture, EULER runs direct, adjacent-domain, and distant-domain routes in competition; a bridge keeps its budget only if it supplies an operation the source representation cannot execute and its target-side evidence returns to the original statement along a checked implication. Six ordered stress tests reject invalid bridges before expensive search begins. We evaluate EULER on 120 recent conjectures. The conjectures were frozen before search and screened for contamination, and are drawn from public papers by authors who had recently published in the Journal of Combinatorial Theory, Series A, a leading journal in combinatorics. EULER produced 10 proofs and 3 refutations, plus 45 scoped partial results. Two mechanisms held up under ablation: bridge-specific stress tests cut incorrect conclusions from 9 to 3, and bridge material combined with a target-native operation yielded a positive interaction of +4.2 resolved tasks that neither factor produced alone. Domain distance did not reliably predict success; executable operation gain and valid return did.

1 Introduction

EULER treats cross-community transfer as a costly but potentially useful search route, requiring a new executable operation and checked return to the source problem. Its evaluation finds safety and operation-set effects, while the overall resolution difference remains uncertain.

1 Introduction

  • Cross-community transfer is costly because researchers must learn another language, map objects, check imported assumptions, and return conclusions to the original problem.Here, “underused” means an equivalent target-native operation is absent from frozen direct and adjacent-domain inventories before search, not that the connection is absent from the literature.Source: §1 · p. 1
  • The Zhao-conjecture search refuted the conjecture with a concrete counterexample found by corrected exhaustive encoding and checked against the original statement.An initial encoding failed a round-trip test after merging equal-valued occurrences.Source: §1 · p. 2
  • A target representation matters only if its tool changes the available operations; target-side success alone does not establish the original problem.The target objects, ranges, and predicates must match the source statement, and evidence must return in the correct logical direction.Source: §1 · p. 2
  • Recent, timestamped conjectures were prioritized because prior exposure to famous problems could confound new search with recall or recombination.The authors screened tasks and routes for answer cues before execution.Source: §1 · p. 2
  • EULER makes direct, adjacent-domain, and distant-domain routes compete, continuing a bridge only when it adds an executable operation and target evidence returns to the source.Six bridge-specific stress tests check candidate routes before expensive search.Source: §1 · pp. 1–2
  • 4.2 percentage points was the paired difference between the full system and distant-domain retrieval, with an interval including zero; stress tests cut incorrect returns from 9 to 3.The operation-set experiment found an interaction of 4.2 resolved tasks, or 3.5 percentage points.Source: §1 · pp. 2–3

2 System overview

EULER coordinates route selection, open-ended mathematical work, verification, and persistent state around a fixed source problem. A run records artifacts and checks, but only source-side coverage can change the root conclusion.

2 System overview

  • EULER takes a fixed source problem and returns a route lineage, mathematical outcome, and itemized cost through four interacting system layers.Figure 2 depicts their interaction across one research cycle.Source: §2 · p. 3

2.1 Four layers

  • The control layer allocates budgets across route types using recorded stress-test results and independently checkable evidence.Table 1 presents role inputs, required outputs, and state authority.Source: §2.1 · p. 3, Table 1 · p. 4
  • Execution agents generate approaches, retrieve mechanisms, use tools, and develop Lean proofs; verification independently checks artifacts and source-side return.A route proposer cannot certify its own output.Source: §2.1 · p. 4
  • The mathematical-state layer separates task progress from claims, storing actions and failures in one graph and exact statements, evidence, dependencies, and versions in another.Completing target search need not create a claim usable by later reasoning, and a true local claim need not resolve the root problem.Source: §2.1 · p. 4

2.2 System components and related work

  • EULER distinguishes itself from related systems by making a bridge between communities its search unit and evaluating both target operations and evidence returned to the source.The paper also relates its design to representation-search and translation-validation work.Source: §2.2 · p. 5

2.3 Data flow of one run

  • A run fixes admissible evidence, boundary objects, budget, and stopping rules, then verifies artifacts before source-side review assigns an outcome.Passing a target checker or completing a verification record alone does not establish the original conjecture; only source-side coverage can change the root conclusion.Source: §2.3 · p. 5

3 Method: bridge search and stress testing

EULER treats a bridge as a route from a fixed source problem to a target representation, requiring both a new operation and a checked return of target evidence. Routes compete for budget through staged tests, refinement, and cross-route reuse.

3.1 Problem setting

  • A valid source return carries target evidence along the registered implication direction, accounting for added assumptions and omitted cases to support a proof, refutation, or scoped local result.Proofs and counterexamples can require different implication directions; a one-way map cannot be reinterpreted as an equivalence after a result is found.Source: §3.1 · p. 6

3.2 Three route families

  • Direct, adjacent-domain, and distant-domain routes run in parallel, with route quotas preventing either safe nearby routes or domain distance from dominating allocation.Adjacent bridges must state their gain over direct search; distant bridges can be randomly sampled or retrieved by structural fingerprints.Source: §3.2 · pp. 6–7

3.3 Bridge opportunities and ranking

  • A BridgeOpportunity records a target mechanism, expected operation, likely gains and losses, an early rejection test, a return outline, and rough cost before a complete map is built.Unknown gains score zero and unknown losses receive the highest risk score; every score must be tied to a concrete object or test.Source: §3.3 · p. 7

3.4 Six stress tests

  • Figure 3 orders six stress tests by cost, moving from direction, assumption, and boundary checks to tests of target-tool gain and valid return.An inconclusive boundary or round-trip check permits one bounded refinement; an inconclusive tool test triggers a small paired probe, while an inconclusive return cannot support source resolution.Source: Figure 3 · p. 8, §3.4 · p. 8

3.5 Early rejection tests and reusable negative results

  • Early rejection seeks the cheapest decisive witness, and failed-route records preserve the specific map, scope, witness, and reopening conditions rather than condemning a whole method or domain.A route can reopen after a proof-critical map or object-scope change, but not merely after changing the model or wording.Source: §3.5 · p. 9

3.6 Refinement, return, and verified resolution

  • Surviving routes advance through three budget stages only by adding checkable objects, and pause after two consecutive stages without one.A return template is frozen before target search; partial coverage is recorded as a local theorem, while verified resolution requires the source domain to be covered.Source: §3.6 · p. 9

3.7 Budget reallocation and cross-route transfer

  • Budget favors routes that survive testing, add checkable objects, and promise source-side impact; material can transfer across routes without counting shared-lemma branches as independent discoveries.Failed routes retain a scoped witness and reopen only if the map, target mechanism, or return relation changes.Source: §3.7 · pp. 9–10, Figure 4 · p. 10

4 State and verification

EULER separates execution tasks from mathematical claims and tracks distinct kinds of evidence rather than using a single verified flag. Centralized admission, independent replay, and dependency-aware recovery preserve the scope and provenance of conclusions.

4 State and verification

  • The task graph supports reproducible, reversible, recoverable work, while these state mechanisms do not enter the bridge utility score.The task graph tracks execution order and resource dependencies; the claim graph stores mathematical content and evidence coverage.Source: §4 · p. 10, Figure 5 · p. 11

4.1 Task and claim graphs

  • The task graph records what to do next, while the claim graph records what is known; task completion alone does not establish a mathematical conclusion.Candidates, artifacts, and verification records connect the graphs, and the source claim changes only after the return chain is complete.Source: §4.1 · p. 10, Figure 5 · p. 11

4.2 Multiple evidence axes

  • Four evidence axes separately track machine checks, semantic correspondence, independent review, and whether local claims compose; mathematical quality and novelty remain separate from truth status.This preserves distinctions such as a kernel-accepted Lean file whose formalized statement has narrower scope than its source claim.Source: §4.2 · p. 11

4.3 Composition obligations

  • Composition closes only when child claims cover the parent’s parameter range and meet interface, invariant, well-foundedness, joint-choice, and boundary obligations.A coverage table links each parameter region to its child claim, assumptions, verification record, and unresolved interfaces.Source: §4.3 · pp. 11–12

4.4 Separation of roles and centralized state updates

  • Execution agents propose claims, but a centralized updater admits them only after claim-type-specific checks of version, scope, evidence, semantic correspondence, and composition.Verification records report checker-specific results; a well-formed record without controlled provenance cannot alone change the root claim.Source: §4.4 · p. 12

4.5 Independent replay and semantic review

  • Independent replay recompiles Lean projects or runs deterministic checkers, while reviewers separately assess statement faithfulness, local correctness, and how proof pieces compose.Replay includes an axiom audit, and two primary reviewers assign task-level outcomes with a third resolving disagreements.Source: §4.5 · p. 13

4.6 Negative results, invalidation, and recovery

  • When evidence changes, EULER withdraws affected source conclusions while preserving valid target artifacts, then records repairs and reconstructs state from a frozen checkpoint.Unrelated parallel routes remain valid when a return map or target theorem changes.Source: §4.6 · p. 13

5 Dataset and mathematical outcomes

The evaluation uses a frozen, screened set of 120 conjectures and reports proofs, refutations, partial outcomes, and unresolved tasks. Its traces include a counterexample, an all-dimensional local theorem, and a candidate theorem with an open obligation.

5.1 Dataset construction

  • The 120-task cohort was drawn from recent JCTA-author papers, screened for eligibility and contamination, and is not representative of all combinatorics or mathematics.Tasks were frozen before search; 18 contaminated root tasks were replaced and five contaminated routes were blocked.Source: §5.1 · pp. 13–14

5.2 Aggregate outcomes

  • The 13 verified resolutions comprised 3 kernel-checked proof-critical chains, 3 independently reproduced programs or certificates, and 7 results checked by two mathematicians.Across five reasoning seeds, the full system resolved 12, 12, 13, 13, and 14 tasks, with a mean of 12.8 and standard deviation of 0.84.Source: §5.2 · pp. 14–15
  • Of 120 tasks, EULER produced 10 proofs, 3 refutations, 27 conditional results, 18 local theorems, 59 unresolved tasks, and 3 incorrect conclusions.The incorrect conclusions were rejected by blinded source-side review and were not admitted as verified claims.Source: §5.2 · p. 14, Table 6 · p. 15

5.3 Outcomes by structural stratum

  • Executable-refutation resolved 5 tasks, including all 3 counterexamples; structural-transfer resolved 4, while its two errors involved over-broad returns and sparse-bridge’s error reversed a map.Language-and-formalization resolved 2 tasks with no incorrect root conclusion, while 18 remained open; the errors arose after target evidence but before source-side coverage was complete.Source: §5.3 · pp. 15–16

5.4.1 Zhao: a distant-domain computational bridge to a counterexample

  • In the Zhao trace, exhaustive enumeration produced a source-readable counterexample to the conjecture, checked by recomputing group sums, lengths, and indexed subsets.The occurrence-preserving encoding was essential because merging equal-valued positions failed the round-trip test.Source: §5.4.1 · pp. 16–17

5.4.2 AJT(5): an adjacent-domain structural bridge to an all-dimensional local theorem

  • The AJT(5) bridge proves the claim for invertible matrices with row supports of size at most two in arbitrary dimension, while the dense-row regime and original conjecture remain open.The scope test prevented promoting the sparse-row result to the full conjecture.Source: §5.4.2 · p. 17

5.4.3 Gao: composition of several bridges with partial Lean verification

  • The Gao trace remains a candidate theorem with partial Lean verification because its top-level result still depends on a proof of the remaining upper bound.Several bridges cover distinct parameter ranges, and composition checks whether those ranges meet without gaps.Source: §5.4.3 · p. 18

6 Evaluation and ablations

Across 120 fixed source tasks, the experiments test bridge routes, return safety, executable operations, and resource allocation. Bridge-specific tests and the operation-set interaction met their decision thresholds, while the overall resolution and cost thresholds did not.

6.2.1 Route pools: do adjacent-domain and distant-domain bridges complement each other?

  • Full-system and distant-domain retrieval each resolved seven tasks; their paired difference was 4.2 percentage points (95% interval [−0.1, 8.4]), leaving the overall difference uncertain.The primary comparison combines adjacent routes, bridge-specific tests, and feedback-based budget reallocation.Source: §6.2.1 · p. 19, Table 9 · p. 19

6.2.2 Stress-test strength and order: filtering or abstention?

  • Bridge-specific tests reduced incorrect conclusions from nine to three; early testing produced 13 resolutions versus 11 late, at $568 versus $621 median per-task cost.Late testing spent target-search resources on bridges with wrong directions or incompatible assumptions.Source: §6.2.2 · pp. 20–21

6.2.3 Bridge material and target-native operations: does the executable operation set change?

  • The target-native operation added 0.6 resolutions without bridge material and 4.8 with it; their interaction was 4.2 resolved tasks, or 3.5 percentage points.The interaction exceeded the prespecified 3-percentage-point threshold.Source: §6.2.3 · p. 21, Table 12 · p. 21

6.2.4 Selector: can useful bridges be identified early?

  • Gain-loss ranking beat semantic and cost rules and stronger related baselines but remained 4.4 tasks below the post-hoc upper bound; 72 unresolved tasks had no useful bridge in the pool.Other unresolved tasks reflected low ranking, stress-test withholding, or unfinished target search.Source: §6.2.4 · p. 22, Table 13 · p. 22

6.2.5 Budget reallocation: is feedback better than a one-shot allocation?

  • Round-by-round reallocation produced two more resolutions than one-shot allocation and cut rejected-bridge budget by seven percentage points.Released budget moved to nine surviving distant-domain bridges with target-operation gain; adjacent routes adding no operation received no further allocation.Source: §6.2.5 · p. 22, Table 14 · p. 22

6.3.1 Model diversity and cross-model handoffs

  • At matched total budget, mean resolutions were 9.6 for a single agent, 11.1 for homogeneous multi-agent execution, and 12.8 for heterogeneous execution.Ten of 13 verified resolutions involved at least one cross-model handoff.Source: §6.3.1 · p. 23, Table 15 · p. 23

6.3.2 Persistent state

  • Across recoveries, persistent task-and-claim graphs reduced repeated target runs from 29 to 4, stale returns from 7 to 0, and recovery time from 93 to 34 minutes.The state improvement affected recovery across days, not candidate quality within a single run.Source: §6.3.2 · p. 23

6.6 Implications for system design

  • Bridge-specific tests met the incorrect-return threshold and the operation-set interaction cleared its threshold, but paired resolution and cost thresholds were not met.The full-system resolution interval crossed zero, and median-normalized cost did not meet the noninferiority threshold.Source: §6.5 · p. 24, §6.6 · p. 25

7 Limitations

EULER’s evaluation is bounded by the task sample, retrieval catalog, and review process. Its cost estimates also depend on expert-work assumptions, and the upper cost interval exceeds the stated noninferiority margin.

7 Limitations

  • The 120-task results apply most directly to recent open problems with a strong combinatorial component, not all active mathematicians.The author frame introduces editorial, language, access, and subfield selection effects; other areas need their own author frames, task strata, and stress-test templates.Source: §7 · pp. 25–26
  • The bridge-distance rubric reflects this dataset’s route geometry and requires recalibration for new mathematical areas.Annotators disagreed most when a standard equivalence also introduced a new tool.Source: §7 · p. 26
  • Bridge retrieval favors communities with accessible literature and tool catalogs, while mechanisms outside the catalog need an expert proposal to enter the candidate pool.Communities with mature English-language resources and established verification procedures are easier to retrieve; rare but useful connections may rank lower.Source: §7 · p. 26
  • The contamination screen cannot establish that proprietary training corpora contain no related statement, proof sketch, or discussion.Detected cues were removed, but undetected paraphrases or implicit memorization may remain.Source: §7 · p. 26
  • Later specialist scrutiny may revise long-proof lemmas, equivalences, or parameter boundaries, although artifacts and dependency graphs localize affected conclusions.Two reviewers and a third adjudicator produced a consistent outcome for this evaluation.Source: §7 · p. 26
  • Deployment remains more complex than for a single mathematical agent because the implementation spans services and formalization environments, some requiring manual integration.Cross-machine recovery and formal replay are included in measured costs.Source: §7 · p. 26
  • The upper cost confidence bound exceeds the noninferiority margin, making EULER best suited to long-running problems where false conclusions are costly and checked bridges can be reused.Combined cost also depends on the hourly price assigned to expert work and how review tasks are divided.Source: §7 · p. 26

8 Conclusion

Across 120 recent open problems, EULER produced proofs, counterexamples, and scoped partial results, while domain distance alone did not determine route success. The conclusion emphasizes new executable operations, stress-tested bridges, and evidence returned to the source statement; the appendices specify how routes, failures, and records are managed.

8 Conclusion

  • EULER produced 10 proofs, 3 counterexamples, 27 conditional results, and 18 local theorems across 120 recent open problems; domain distance did not determine route success.The full-system versus distant-domain retrieval difference was 4.2 percentage points, with an interval that included zero; stress tests reduced incorrect source-side conclusions from 9 to 3, and the operation-set experiment found an interaction of 4.2 resolved tasks (3.5 percentage points).Source: §8 · pp. 26–27

A Fields fixed before search

  • The task contract fixes the source statement and the statistical unit, so multiple bridges and attempts for one problem remain in the same task cluster.Bridge-level funnels describe mechanisms, while task-level outcomes determine the primary endpoint.Source: A Fields fixed before search · p. 30

B Bridge objects and route lineage

  • A BridgeOpportunity is a structured record of source and target objects, mapping, target mechanism, expected operation, return obligations, tests, and budget.Route lineage distinguishes substantive changes to the map, target mechanism, or proof-critical source-return relation from mere rewording.Source: B Bridge objects and route lineage · pp. 30–31

C Route generation and the retrieval index

  • Routes begin from a structural fingerprint, and distant-domain retrieval prioritizes transformations, encodings, or verification procedures that change executable operations.Candidates are grouped by bridge-family structure, while different source-return directions remain separate routes for independent testing.Source: C Route generation and the retrieval… · p. 31

D Failure records and stopping rules

  • A route’s failure ledger stores scoped, checkable witnesses and reopening conditions, while stopped-route budgets return to the same source task.A route stops after two consecutive stages without new independently checkable evidence; infrastructure failures are not recorded as mathematical counterexamples.Source: D Failure records and stopping rules · p. 32

E Reproducibility bundle specification

The reproducibility bundle organizes evidence and review records by source task and run, linking aggregate results to per-task artifacts. The accompanying annotation and stress-test specifications describe how bridge distance is scored and how checks record their outcomes.

E Reproducibility bundle specification

  • Each task’s reproducibility bundle contains the fixed statement and metadata, while each run stores route lineage, stress tests, artifacts, verification, decisions, costs, and event logs.A manifest maps aggregate table cells to per-task records, and the bundle supports reconstructing endpoints, costs, and the final claim graph.Source: E Reproducibility bundle specification · pp. 32–33, Table 21 · p. 33

F Bridge-distance annotation

  • Two annotators score five bridge-distance dimensions; totals of 0–4 are adjacent, 6–10 distant, and score 5 is a gray zone excluded from the primary binary comparison.Gray-zone routes remain in the full route pool and continuous trend analysis.Source: F Bridge-distance annotation · p. 33, Table 22 · p. 33

G Stress-test record template

  • A stress-test record captures the bridge version, test, input, preservation relation, method, PASS/FAIL/UNKNOWN result, witness, scope, cost, and reopening conditions.A PASS records covered scope, a FAIL includes an object or derivation, and an UNKNOWN identifies the smallest next task; the same template covers natural-language-to-Lean bridges.Source: G Stress-test record template · pp. 34–35, Table 24 · p. 34

H Capability matrix for experimental conditions

The experimental conditions use matched per-task limits, and the dataset protocol draws recent conjectures from a defined JCTA author frame. Eligibility screening and stratified sampling establish the task set before model attempts are considered.

H Capability matrix for experimental conditions

  • The six experimental conditions share per-task limits on tokens, tool slots, target documents, cost, and expert minutes, with released budget movable only within the same task.Distant-domain random selection and retrieval use the same target-mechanism catalog and minimum eligibility screen.Source: H Capability matrix for experimental… · p. 35, Table 25 · p. 35

I Dataset construction protocol

  • The author frame is the closed 24-month window ending at the frozen harvest cutoff and uses JCTA, whose scope spans finite and discrete structures.The frame targets active researchers at a recognized specialist level, not all of combinatorics.Source: I Dataset construction protocol · pp. 35–36
  • The protocol extracts and deduplicates explicit problems, screens eligibility before model attempts, and samples 30 tasks from each of four structural strata.Candidates can be excluded for unrecoverable definitions, prior solutions, non-decidable research directions, licensing restrictions, or no eligible direct route; execution failures remain in the eligible denominator.Source: I Dataset construction protocol · p. 36

I.1 Contamination audit and replacement rule

The audit distinguishes alerts from substantive contamination, and the verification procedures preserve evidence and scope through refutation, Lean, and deterministic-program checks.

I.1 Contamination audit and replacement rule

  • Only material containing a proof idea, counterexample, answer-bearing theorem, or query cue that could materially shorten a route triggers blocking or replacement.Overlap alerts are reviewed by two curators blind to system outcomes; decisions are frozen before execution.Source: §I.1 · p. 36, Table 27 · p. 36

I.2 Refutations and author communication

  • Counterexamples to living authors’ statements require a checked witness, independent recomputation, and source-side review of version, quantifiers, scope, and conclusion.If statement scope remains ambiguous, the outcome stays conditional or local; author communication resolves scope and wording.Source: §I.2 · p. 37

J.1 Three-stage Lean procedure

  • Lean verification separates premise retrieval, candidate generation, and independent replay, with separate permissions and recorded environments and results.Environment failures are distinguished from mathematical feedback, and mathematical revisions create new candidate versions.Source: §J.1 · p. 37, Table 28 · p. 37

J.2 Certificates from deterministic programs

  • Deterministic-program claims retain reproducible inputs and outputs, and their computational scope must match the statement’s scope.Repeated runs establish repeatability, not independence; a second implementation, deterministic check, manual check, or formalization can provide an independent path.Source: §J.2 · pp. 37–38

K Persistent-state experiment

The persistent-state experiment compares recovery across three state configurations after restarts and two version changes.

K Persistent-state experiment

  • In a state experiment after three recoveries and two version changes, execution restarted at the first recovery, a bridge assumption changed before the second, and a target theorem was upgraded before the third; outputs were compared with a preregistered dependency table.Source: Table 29 · p. 38, K Persistent-state experiment · p. 38

L.1 Zhao counterexample certificate

A constructed sequence yields a source-side contradiction to Zhao’s conjecture by showing that every nonempty zero-sum subsequence has length 10, despite the sequence having length 12.

L.1 Zhao counterexample certificate

  • The group G has rank four, exponent 4, and Davenport constants D(G) = D∗(G) = 11, satisfying the stated hypotheses of Zhao’s Conjecture 6.1 [Zhao, 2025].The cited conditions include D(G) − 2 = 9 ≥ 4 and 4 < (D(G) − 1)/2 = 5.Source: §L.1 · p. 38
  • A homomorphism to G has kernel {(0, 0, 0, 0), (2, 2, 2, 2)}, restricting zero-sum selections to the empty selection or the latter coefficient vector.The construction uses the stated coordinate map and a length-12 sequence built from three repeated blocks and three additional terms.Source: §L.1 · pp. 38–39
  • Every nonempty zero-sum subsequence has length 10, so the length-12 sequence has none of length at most 9; an exhaustive 4095-subset computation independently checks the classification.The selected length is i+j+k+Q = 10, with nine indexed zero-sum subsequences.Source: §L.1 · p. 39

L.2 AJT(5) sparse-row theorem

The sparse-row theorem establishes a lower bound for AJT(5) instances with at most two nonzero entries per row, while dense rows remain outside its scope.

L.2 AJT(5) sparse-row theorem

  • For invertible B with row support at most two, the theorem establishes a lower bound for every affine offset and dimension; dense rows remain outside its scope.AJT(5) is the special case B = A and b = 0.Source: §L.2 · p. 39
  • The row-support multigraph decomposes into unicyclic components, and cycle-component counts combine because distinct blocks use disjoint variables.Loops and parallel-edge 2-cycles are allowed; the proof bounds cycle counts and multiplies counts across blocks.Source: §L.2 · p. 39

M Model identities and matched costs

  • Matched-cost conditions equalize per-task limits, while heterogeneous models may pass verification records between models; handoffs require different models in specified bridge roles.Replacing a model alone does not change bridge identity.Source: M Model identities and matched costs · p. 40

N Cost accounting

  • One-time development required 552 person-hours, and the cost analysis retains failed runs, unresolved tasks, and incorrect conclusions in the per-task distribution.The reuse analysis changes only new-task construction minutes and does not retroactively amortize development time.Source: N Cost accounting · p. 40

O Reproduction protocol

  • The run-identified reproducibility bundle supports rebuilding tables, figures, the failure ledger, and cost analysis from per-task records, with software metadata and original failure codes retained.The protocol replays verification artifacts and obtains blinded source-side decisions before rebuilding analyses.Source: O Reproduction protocol · pp. 40–41

P Full Gao candidate-proof manuscript

The manuscript presents a candidate proof of the Gao constant formula for generalized dihedral groups with a nontrivial finite abelian kernel of odd prime-power order, using reflection-containing and rotation-only quotient cases combined by simultaneous induction to obtain matching bounds, E(G) = 2Q + DA. Independent review and the top-level Lean obligation remain pending.

P Full Gao candidate-proof manuscript

  • The manuscript is a complete natural-language candidate proof, but independent line-by-line review, source-derived theorem-instance verification, and the top-level Lean obligation remain pending.Its claims do not change the source-side outcome reported in the paper.Source: P Full Gao candidate-proof manuscript · p. 42

5 Subgroup descent in the intermediate range

  • The proof splits by reflection count: prescribed-length zero-sum results handle the extremes, while a weighted structural alternative and induction handle the intermediate range.The subgroup descent proves two statements simultaneously; its auxiliary all-rotation conclusion is needed when rotation vectors are translated.Source: P Full Gao candidate-proof manuscript · p. 43, §5 · p. 50

1 Introduction

2.1 Realizing prescribed signs

  • Prescribed signs on an even positive number of reflections can be realized by ordering the terms, so a zero signed vector sum yields a product-one sequence.Rotation signs may be chosen arbitrarily, with exactly half of the reflections assigned each sign.Source: §2.1 · p. 45

2.3 The lower bound and identity padding

  • E(G) ≥ 2Q + D(A) follows by padding a product-one-free sequence with identity rotations.The manuscript also gives an identity-padding lemma for sequences of length 2Q + D(A) containing at least D(A) identity rotations.Source: §2.3 · p. 46

3 A plus-minus Davenport bound

  • Every sequence of length (D(B) + 1)/2 over a nontrivial finite abelian p-group B, for odd p, has a nonempty plus-minus zero-sum subsequence.The manuscript proves this bound using the group algebra over Fp.Source: §3 · p. 47

4 Reduction by the number of reflections

  • For at most one reflection the proof finds an all-rotation subsequence; with at least D(A) + 1 reflections it uses signed pair labels; the intermediate range yields a product-one subsequence or a proper subgroup reduction.The intermediate reduction uses the weighted structural theorem; the subgroup descent then establishes the required product-one conclusion for every proper subgroup.Source: §4.1 · p. 48, §4.2 · p. 48, §4.3 · p. 49

5.1 Three subgroup estimates

  • Three subgroup estimates support the quotient arguments: target-length bounds, concentration transitivity, and correction of a K-valued quotient defect.For the correction step, a disjoint signed rotation sequence summing to −z combines with the selected reflection sequence to form a product-one sequence.Source: §5.1 · p. 50

5.2 A reflection-containing quotient block

  • A reflection-containing product-one block in the quotient yields either a product-one subsequence of length 2Q or a strict-subgroup concentration alternative.The proof lifts the quotient block and corrects its K-valued defect using a disjoint rotation sequence.Source: §5.1 · p. 50, §5.2 · p. 51

5.3 The rotation-only quotient case

  • If Y has length 2Q+DA, the same counts a,b as S, and T_K(Y) has no reflection-containing product-one subsequence, then either Y has an all-rotation product-one subsequence of length 2Q or some H<K and α∈K make τα(Y) satisfy Q(H).If an all-rotation subsequence of length 2Q is product-one in τα(Y), the same positions form a product-one sequence in Y.Source: §5.3 · pp. 52–53

5.4 Simultaneous induction

  • Strong induction on subgroup order proves PS(K) and Q(K) by applying the two quotient-case propositions and transferring translated solutions back to the original sequence.The base case K = 0 follows by extracting rotation-only product-one blocks and extending with identity rotations.Source: §5.4 · p. 54

6 Completion of the proof

  • The proof establishes E(G) = 2Q + DA by reducing the remaining reflection-count range to a subgroup case and applying Theorem 5.1.The other ranges follow from Propositions 4.1 and 4.2; Proposition 4.3 either gives the subsequence directly or yields the subgroup hypothesis.Source: §6 · p. 54

Related papers

Loading 2609.00032v1…