OpenAI Math import

8 October 2026 — OpenAI Math offers three transfer mechanisms, but no ready Frege theorem

Source audit and conditional research proposals; neither target lower bound is advanced. Produced by Codex (gpt-6-astra, medium reasoning).

Cite as: Kamil Braun, “OpenAI Math offers three transfer mechanisms, but no ready Frege theorem”, OpenAI Math import, Noemesis research notebooks, 8 October 2026, https://kbr.is-a.dev/math-research/branches/openai-math-import/#entry-2026-10-08-openai-math-survey.

Assignment. The user requested cloning OpenAI Math, searching for material useful to the main or Near-half PC degree notebook, recording findings here, and notifying their sessions about useful imports. This is a bounded source survey, not a Spin or a scheduled route review.

Question. On side-source-transfer, can a source result give a quantitative, source-specific nonlinear retained-error bound on the same filtered quotient, with one surviving weight, all original degrees and coherent legal coefficient choices, or supply the alternative route's near-half Boolean PC family? The latter needs a polynomial-size Boolean family with a barrier over \(\mathbb F_2\) at \(D=\lfloor v/2-s(v)\rfloor\), with \(s=o(v/(\log v)^{\ell-2})\), in actual Boolean variables, plus complete Frege transfer. A new analogy, circuit lower bound, or unspecified linear degree bound does not meet either endpoint.

New mathematics. None. This entry records source-reported statements, inspected proof mechanisms, explicit transfer gaps and a search inventory. It does not certify the collection's headline claims.

Goal progress. Unchanged for the main binary lower bound, the near-half family, and this notebook's useful-transfer obligation. Three concrete mechanisms merit import as research leads; no hypothesis-compatible transfer has been proved.

Source and coverage

The clean checkout is ~/dev/openai-math, from commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. The first full clone timed out; a monitored depth-one fetch and checkout succeeded. Thus this is a shallow clone of that revision, not a claim to have downloaded all historical Git objects. The source README describes 719 manuscripts in 372 families. Family IDs have gaps and reach 377. The web-rendered catalogue differed from the local text; conclusions here use the pinned local checkout.

The survey screened the catalogue's family titles across all 17 subject headings, read targeted summaries, and searched all preprint TeX for Frege, polynomial calculus, proof complexity, pseudoexpectation, Nullstellensatz, sums of squares, Hilbert series, rank and polynomial-method terms. The only literal polynomial-calculus hit in the narrow search is spectral polynomial calculus in the Thorp paper, not the proof system. This is a source-discovery result, not an assertion that no useful lemma is hidden elsewhere. Most manuscripts were not read in full. The source scope and search record identifies the exact files read and the limits.

Version and verification caution. The upstream history records withdrawals and repaired papers. Each selected mechanism below is cited at the pinned revision. The Lean comparator files are statement challenges and intentionally contain sorry; their JSON configurations point to separate solution modules. For families 112 and 274, the corresponding top-level solution declarations were also inspected. No Lean build or comparator replay was run, and no dependencies were installed. The existence of a scope note or solution file is not claimed here as an independent verification.

First proposal: normalized reverse paths

Family 112, OpenAI, Beyond the Square-Root Exponent for Depth-Three Boolean Circuits (23 September 2026), contains the Restriction bound, the named Restriction bound. For a width-at-most-\(k\) CNF, independently retain variables with probability \(p\), assign the rest uniformly, and take \(b\ge1\). If \[ \theta=\sum_{j=b+1}^{k}\binom kj\left(\frac{2p}{1-p}\right)^j<1, \] the paper constructs a signed combination of width-at-most-\(b\) CNFs whose coefficient mass \(W\) has \(\mathbb EW\le(1-\theta)^{-1}\). Consequently every real test function's correlation with the restricted CNF is at most \(W\) times its largest absolute correlation with a width-\(b\) CNF. The choice of expansion does not depend on the test function. The bound has no clause-count factor.

Proof inspected in full. The finite expansion follows compatible sequences of violated clauses. Each step fixes more than \(b\) new live coordinates. A path receives reciprocal counts of already determined violated clauses. A marker-permutation experiment represents the remaining reciprocal functions as convex mixtures of narrow CNFs. Counting paths backward cancels the number of eligible clauses against the reciprocal count and gives a geometric series in \(\theta\). Duplicate clauses are explicitly allowed and counted in both numerator and denominator. This is a concrete way to avoid paying the entire inventory at every local correction.

Proposed import. The main session should test normalized reverse-path counting against the actual retained-error inventory, rather than importing the headline circuit theorem. The first missing bridge is a degree-compatible finite-field certificate or a rank inequality on one surviving quotient. The source uses positive real probabilities and divides by integer violation counts; those denominators need not be invertible modulo the proof characteristic. A signed representation with small real coefficient mass need not have few terms, low algebraic degree, or a nonzero surviving weight. Uniform Boolean restrictions must also preserve the selected hard family. The near-half session may inspect this as a restriction mechanism, but it presently supplies no lower bound on PC degree and its main theorem has only depth three and no MOD gates.

Second proposal: branch-centered matrix smoothing

Family 126, OpenAI, Exponential PSD rank of positively shifted matching matrices (5 October 2026), has a separate Fourier smoothing of matrix squares theorem, the named Fourier smoothing theorem. It assumes product channels from finite \(X_i\) to \(Y_i=(\mathbb F_2)^a\), uniform averaged marginals, and a scalar variance estimate with constant \(\theta\) for every real test function. Put \(L=2^a\), \(C_L=2^{L-1}\). For a real PSD matrix function \(F\) of size \(r\), with \(\operatorname{tr}F\le B\), and \(\lambda>1\) satisfying \(L\lambda^2C_L\theta\le1\), it constructs an exact square decomposition of the product average with a separate Fourier center \(q\) for each branch. Some channel choice satisfies \[ \sum_{q,p}\lambda^{\operatorname{dist}(q,p)}\|\widehat H_{q,p}\|_F^2 \le L^t\sqrt r\,B\,2^{t/2}. \] This includes exponential costs in the number \(t\) of blocks; it is not dimension-free in every parameter.

Proof inspected in full with its splitting lemma. Orthogonal row tags make product averages exact. Spectral splitting assigns frequency Gram matrices to branches, controlling misplaced compressions by pairwise overlaps. A fourth-order Gram potential grows by at most two per block. The final rank bound uses the number of columns, not the growing row dimension. Multiplication by a branch's real sign character recenters its Fourier support while preserving its square. Future channel parameters stay independent of choices already made; no unjustified conditioning independence is assumed.

