# Source adjudication of the independent panel

The original model responses remain unchanged. This document is the Codex curator's source-based adjudication, not an additional independent referee. The initial source assessment was saved before completed panel responses were opened.

## Evidence standard

An objection requires an exact inference or counterexample satisfying the statement's hypotheses. A model saying “checked” reports its assessment; it does not supply executable verification or certify the entire proof. Absence of an objection and agreement among models are not certificates.

## Scope and source clarifications

- **Gemini's Lemma 3.5 locator:** its description of the three-kernel shear and the zero-coefficient split refers to the concluding proof of Proposition 3.1, following Lemma 3.5. Lemma 3.5 itself establishes the monomial/shear Fourier layers. The formulas are present, but that audit row's locator is imprecise.
- **Gemini's empty obligation list:** its sweeping “checked” statements do not demonstrate that every external theorem was inspected. The request supplied the manuscript only. Sol explicitly leaves companion claims and contextual lower bounds unverified; Grok similarly distinguishes external attributions. Preserve this coverage distinction instead of treating all three as exhaustive audits of the bibliography.
- **The finite network:** the incidence cancellation, terminal-frame mechanism, residual count and exact recurrence are actually written in Section 2. A dependency on the companion's unseen integer-multiplication precision analysis is not needed for these displayed identities. The curator's exact arithmetic reproduces the saving, but has not generated and verified the complete million-dimensional binary-label schedule.
- **Auxiliary values and width:** arbitrary initial contents are explicitly handled in both the finite network and the local replay lemma. An objection premised on zeroed borrowed registers would need to address the source-suppressed second replay and the full-role frame identity.
- **Prepared scalars:** the main proof charges the transform of the fixed chirp operand as a third full transform. Conjugation appears only as a prepared-scalar construction through inverse-root DAG evaluation. The native model does not conjugate variable input or hide arbitrary initial roots in rational field operations.
- **Uniformity:** the explicit schedule and measured workspace test form the main quantitative route. Appendix A's bounded printer is a separate route to a qualitative bound. Sol correctly marks its theorem as conditional on the stated printer contract while checking the supplied local construction. Uniform and nonuniform companion statements must remain separate.
- **Decimal exponent:** the exact fraction and strict exponent inequality establish the advertised eventual power bound independently of the long decorative decimal expansion. The local check reproduces the fraction and its rational comparison; it does not certify every displayed decimal digit.

## Strongest outstanding checks

The complete finite binary-label schedule and operation count, implementation of the exact-width compiler at every width, and the all-array indexing ledger merit dedicated machine-checkable verification. The companion theorems, external attribution and discovery provenance remain separate obligations. No target Lean build, target axiom report or statement comparison was performed.

The final panel report lists every completed assessment and every incomplete native attempt. No mathematical conclusion is assigned to a refusal, timeout or exhausted output cap.

## Opus high-effort objections

Opus returned two items classified as unverified steps and reported no demonstrated error.

1. **Preparing L⁻¹:** Section 5 uses `F_L⁻¹=L⁻¹ JF_L` without repeating a scalar-integer construction. The later proof of Corollary 1.3 explicitly constructs the analogous integer M by binary doubling/addition and divides by it. Applying that same construction to the known positive integer L costs O(log L) field operations; L is nonzero. This is a harmless detail to make explicit in Section 5, not a demonstrated cost or correctness defect. The construction is in the frozen manuscript, although its earlier application is implicit.
2. **Ordering the power-of-two fibers:** CRT indexing does not impose a fixed order on the factors. Choose the power-of-two digit as the most significant digit and the odd-prime product as the remaining field. Holding that digit fixed gives contiguous arrays for Proposition 4.2. For the remaining power-of-two transform, a transpose/copy of each fiber or another prefix permutation costs O(L); the Section 4 traversal covers that operation. An explicit layout sentence would improve the exposition. No unavoidable extra logarithmic factor was demonstrated.

Opus also leaves the Appendix A amplification induction incompletely rederived. Its source locator “(A.5) amplification” refers to `syn:amplification`, which is (A.3) in the supplied PDF; (A.5) is the later uniform-cost formula. This optional route remains an audit obligation and does not supply the main quantitative exponent. Several of Opus's Section 2 equation numbers similarly drift; native source labels identify the intended passages.

## Fable high-effort objections

Fable reports no demonstrated error, with three concerns that its own derivations characterize as consistent or expository.

1. **Huge tables and address width:** the proof of Theorem 2.6 explicitly uses the direct method below K=72m and introduces column tables only in the recursive range. Thus their m-bit indices fit the k+O(1)-bit address contract when used. The table and role constants are enormous but fixed independently of n. This explains the source's lack of a useful crossover estimate; it is not a violated inequality. Fable's approximate `S≈1.87×10²⁷` refers to the unpadded residual count s; the padded S is `2⁷¹m−Δ`, approximately `2.36×10²⁷`. Both are fixed constants.
2. **Bounded-fan-out convolution DAG:** a binary butterfly can be printed as one fixed-scalar multiplication followed by two sums. Each evolving coordinate has at most two uses per butterfly level. The inverse has the same structure; fixed diagonal products add one level. In the three displacement branches, a source enters at most three such circuits, so this construction has an absolute fan-out bound (six suffices at the shared sources), including the final output reads. Gate count is O(v log v), depth O(log v), and the two output additions per target do not create unbounded fan-out. The source already sketches this construction in Section 3.2; writing explicit constants would improve inspectability. No missing asymptotic premise is demonstrated.
3. **Synchronizing children:** identity monomial rounds are allowed by the definition of mixed rounds. Pad the shorter child word to the longer child's length on disjoint blocks, then execute the cross update. This realizes the displayed maximum-depth recurrence at the original width. The later compiler explicitly describes identity padding. A local reminder in the Toeplitz recursion would improve exposition; it does not require a change of exponent or width.

Fable calls its appendix coverage a spot check and leaves its algebra extraction/printer obligations open. Its phrase “nonuniform/companion route” is imprecise: Appendix A includes Theorem A.4, an explicitly uniform all-length conclusion. That route is complementary and weaker than the quantitative main theorem, rather than solely nonuniform. The original response is preserved with this clarification.

## Result of adjudication

All five completed responses report `no_demonstrated_error_found`. This records the panel's assessments, not a proof certificate. Opus and Fable offer useful exposition/accounting clarifications, with no supplied counterexample or invalid inference surviving the source checks above. Fable's limited Appendix A coverage, Opus's incomplete amplification check and the curator's unexecuted full-network obligations remain visible. A completed five-provider panel is broader scrutiny than a single review, but the next decisive evidence would be a checkable complete network certificate and a target formalization audit.