Proposed import. This is a concrete comparison object for the main notebook's graded/matrix polymer item: try separate centers for surviving error pieces, retaining a joint overlap potential, rather than bounding each piece around zero. Its direct use fails at the current interface: PSD order, real Fourier characters and Frobenius norms are not finite-field rank; over \(\mathbb F_2\), the signs \(+1\) and \(-1\) coincide. A suitable replacement must pay translation degrees and all branch costs, and establish its channel variance hypothesis on the actual quotient. The reread truncated-kernel dependence example rules out inferring independence merely from disjoint supports. The legal-row counterexample also prevents an automatic relative-rank improvement. The source's shifted matching PSD lower bound is not a near-half PC theorem.

Third proposal: a finite backward scale induction

Family 274, OpenAI, Product-projection localization and the QAC0 parity lower bound (24 September 2026), states localization, the named localization theorem. On \((\mathbb C^2)^{\otimes N}\), let \(M,D\) count mismatches against product vectors and let \(U\) have fixed depth of disjoint product-reflection layers and local unitaries. For every fixed \(0\le s<t\), uniformly in these choices for sufficiently large \(N\), \[ \|[M\ge N^t]U[D=0]U^\dagger[M=0]\|\le e^{-N^s}. \] The allowed gates and complex operator norm are essential parts of the statement.

Mechanism inspected. The complete backward-step proof replaces only one projection after squaring a transition norm. The remaining tail is conjugated into the inverse circuit with the two mismatch counts exchanged. Assuming localization at the preceding depth for every fixed exponent pair, the same-depth implication runs from \((t,b)\) to \((s,t)\) for \(t<b<2t-s\). A finite chain reaches a mismatch exponent above one, where the tail vanishes, then returns backward. The polynomial-approximation and preceding-depth lemmas were identified but not fully audited here.

Proposed import. Test whether the complete retained-source error map admits a dual formulation closing the high-degree tail at a larger cutoff. The first task is an exact interface, not another cutoff optimization: give an adjoint or reversible map on the same filtered quotient, a finite terminal regime, and the full degree ledger. PC inference and the present compiler are not unitary or automatically inverse-closed. Rank has no replacement supplied here for the source's norm-squaring estimate. A quantum circuit parity lower bound does not imply an \(\mathrm{AC}^0[2]\)-Frege lower bound; parity gates are allowed in the latter. This remains a method proposal, not a reduction.

Near-half candidates and other screened material

Remaining subject coverage. Number theory; algebraic/complex geometry; real/complex analysis; convex/metric geometry; dynamical systems; group theory; operator algebras; topology; functional analysis; differential geometry; and PDE were screened through catalogue titles, with targeted keyword hits across their TeX included in the global search. No direct source-to-goal implication was identified in that screening. This does not close any of these fields as a source of future ideas. The other six catalogue headings are represented by the specific candidates above: theoretical computer science, combinatorics, algebra, probability/statistical mechanics, mathematical logic, and mathematical physics.

Novelty, transfer decision and communications

Claim searches covered signed restrictions, clause-count independence, Fourier/matrix smoothing, backward localization, coboundary expansion, and lex-plus-powers; literal-name searches also covered both target notebooks and the historical index. The relative-dimension and relative-intersection records were reread in full and their reviewed graph links inspected. No prior record of these exact OpenAI sources was identified; no global novelty claim is made. Existing Boolean kernel controls remain constraints on any proposed translation.

The proposed imports are the three mechanisms above, each with its open bridge, not the repository's headline conclusions. Proposals containing this notebook's local path and stable anchors were accepted for active-turn delivery to Math auxiliary (the main Frege session on aux) and Near-half PC degree. The latter also received the explicit negative screen of families 177, 200 and 235. The exact messages and delivery status are retained without runtime session identifiers; no recipient response or import is asserted.

Gate for every proposed test. An identity, potential or dual map alone is insufficient. Main-route success requires the quantitative source-specific bound on the same filtered quotient, one surviving weight, coherent legal choices and all original degrees. Near-half success requires a polynomial-size Boolean family, the displayed barrier over \(\mathbb F_2\) in total Boolean variables, and complete Frege transfer.

Sub-ideas

• Translate the family-112 reverse-path normalization into a degree-compatible finite-field source identity or conditional-rank bound; explicitly handle violation-count denominators and survival under restrictions. Resolve the interface before estimating a long inventory.
• Test a branch-centered graded overlap potential inspired by family 126 on actual retained errors, with finite-field replacements for positivity and sign characters, source-specific conditional dependence, and all translation and branch costs.
• Test a finite backward-cutoff induction inspired by family 274 only after defining the dual error map, same-quotient comparison, paid degrees and terminal regime; determine whether irreversible source operations prevent that interface.
• For the near-half route, investigate whether family-177 complexes admit a nontrivial alternative encoding or characteristic with an explicit PC barrier in total Boolean variables; the direct binary linear encoding is not a hardness candidate. Audit the construction proof before relying on the complex family.

Verification gate. The sole isolated medium reviewer passed with scope corrections, all incorporated: preceding-depth localization, expander dimensions, SAT sampling, the precise monomial-ideal conclusion and the full target gates. The review report confirms the displayed formulas and unchanged goal assessment. No finite computation or formal proof verification was performed. Full reading of the restriction proof and the matrix-smoothing proof with its splitting lemma supports the mechanism descriptions, not independent certification of either complete paper. The localization backward-step proof was read with the separate unaudited prerequisites identified.

Timing scope. Mandatory restoration and initial notebook setup preceded instrumentation; the timed interval includes the failed clone, successful retry, source reading, review, communication and checkpoint preparation.

Measured timing

8 October 2026 — BMD candidates: Betti bounds, canonical symmetric maps and interpolation

Source audit and conditional import proposals; no BMD threshold or exception cutoff proved. Produced by Codex (gpt-6-astra, medium reasoning).

Cite as: Kamil Braun, “BMD candidates: Betti bounds, canonical symmetric maps and interpolation”, OpenAI Math import, Noemesis research notebooks, 8 October 2026, https://kbr.is-a.dev/math-research/branches/openai-math-import/#entry-2026-10-08-openai-bmd-survey.

Picked. The user requested: “Search also for anything potentially useful for BMD.” This extends the source survey without changing the BMD session's active assignment.

Source refresh. The user also requested tracking and pulling main on future repeats. The checkout was already on main with upstream origin/main; it was not detached. The pull performed during this survey reported “Already up to date.” The inspected revision remains fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. The living Source refresh policy owns the future rule; old source citations remain reproducible.

Question. BMD's characteristic-two formula and dimension-three odd-field case are already solved. Relevant open work concerns small-prime stable root-curve orders and the characteristic-zero first-step and remaining pre-stable thresholds. On side-source-transfer, find a source theorem or concrete proof mechanism that addresses one of these necessary implications while retaining the actual marked source and its coefficient field.

Current obstacle. The live BMD notebook was read in the main checkout at revision 9322276a71043103181f5e5d6eab14a59b144c5e, including its latest global architecture review and outer quadratic cover. This is newer than this worktree's BMD overview. Its immediate assignment is the next actual section obstruction in eight characteristic-three coefficient classes, with global principal-part corrections and integer-multiplier dependence retained. It also still needs outside-progression coverage and a global finite candidate set. A theorem about contraction or finite generation alone does not close that endpoint. The source paths, reading scope and exact target revision are retained in the source record.

New mathematics. None. Three candidates warrant scoped proposals for the characteristic-zero part of BMD. One more distant positive-characteristic mechanism was inspected and compared with a stronger already-recorded BMD splitting. No external headline theorem is adopted as a verified local result.

Goal progress. Unchanged. There is no new stable-order family, first-step threshold, computed exception set or evaluated global cutoff. No theorem found here directly settles the live characteristic-three obstruction.

Lex-plus-powers and the actual Ext target

Family 200, OpenAI, The Artinian Lex-Plus-Powers Betti Theorem (23 September 2026), states in its main theorem and characteristic-zero corollary: for a homogeneous ideal \(I\) in a standard graded polynomial ring over a characteristic-zero field, containing a regular sequence of degrees \(2\le a_1\le\cdots\le a_c\), there is a lex-plus-powers ideal \(J\) containing \((x_1^{a_1},\ldots,x_c^{a_c})\) with the same Hilbert function and \[ \beta_{i,j}(S/I)\le\beta_{i,j}(S/J) \quad\text{for every homological and internal degree }(i,j). \] The corollary allows \(1\le c\le\dim S\), so is not confined to Artinian quotients. This was unsuitable for the binary Frege route but its field matches BMD's characteristic-zero component.

Specific target. The reread actual-prefix formula expresses the first-step threshold using \(e_N=\operatorname{indeg}\operatorname{Ext}^2_S(C_N^+,S)\). The missing reverse bound is \(e_N\ge-\max(p_N,4N-5)\), where \(p_N=\binom N2+2\). A suitable bound on the shifts in the actual second free module could help exclude lower-degree Ext classes. This is a possible route through a presentation and grading comparison, not a consequence of the displayed ideal theorem as it stands.

Transfer gate. BMD uses the weighted ring \(S=k[c_2,\ldots,c_N]\), \(\deg c_j=j\), a shifted marked free core and a module cokernel \(C_N^+\). The source's headline theorem is about standard graded cyclic quotients \(S/I\). Supply the actual compatible presentation or reduction, retain all shifts and the marked highest coefficient, identify the regular sequence and determine the Hilbert data needed to construct the comparator. An unknown Hilbert function cannot simply be treated as computed. Betti domination is one-sided; it does not identify Ext or the original marked image.

Proof mechanism read. Sections on leading coefficient spaces and monomial reduction were read in full. The former is a filtered Koszul comparison with vector-space coefficients; it preserves the Hilbert function and can only increase graded Betti numbers on passing to the leading submodule. The latter transfers a minimal resolution using commuting linear forms over a division algebra, then cancels a common dimension factor. The deep existence of those forms and the full lex compression proof were not reverified. The filtered comparison is a standard degeneration principle, not a new result claimed here. Its published formulation still has an unshifted coefficient space and standard grading.

A bound for the canonical image, not just its ambient representation

Family 210, OpenAI, Quadratic stabilization of the canonical Foulkes–Howe map (25 September 2026), states for every finite-dimensional complex vector space \(V\), \(a\ge2\), and \(b\ge a(a-1)\) that the specified map \[ \mu_{a,b,V}:\operatorname{Sym}^b(\operatorname{Sym}^aV) \longrightarrow\operatorname{Sym}^a(\operatorname{Sym}^bV) \] is surjective. See the source, main theorem. The convention matters: it is multiplication in the invariant tensor algebra, identified by averaging. If \(A\) is the subalgebra generated in degree one and \(R\) its stated normalization, the conclusion is \(A_b=R_b\) in this range, uniformly in \(\dim V\). It is stronger than existence of some equivariant embedding in the opposite direction, and does not claim the optimal threshold.

Proof read through completion. The proof converts the canonical image to a diagonal-vanishing criterion for symmetric multilinear forms. A directional derivative moving degree from an independent variable block \(U\) to another block \(Y\) is injective when \(\deg_U>\deg_Y\), by the positive Fischer inner product. Two sequences of those operators first free one slot and then remove a shared power. The degree accumulated in the shared block produces the quadratic bound. Polarization, factorial divisions and positivity are characteristic-zero inputs.

Proposed BMD use. Test whether a characteristic-zero coefficient-image or polynomial-descent obstruction is an explicit quotient or compatible subdiagram of this canonical map. This targets the difference between an actual polynomial image and its normalized ambient module, which the recorded image obstruction makes essential. It does not license replacing BMD's image by its normalization: the six-root witness and its formal extensions must remain falsifying controls. Nor does ambient surjectivity imply surjectivity on the marked constrained subspace. The first test is to exhibit the exact map and parameter correspondence on the known six-root control, including its grading; without that diagram there is no BMD application. The source proof supplies no characteristic-three analogue.

Theta degeneration and a two-coordinate interpolation criterion

Family 039, OpenAI, Nagata's Conjecture for Plane Curves (23 September 2026), states the strict Nagata inequality for arbitrary multiplicities at \(r\ge10\) very general complex plane points. Its main theorem cannot be applied to the fixed cube, collision strata or a prescribed root configuration. The more useful item is the elementary horizontal-row interpolation lemma.

For a finite set \(E\subset\mathbb C^2\) with coordinates \((j,K)\), let \(N_K\) count its points at height \(K\). If \(q,m\) are positive integers and \[ N_K\le m,\qquad \#\{K:N_K\ge t\}\le q(m-t+1)\quad(1\le t\le m), \] the monomials \(K^\ell J^b\), \(0\le b<m\), \(0\le\ell<q(m-b)\), interpolate every function on \(E\). Its complete proof orders rows by size, interpolates within each row, and multiplies each correction by factors vanishing on earlier rows. The row-size distribution, not just the total number of exponent pairs, pays both degrees.

Proposed BMD use. In a permissible theta degeneration or confluent window, identify the actual limiting marked matrix with such a two-coordinate evaluation matrix and check its row profile. This is a possible sufficient rank certificate for characteristic-zero contact or interpolation windows; the lemma itself is familiar triangular interpolation. I read the full interpolation section, but only the introductory description of the theta degeneration. The latter requires its own full audit before use. The source takes common powers to absorb an integer endpoint error; that does not directly recover BMD's exact per-order thresholds. Small-characteristic residue collisions and Hasse binomial coefficients also prevent transplanting the complex exponent matrix unchanged. Existing Tate interpolation and fat-point leads are prior work, not newly discovered subject areas.

The live small-prime obstruction: a more distant comparison

Family 313, OpenAI, Finite generation for the K(n)-local sphere (24 September 2026), has a fixed normalized Cartier transfer in its particular finite marked Lubin–Tate setting. With a whole finite free algebra \(A'\), a localized idempotent summand, an invariant volume and a suitable constant-field-fixing power \(h_0\), it proves a pole estimate \[ S(x^{-D}A')\subset x^{-\lceil D/h_0\rceil-c}A' \] with one fixed \(c\). The associated fixed-finite-diagram lemma transports chosen splittings through roots and keeps one pole bound for the entire diagram. The exact statement, whole-model pole argument and fixed-diagram proof were read; the construction of the required invariant volume and geometric marking machinery was not audited.

This suggests comparing the next BMD section obstruction with a coherently transported finite principal-part diagram, rather than rebuilding unrelated inverses at larger exponents. However, the needed root identification of the full global correction diagram is missing. BMD already has a more directly applicable source-specific tool for bare degree contraction: the reread polynomial Frobenius splitting retains every marked jet and the exact divisibility image. Reproving contraction would be no progress. A genuinely useful import would have to preserve the higher nonlinear obstruction, its integer-multiplier dependence and global corrections, and reduce the complete exception problem. A finite pole bound is not a finite set of rank states or an evaluated global cutoff. This comparison is lower priority than the existing BMD-specific machinery.

Other searches and scope exclusions

• Family 311 classifies radical ideals invariant under open subgroups of the Honda formal-group stabilizer in a Lubin–Tate deformation ring. Its exact introductory theorem was inspected. No such stabilizer invariance or ring identification is supplied for BMD's theta obstruction; this is not a theorem about arbitrary Frobenius-stable ideals.
• Families 193–194 concern Serre intersection multiplicity and Hilbert–Samuel multiplicity under flat local maps. Catalogue statements give no marked jet-rank or graded initial-degree formula. Families 059 and 064 concern complex singularity topology and Milnor numbers; the shared word “multiplicity” does not match BMD's finite-grid problem.
• Family 205's symmetric-group tensor-square occurrence theorem does not determine the actual marked coefficient image. Family 208 concerns finite symmetric tensor categories, not automatic full rank of a Hasse matrix. Family 142's prime-field factoring algorithm supplies neither the missing polynomial nor an exception cutoff; no factoring bottleneck was identified in the live BMD test.
• The positive-characteristic multipoint Seshadri result in family 039 concerns a geometric generic tuple on a polarized variety for sufficiently many points. Its catalogue statement does not supply a theorem for this structured cube or root family; its proof was not audited.

Novelty and dependencies. Searches included Foulkes, lex-plus-powers, Eisenbud–Green–Harris, Nagata, Cartier contraction, and the actual Ext and normalized-image formulations. Foulkes had no registered match in either this checkout or the live BMD checkout. The old fat-point lead and existing exact Frobenius split were retained explicitly. The complete actual-prefix formula, normalized-image obstruction and polynomial splitting record were reread; reviewed dependency links were inspected for the first-step and splitting claims. These are bounded source comparisons, not global novelty certifications or a re-verification of every dependency.

Sub-ideas

• For the characteristic-zero first-step target, determine whether a source-compatible standard graded ideal/module comparison makes the lex-plus-powers Betti bound control the actual weighted second-Ext initial degree, retaining the marked coefficient and known normalization obstruction.
• Construct or rule out a precise characteristic-zero map from the relevant BMD coefficient image to the canonical Foulkes–Howe multiplication diagram, starting with the six-root marked-image control; preserve constraints and grading before invoking ambient surjectivity.
• Read the full family-039 theta degeneration and test whether an actual BMD characteristic-zero window has its two-coordinate exponent matrix and row-size bounds; retain endpoint costs and do not replace the structured configuration by very general points.
• Compare the live higher section obstruction with a single root-compatible principal-part diagram and bounded pole corrections as in family 313, only if it adds something beyond the existing exact polynomial Frobenius split; retain nonlinear multiplier dependence and the separate global cutoff requirement.

Verification gate. The sole actual reviewer was a fresh native GPT-6.1-Sol subagent at medium effort, following the updated reviewer protocol. It passed without required corrections, including fields, gradings, map direction and unchanged goal progress. The retired root launcher had refused before inference; no second review occurred. No numerical experiment, Lean build or full-paper correctness certification was performed.

Communication. The reviewed proposal was accepted for active-turn delivery to Math, the BMD session. The exact message and delivery status retain all three primary candidates, the lower-priority Cartier comparison, and the explicit statement that none closes the current characteristic-three task. No recipient response or completed import is asserted.

Timing scope. The first BMD overview read preceded instrumentation; subsequent target restoration, main-branch refresh, source reading and review are timed.

Measured timing

11 October 2026 — Imported quasi-Riemann and related zero-free manuscripts

Imported source statements; complete proofs and formal verification remain unaudited. RH source import. Produced by Codex (gpt-6.1-sol, medium reasoning).

Cite as: Kamil Braun, “Imported quasi-Riemann and related zero-free manuscripts”, OpenAI Math import, Noemesis research notebooks, 11 October 2026, https://kbr.is-a.dev/math-research/branches/openai-math-import/#entry-2026-10-11-openai-rh-import.

Picked. The user requested: “Pull the openai-math repk. Then search it for anything related to Riemann hypothesis. Import this stuff.”

Question. On side-rh-import, identify which repository statements address zeta or generalized zero-freeness, their exact fields and boundaries, and what verification supports them. The missing source-audit implication is from an upstream headline to a reliable, precisely scoped local mathematical dependency. This turn imports the evidence and statements; full-proof or transitive Lean verification would be needed to adopt them as established dependencies. Completion of the requested import is separate from proving RH.

Acquisition and retention. The source checkout remains on main, tracking origin/main. The requested pull reported “Already up to date.” The source-scope record identifies the exact upstream revision, searches and reading limits. Four complete manuscript directories, including PDF, TeX and citation metadata, are retained under the local import. The upstream Apache-2.0 license, attribution and selected Lean scope files accompany them. Unchanged upstream Markdown is archival source, not rewritten prose.

New mathematics. No original result. Four attributed external statements are registered as context, with imported status in their assessments. Their substantial proofs are preserved in full source form, but only the exact statements, selected reductions, conclusions and formalization entry declarations were read in this turn.

Goal progress. Unchanged for the source-audit obligation: none of these mathematical results has received complete independent verification here. The requested source import is complete. No full Riemann-hypothesis proof is supplied by the selected manuscripts; the strongest directly relevant zeta boundary they state is \(7/8\).

Seven-eighths half-plane

Source. OpenAI, The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane \(\Re s>7/8\), 30 September 2026, main theorem. Imported PDF; complete TeX; live upstream source.

Imported statement. thm:openai-seven-eighths-half-plane: every Dirichlet \(L\)-function, including \(\zeta\), and every finite-order Hecke \(L\)-function over \(K=\mathbb Q(\sqrt{-3})\), is zero-free in \[ \Re s>\frac78. \] Principal-character poles at \(s=1\) are allowed. The boundary \(\Re s=7/8\) is not excluded. The width is independent of character, conductor and height; constants in intermediate fixed-character estimates may depend on that character. The source's Hecke convention is a finite-order ray-class character extended by zero on noncoprime ideals; it includes imprimitive characters. Status: source-reported theorem, not a locally established theorem.

Proof map and reading limit. The paper first establishes an \(11/12\) half-plane, then sharpens it with compensated prime slots, asymmetric scales and moment estimates. Cubic theta reflection and Poisson summation give two expressions for the same completed sum; the principal row exposes a reciprocal Hecke \(L\)-function. A continuation criterion uses target-independent exponent savings. The exact main statement, introductory conventions, the first-stage final proof and the order-of-choices statement with part of its proof were read. The long reflection, moment, zero-detection and continuation inputs were not audited in full. Keeping a reciprocal factor and a uniform width in a proof outline does not certify the required bounds.

Relation to RH. The usual RH requires every nontrivial zeta zero to have real part \(1/2\); the source itself explicitly states that its \(7/8\) theorem does not establish RH or its generalized versions. Its conclusion would confine the rightmost nontrivial zeros to real part at most \(7/8\). No boundary improvement to \(1/2\) is imported.

Eleven-twelfths alternative

Source. OpenAI, The Quasi-Riemann Hypothesis, 5 October 2026, main theorem; its README reports human assistance. Imported PDF; complete TeX.

Imported statement. thm:openai-eleven-twelfths-half-plane: for the same Dirichlet and finite-order Eisenstein-field Hecke families, the source states zero-freeness in \(\Re s>11/12\), with the principal pole treated by meromorphic continuation. This is a later presentation with a weaker boundary than \(7/8\), not a replacement by a stronger theorem. Formally, \(\Re s>11/12\) implies \(\Re s>7/8\), so the seven-eighths statement implies this conclusion on the same families. That comparison is recorded as refinement of statements, not verification of either proof.

Complete reduction read. For a fixed Hecke character \(\nu\), an excluded prime set \(S\), and compactly supported smooth \(W\), the paper's principal input is a family mean-square bound \[ \sum_{0<N(u)\le D^{1+\vartheta}}|A_u(D)|^2 \ll_{\nu,S,I,\vartheta,\varepsilon} \left(\max_{j\le k}\|W^{(j)}\|_\infty\right)^2D^{2+\vartheta+\varepsilon}, \quad0<\vartheta\le1/10. \] Here \(A_u(D)\) is the twisted Möbius sum defined in its reduction section, and the finite smoothness order \(k\) depends on the losses. Rows at prime sixth powers yield a pointwise bound \(A_1(D)\ll D^{11/12+\varepsilon}\). The Mellin transform of that sum equals \(\widehat W(s)/L_K^S(s,\nu)\) in its original convergence region, and continuation gives the stated exclusion. The reduction then uses quadratic base change to reach Dirichlet functions, with nonvanishing at one preventing pole–zero cancellation. This entire deduction was read; the proof of the family mean-square bound was not. It therefore remains the central unaudited input of this alternative route.

The introduction states further prime-distribution, least-nonresidue and class-number consequences. Their exact dependence and effectivity proofs were not audited and they are not separately promoted to verified imported claims. Their full source text is retained.

Uniform real-zero gap

Source. OpenAI, Uniform exclusion of Landau–Siegel zeros, 1 October 2026, main theorem. Imported PDF; complete TeX.

Imported statement. thm:openai-real-zero-gap: there exists one absolute constant \(c>0\) such that every primitive nonprincipal real Dirichlet character of conductor \(q\ge3\), and every real zero \(0<\beta<1\) of its \(L\)-function, satisfy \[ (1-\beta)\log q\ge c. \] Both character parities are included. This excludes zeros in \(1-c/\log q<\beta<1\), not all real zeros in the critical strip. The imported source and external Lean scope provide no explicit numerical value of \(c\).

Proof map. The claimed proof converts a putative small normalized zero gap into a prime-character bias, constructs a nonzero weighted interpolation determinant in a biquadratic field, and compares its Archimedean size with prime divisibility. Its final limiting comparison contradicts \(1\le7/8\). The main statement, introductory outline and final contradiction were read; the analytic prime-bias, projected-box interpolation and determinant-divisibility lemmas were not audited in full. This paper is imported as its own argument, rather than claiming its proof is verified by the other zero-free paper.

Cyclotomic Hecke half-plane

Source. OpenAI, Primitive roots for every admissible integer base, 4 October 2026, the separate Hecke zero-free theorem. Imported PDF; exact introductory theorem.

Imported statement. thm:openai-cyclotomic-half-plane: for every cyclotomic number field \(F\) containing \(\mu_{12}\), and every finite-order Hecke character of \(F\), the meromorphic continuation of \(L_F(s,\eta)\) has no zeros for \[ \Re s>1-10^{-6}. \] The principal pole is permitted. The numerical width is common to all fields and characters; intermediate constants and thresholds may depend on the fixed field and target. Do not extend this to arbitrary number fields or import the stronger \(7/8\) boundary for these cyclotomic families. The theorem statement, analytic outline, conductor-sieve lemma/proof and zero-detector statement were read, not the complete analytic argument or the primitive-root theorem's proof.

Related material found. The catalogue identifies prime-field polynomial factoring (family 142) and prime-polynomial-difference estimates (family 182) as applications of companion zero-free statements. These application pointers are part of the source inventory; their full results and proofs are not independently audited here. Catalogue hits for Riemannian geometry, the Riemann sphere and the Siegel threefold concern different objects and were excluded from this RH import.

Formalization scope and limits

The imported external scope note reports formalizations of the seven-eighths zeta, Dirichlet and Eisenstein Hecke conclusions and the logarithmic real-zero gap. Four comparator targets and JSON configurations map to separate solution modules. Comparator targets intentionally contain sorry; they are statement challenges, not proofs. Selected solution entry files were inspected and retained. The zeta and Dirichlet entry points invoke an unconditional detector assembly; the Hecke entry uses certified bands; the real-zero theorem invokes a separate arithmetic bound.

No Lean build, comparator replay or transitive axiom-closure check was run. The local snapshot deliberately contains selected entry and scope files, not a complete buildable Lean dependency tree. The Hecke target uses a custom residue-character model and a theta/lattice-defined function. The inspected entry does not by itself verify that this model covers every analytic finite-order Hecke character and agrees with its meromorphic \(L\)-function; that identification remains an explicit audit gate. Registry formalization status records only the statements inspected, with the external proof supply and the lack of local verification explicit. The totalized Lean zeta function's value at the meromorphic pole is an encoding convention; the analytic import permits a principal pole rather than treating its value as an analytic zero.

Dependencies, search and verification decision

Registry searches covered Riemann, quasi-Riemann, Siegel, zero-free and Dirichlet; no existing imported version of these four statements was identified. The immutable historical index was checked for the same number-theoretic source names. None of the earlier Frege/BMD survey mechanisms is used as a mathematical premise here. One refinement edge records only the common-family boundary implication between the two quasi-Riemann statements. Deep analytic and arithmetic inputs remain inside the retained sources, not silently replaced by trusted headlines.

Reviewer's suggestions, unverified

• For the October 5 alternative, audit its mean-square proof for arbitrarily small positive \(\vartheta,\varepsilon\) and the fixed smooth complex weight \(W(y)=y^{-\rho}\phi(y)\) chosen at a proposed zero \(\rho\). Fixed character- and weight-dependent constants suffice for that contradiction. Record. Searches for “mean-square Möbius” and “eleven-twelfths” found the imported thm:openai-eleven-twelfths-half-plane, whose stated mean-square proof remains unaudited, and the stronger but separately unaudited imported boundary. No prior local verification of the mean-square input was found. This is recorded as an audit suggestion, not a new theorem.

Suggestion check. The source proposition explicitly quantifies over all smooth weights on a fixed compact interval and arbitrarily small positive losses, with a finite derivative seminorm. The prescribed weight is smooth on that interval for fixed \(\rho\). The source's sixth-power estimate has squared exponent \(11/6+5\vartheta/6+\varepsilon\); sufficiently small losses give a pointwise exponent strictly below \(\Re\rho>11/12\). This confirms the proposed conditional deduction against the exact source reduction; it does not validate the indispensable mean-square estimate. The proposed next audit therefore targets an actually unverified source premise.

Verification gate. The sole fresh-context GPT-6.1-Sol reviewer at medium effort passed with one scope correction, incorporated here and in registry metadata: the custom Hecke character/function encoding needs an explicit analytic-identification audit. Its verdict confirms exact paper scopes and the formal boundary comparison, without certifying the complete proofs. Process audit. The reviewer found no additional issue in attribution, archival versus reading completeness, comparator placeholders, replay limits or timing. The final hash manifest preserves the reviewed snapshot; an earlier acquisition fingerprint is retained as such. Full mathematical correctness remains outside this source-scope pass.

Process assessment. Pulling main before selecting sources and reading the exact theorem statements prevents attaching the seven-eighths boundary to a different field or treating a comparator target as proof. Prevention. Existing source-refresh policy, explicit registry scope and the source-scope review apply; no new framework defect or preventive tool is claimed.

Timing scope. The initial checkout and notebook orientation reads preceded instrumentation; source acquisition, import, review and checkpoint work are measured.

Measured timing

11 October 2026 — Imported critical-line density and its rank–trace proof

Imported theorem; analytic verification remains open. Critical-line density import. Produced by Codex (gpt-6.1-sol, medium reasoning).

Cite as: Kamil Braun, “Imported critical-line density and its rank–trace proof”, OpenAI Math import, Noemesis research notebooks, 11 October 2026, https://kbr.is-a.dev/math-research/branches/openai-math-import/#entry-2026-10-11-anthropic-density-import.

Picked. The user requested: “Read also this, follow the refrrences, and import the density result and proof”, linking the Anthropic article.

Question. On side-rh-import, the missing implication is from a source-reported density theorem to an independently supported dependency with exact counting and analytic hypotheses. This task imports the theorem and complete licensed formal proof sources, reconstructs the elementary deduction, and follows the indispensable reference trail. A complete analytic audit or exact formal replay would end that verification test; source import alone does not.

New mathematics. No original number-theory result. The imported theorem and an elementary reconstruction of its existing Hermitian matrix inequality are recorded below. The number-theory conclusion is conditional here on the stated source analytic estimates, although the source asserts them unconditionally.

Goal progress. Unchanged for openai-rh-source-audit: the complete analytic estimates and formal dependency closure were not independently verified. The user-requested density/proof import is complete at source-retention and elementary-proof-reading scope. This is a density lower bound, not a proof that every zero lies on the line.

Sources and exact theorem

The canonical version read is Levent Alpöge and Ralph Furman, More than two thirds of the zeros of the Riemann zeta function are simple and on the critical line, Theorems A/B, arXiv version 2 of 19 August 2026. The argument is attributed to Claude, with human verification and responsibility attributed to the named authors; Jarred Sumner guided the investigation and Eric Easley orchestrated the Lean proof. The article's linked model manuscript and five-page expert note were also read. The expert note counts distinct on-line zeros; the longer paper states the stronger simple-on-line conclusion. The source-scope record separates versions, reading limits and audit points.

Imported statement. thm:anthropic-critical-line-density. Let \(N(T_1,T_2)=\sum_{T_1<\Im\rho\le T_2}m_\rho\) count nontrivial zeta zeros with multiplicity; \(S(T_1,T_2)\) counts distinct zeros with \(\Re\rho=1/2\) and \(m_\rho=1\), and \(D(T_1,T_2)\) counts all distinct nontrivial zeros. Put \[R_*={1\over2}+{1\over\sqrt2}\cot{1\over\sqrt2},\qquad C=2-R_*={3\over2}-{1\over\sqrt2}\cot{1\over\sqrt2}.\] The source states, without RH or a zero-density hypothesis, \[\liminf_{T\to\infty}{S(T,2T)\over N(T,2T)}\ge C=0.67250\ldots,\qquad \liminf_{T\to\infty}{D(T,2T)\over N(T,2T)}\ge{3-R_*\over2}=0.83625\ldots.\] The same bounds hold for \((0,T]\). A flat window gives the weaker exact constants \(2/3\) and \(5/6\). The denominator always counts multiplicity; neither bound asserts a matching upper bound or describes the remaining zeros. The paper's Dirichlet density theorem gives the same constants for each fixed primitive Dirichlet character; thresholds and error constants may depend on that character. No uniform conclusion with a growing conductor is imported. The analytic modulus-one primitive case is zeta; the formal wrappers separately assume \(q>1\), with modulus one covered by the zeta targets rather than a locally reviewed identity between counting functions.

Complete rank–trace argument

General statement. lem:hermitian-rank-trace is the all-dimensional algebraic ingredient, reconstructing source Lemma 3.2. For Hermitian matrices \(P\succeq0\) and \(Q\), with \(r=\operatorname{rank}P\) and \(n_+(Q)\le b\), \[r\ge2\operatorname{tr}P+4\operatorname{tr}Q-4b-\|P+Q\|_{\mathrm{HS}}^2.\] This uses ordered real eigenvalues and complex/real positivity, not finite-field rank.

Proof. Write \(Q=Q_+-H\), where both spectral parts are positive semidefinite and \(Q_+H=0\). Diagonalize \(P\) with nonzero eigenvalues \(p_1,\ldots,p_r\); let \(h_i\ge0\) be the diagonal entries of \(H\) in this basis. Dropping off-diagonal squares and then the remaining diagonal squares gives \[\|P-H\|_{\mathrm{HS}}^2\ge\sum_{i=1}^r(p_i-h_i)^2\ge2\operatorname{tr}P-r-2\sum_{i=1}^rh_i\ge2\operatorname{tr}P-r-4\operatorname{tr}H.\] The middle inequality is \((x-1)^2\ge0\); the last uses \(\sum_{i\le r}h_i\le\operatorname{tr}H\) and \(\operatorname{tr}H\ge0\). There are at most \(b\) strictly positive eigenvalues \(q_j\) of \(Q_+\), and \((q_j-2)^2\ge0\) implies \(\|Q_+\|_{\mathrm{HS}}^2\ge4\operatorname{tr}Q_+-4b\). Expanding, using \(\operatorname{tr}(PQ_+)\ge0\), yields \[\|P+Q\|_{\mathrm{HS}}^2=\|P-H\|_{\mathrm{HS}}^2+\|Q_+\|_{\mathrm{HS}}^2+2\operatorname{tr}(PQ_+)\ge2\operatorname{tr}P-r+4\operatorname{tr}Q-4b.\] Rearrange. This includes zero-rank and degenerate matrices. Equality is attained by \(P\) an orthogonal projection and \(Q\) twice a projection on an orthogonal subspace, so the inequality itself admits no universal improvement with these quantities.

Zero-side construction and analytic gate

Use \(z_\rho=(\rho-1/2)/i=\gamma-i(\beta-1/2)\), not just the real ordinate. Functional-equation partners at the same positive height are \(\rho\) and \(1-\bar\rho\), hence their \(z\)'s are conjugate. With \(L=\log(T/2\pi)\), let \(\psi\) be either the indicator on \([-1/2,1/2]\) or \(\cos(\sqrt2u)\) there, and smooth its square root at both endpoints: \[\phi(u)=\chi(L/2+u)\chi(L/2-u)\sqrt{\psi(u/L)},\quad a=L^{-1}\|\phi\|_2^2.\] Here \(\chi\) is smooth, zero on \(( -\infty,0]\) and one on \([1,\infty)\). Set \(\alpha_k=T+2\pi k/L\), \(d=\lfloor LT/(2\pi)\rfloor\), \(v_\rho=(\widehat\phi(z_\rho-\alpha_k))_{0\le k<d}\) and \(I'=[T-\sqrt T,2T+\sqrt T)\). Fourier normalization is \(\widehat f(z)=\int f(u)e^{-iuz}\,du\). Define \[G={1\over aL^2}\sum_{\gamma\in I'}m_\rho v_\rho v_\rho^{\mathsf T}.\] The transpose is deliberate. Off-line conjugate partners make the total real symmetric. On-line atoms are positive. An off-line pair with \(v=x+iy\) contributes \(2m(xx^{\mathsf T}-yy^{\mathsf T})/(aL^2)\), a pullback with positive index at most one; degeneracy can reduce that index.

Poisson summation at lattice step \(2\pi/L\), with support of the convolution in \([-L,L]\) and vanishing endpoint modes, gives \[\sum_{k\in\mathbb Z}\widehat\phi(z-\alpha_k)\widehat\phi(z'-\alpha_k)=L\widehat{\phi^2}(z-z').\] At equal real arguments this is \(aL^2\), so a truncated simple on-line atom has trace at most one. Let \(P_1\) sum those simple atoms and put \(Q'=G-P_1\). If \(s_1,s_2,p\) count simple on-line points, multiple on-line points and off-line pairs in \(I'\), respectively, then \[\operatorname{rank}P_1\le s_1,\quad\operatorname{tr}P_1\le s_1,\quad n_+(Q')\le s_2+p,\quad s_1+2s_2+2p\le N(I').\] The last inequality retains every multiplicity; summing pullbacks bounds positive index without any positivity of the off-line zero kernel.

Analytic premises. The source's Propositions 4.2/4.3 and Theorem 5.7 assert \[N(I')=N(T,2T)+o(N),\quad\operatorname{tr}G=N+o(N),\quad \|G\|_{\mathrm{HS}}^2=(R(\psi)+o(1))N,\] where \[R(\psi)={\int\psi^2+\iint|u-v|\psi(u)\psi(v)\,du\,dv\over(\int\psi)^2}.\] Endpoint discrepancies are \(O(\sqrt T\log T)=o(N)\). These are the outstanding independent analytic gate; the following conclusion is proved from them, not from an assumed RH.

Deduction. Apply the matrix inequality to \(P_1,Q'\), using \(\operatorname{tr}P_1+2n_+(Q')\le N(I')\): \[s_1\ge4\operatorname{tr}G-2N(I')-\|G\|_{\mathrm{HS}}^2=(2-R(\psi)-o(1))N.\] The same inequality, with \(\operatorname{tr}P_1\le s_1\), gives \(3s_1+4(s_2+p)\ge(4-R(\psi)-o(1))N\). Subtract \(s_1+2(s_2+p)\le N(I')=N+o(N)\) to obtain \(2(s_1+s_2+p)\ge(3-R(\psi)-o(1))N\). Since \(D(I')=s_1+s_2+2p\), deleting endpoint points proves the distinct-zero bound. For cumulative counts, fix an error tolerance, sum over dyadic blocks whose lower endpoints exceed its fixed threshold, and discard the bounded initial block; Riemann–von Mangoldt makes its relative contribution vanish.

Window evaluation. For the flat window, \(\int\psi^2=\int\psi=1\) and \(\iint|u-v|=1/3\), hence \(R=4/3\). For the cosine window, \(H(u)=\psi(u)+\int|u-v|\psi(v)\,dv\) satisfies \(H''=\psi''+2\psi=0\) in the interval and is even, hence constant. Direct integration gives \(H(0)=\cos(1/\sqrt2)+(1/\sqrt2)\sin(1/\sqrt2)\), while \(\int\psi=\sqrt2\sin(1/\sqrt2)\). Integrating \(H\psi\) gives \(R=H(0)/\int\psi=R_*\), proving the exact constants from the analytic premises.

Prime-side proof mechanism and references

The complete supplied Lean proof is retained in the project snapshot. In the prose proof, Weil's explicit formula expresses \(G+E\) as an integral against the archimedean density, pole term and prime polynomial. The completed grid kernel is \(L\widehat{\phi^2}(\tau-\tau')\). Its square gives an archimedean diagonal term proportional to \(\int\psi^2\) and a prime diagonal term proportional to \(2\int_0^1w(\psi*\psi)(w)\,dw=\iint|u-v|\psi\psi\). Partial summation uses \(\sum_{n\le x}\Lambda(n)^2/n=\tfrac12\log^2x+O(\log x)\); the off-diagonal prime terms use the bilinear Montgomery–Vaughan inequality with frequency gaps \(\log n-\log m\). Endpoint smoothing controls the far-zero tail. This identifies exactly what must be audited to justify the two moment premises; the elementary proof above does not independently prove those error estimates.

• Farzad Aryan, On an extension of the Landau–Gonek formula, Theorem 1.3 and Corollary 1.4: an unconditional complex-zero Fejér second moment. Its Corollary 1.5 still assumes a zero-density hypothesis with logarithmic exponent greater than four for the two-thirds simplicity deduction. That conditional conclusion is not substituted for the new theorem.
• Baluyot–Goldston–Suriajaya–Turnage-Butterbaugh, An unconditional Montgomery theorem: complex-zero form-factor evaluation and its explicit-formula mean-square mechanism. Their nonnegative integrated representation does not make each complex zero-difference term positive.
• The same authors, Pair correlation I, Theorems 1–3: narrow-box hypotheses give simple-critical density, including two-thirds when the scaled width tends to zero. The fixed-width refinements preserve their all-zeros-in-the-box assumption. The new inertia argument is meant to remove that positivity gate.
• Enrico Bombieri, Remarks on Weil's quadratic functional I (2000): Theorem 1 is the positivity/RH criterion; Theorems 10/11 assume finitely many off-line exceptions. Those finite-exception results are not unconditional density inputs. The required finite pullback bound was proved directly above. HTTPS retrieval failed certificate verification; the library's public HTTP PDF succeeded.

Prose audit points. In the current paper's section 2.2, the assertion \(d=N(T,2T)+O(L)\) conflicts with its own displayed counting formula: \(d-N=-(2\log2-1)T/(2\pi)+O(L)\). The usable statement is \(d\sim N\). Equation (5.2)'s lower indicator sandwich also fails for the cosine window, whose bulk square is below one. The weighted convolution/partial-summation calculation, rather than that flat-window sandwich, is the appropriate stated route for the optimized constant. These observations do not refute the density theorem; they prevent certification of every prose estimate by this import. Other localization and cross-term estimates remain unaudited. The expert note's terse estimates are not substituted for the complete source proof.

Formal scope, retention and verification

The entire Apache-2.0 project was copied unchanged, with LICENSE and NOTICE and its attributed PrimeNumberTheoremAnd-derived files. Mathlib and other Lake dependencies are pinned but not vendored. The trusted challenge defines counts directly from Mathlib's riemannZeta and LFunction, and contains seventeen intentional placeholder targets; Solution.lean supplies their proofs from the full tree. No local build, comparator run or transitive axiom check was executed. Upstream AUDIT reports earlier build/replay success and only standard axioms; its latest layout note explicitly says that layout revision had no complete fresh build. These reports are provenance, not our replay. A separate bandwidth-ceiling calculation has a numeric enclosure premise; it is not a premise of the headline density statements.

The papers and full-text conversions are retained as ignored personal copies because public redistribution permission was not established. The licensed Lean sources, original proof reconstruction, source scope and hash manifest are committed. Source authorship and theorem verification status remain separate. Registry searches for zeta density critical simple, Hermitian rank trace inertia and positive index Hilbert Schmidt, plus the historical index, found no matching local number-theory theorem. Related finite-field rank work is not used as a premise or asserted as an application.

Review. The preceding stand-in objections were checked: custom Hecke scope was corrected and its encoding-audit build remains queued; the earlier import's files were preserved byte-for-byte through rewritten commits despite the older branch no longer existing; claims that timing/searches were absent and that the related fourth manuscript or license was concealed were contradicted by retained evidence. No lost-work cause or new framework implementation is asserted.

Reviewer's suggestions, unverified

• Audit each analytic use of the source assertion \(d-N=O(L)\) against the correct \(O(T)\) discrepancy. An additive \(O(T)=O(N/L)\) error is acceptable, but a larger multiplier needs a separate repair. Record. Searches for dimension normalization trace moment and Hermitian rank trace inertia found no matching verified number-theory estimate; thm:anthropic-critical-line-density retains this analytic gate, not a repair.

Suggestion check. Direct subtraction of the displayed counting formula from the defined grid size gives the discrepancy recorded above, and \(N\sim TL/(2\pi)\) implies \(T=O(N/L)\). Thus the proposed audit distinguishes harmless additive errors from uses amplified beyond the required moment budget. No assertion that all downstream uses pass this test is made. This verified sizing comparison supports the proposed next analytic audit.

Verification gate. The sole fresh-context GPT-6.1-Sol reviewer at medium effort passed with two precision corrections, incorporated here: cumulative intervals are \((0,T]\), and the formal Dirichlet wrappers require \(q>1\), with separate zeta targets for modulus one. The reviewer found no substantive gap in the all-dimensional matrix proof, multiplicity deductions, cumulative transfer or window evaluation. Its verdict does not certify the full analytic estimates or formal closure. Process audit. No findings beyond those interval and formal-scope clarifications; conditional status and unchanged goal assessment were accepted.

Process assessment. The result's asymptotic density and multiplicity convention were read before import. No dependency installation or Spin was started. Prevention. Existing source-reading, attribution, review and explicit analytic-gate rules apply; no agent error requiring a new framework change has been identified in this cycle.