[antonkov]

Change

Part of #1226 (building on #1305, #1306, and #1311). Formalizes the uniform native heavy-branched sparse $\mathbb{F}_2$ polynomial-system common-zero counter of §5.5 (Proof of Theorem 2.2, printed pp. 38–39) and its context-carrying §6.3 parity-system wrapper (printed p. 43) from [OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH] (pinned revision 7ef5c0cc) in Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean, parameterized cleanly over a supplied Proposition 5.3 bounded-incidence branch evaluator (BranchEvalInput → ℕ with its Cslib.GenericRAM.NativeCertificate time and polynomial-space contract) and guarded by exact integer parameter checks (Cslib.Complexity.SubexponentialSAT.ParameterCheck) and streaming $2^n$ exhaustive fallbacks (Cslib.GenericRAM.ExhaustiveCountFallback) so that the combined counter is unconditionally exact on all inputs while preserving independent polynomial working space.

Source statements ([OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH], printed pp. 20–21, 38–39)

(Mathematical-transcription note: Plain-text extraction from the source PDF flattens rendered blackboard/bold field symbols, superscripts, subscripts, primes, ceiling and floor brackets, square roots, and summation signs—including $\mathbb{F}2$, $m{\mathrm{test}}$, $2^{O_{k,c}(n(\log \log n)^2 / \sqrt{\log n})}$, $M = \sum_{f \in F} |I_f|$, $b_0 = \lceil M / n \rceil \lceil \sqrt{\lambda} \rceil$, $2^{n / \sqrt{\lambda}}$, $I'_f$, $M' = \sum_f |I'_f|$, $r = \lfloor \sqrt{\lambda'} / (\nu')^2 \rfloor$, $Q = \lfloor \lambda' / (128 \nu') \rfloor$, and $R = (\beta + 3)\lceil \sqrt{\lambda'} \rceil$; in the separate contiguous source passages below, all mathematical symbols, brackets, superscripts, subscripts, and displayed equations are restored to match rendered printed pages 20–21 and 38–39.)

• §2.9, Theorem 2.2, printed pp. 20–21:

  Theorem 2.2 (Counting common zeros of sparse polynomials). Fix integers $k \geqslant 2$ and $c \geqslant 1$. Let $P_1, \ldots, P_{m_{\mathrm{test}}}$ be polynomials over $\mathbb{F}2$ in $n \geqslant 20$ Boolean variables, with $m{\mathrm{test}} \leqslant cn$. Each $P_i$ is given as a list of at most $(\log n)^c$ monomials of degree at most $k$. The exact number of common zeros in ${0, 1}^n$ can be computed deterministically in $2^{O_{k,c}(n(\log \log n)^2 / \sqrt{\log n})}$ bit operations and $n^{O_{k,c}(1)}$ space.

• §5.5, Constructing the forms and completing the proof (Proof of Theorem 2.2, heavy-variable branching and restricted scopes), printed p. 38:

  5.5. Constructing the forms and completing the proof. Each sparse polynomial reads few variables, but one variable might occur in many equations. We first fix the values of the few variables with the largest numbers of occurrences. On each resulting branch we can construct the design required by Proposition 5.3.

  Proof of Theorem 2.2. Let $P$ be the supplied polynomial system. An empty list of equations gives $2^n$ common zeros; a constant equation $1 = 0$ gives none. Discard equations $0 = 0$. Include a neutral factor equal to one with scope ${v}$ for each declared variable $v$, and write
  $$M = \sum_{f \in F} |I_f|$$
  for the total number of factor–variable incidences. The input bounds imply $M = n(\log n)^{O_{k,c}(1)}$, and every scope has $(\log n)^{O_{k,c}(1)}$ variables. A particular variable, however, may occur in many of these scopes.

  Put $\lambda = \lceil \log_2 n \rceil$ and
  $$b_0 = \left\lceil \frac{M}{n} \right\rceil \lceil \sqrt{\lambda} \rceil.$$
  Let $S \subseteq [n]$ be the variables belonging to more than $b_0$ scopes. For each $b \in {0, 1}^S$, we fix $x|_S = b$ and count the completions on $[n] \setminus S$; we call this restricted problem a branch. Since $|S| \leqslant M / b_0 \leqslant n / \sqrt{\lambda}$, there are at most $2^{n / \sqrt{\lambda}}$ branches. Each branch has the same number $n'$ of free variables, with
  $$n' \geqslant n - \frac{n}{\sqrt{\lambda}} \geqslant \frac{n}{2} \qquad (n \geqslant 20).$$
  Substitute the fixed bits in every $P_i$ over $\mathbb{F}_2$ and combine duplicate monomials modulo two before forming its integer lift. Neither degree nor the number of monomials increases. A constant equation can again be handled immediately. The branches partition the Boolean cube, so their common-zero counts add to $N(P)$.

• §5.5, Proof of Theorem 2.2 (per-branch schedule parameters, integer feasibility checks, exhaustive fallback, and streaming space), printed pp. 38–39:

  To apply Section 4, remove the fixed variables from the scopes and relabel the free variables by $[n']$. Write $I'_f \subseteq [n']$ for the restricted scopes and $M' = \sum_f |I'_f|$ for their total incidence count. Let $b$ be the maximum factor incidence of a free variable and let $w = \max_f |I'_f|$. Then $b \leqslant b_0$, and both $b$ and $w$ are bounded by a fixed power of $\log n'$. The remaining neutral factors ensure $M' \geqslant n'$. Set
  $$\lambda' = \lceil \log_2 n' \rceil, \qquad \nu' = \lceil \log_2 \lambda' \rceil,$$
  and choose the smallest integer $\beta \geqslant 1$ with $b, w \leqslant (\lambda')^\beta$. For fixed $k, c$, the possible values of $\beta$ are bounded by a constant for all sufficiently large $n$. We apply Lemma 4.8 to the restricted scopes $(I'f)$ on $[n']$, with incidence count $M'$, using
  $$r = \left\lfloor \frac{\sqrt{\lambda'}}{(\nu')^2} \right\rfloor, \qquad Q = \left\lfloor \frac{\lambda'}{128 \nu'} \right\rfloor, \qquad R = (\beta + 3)\lceil \sqrt{\lambda'} \rceil.$$
  If $r < 2$ or $Q \leqslant R$, use the exhaustive-search fallback below before forming $\tau$, $\epsilon$, or the parity interpolation interval $I$. Otherwise set
  $$\tau = \frac{1}{r \lambda'}, \qquad \epsilon = \frac{1}{b r^2 \lambda'}, \qquad D = r^{2Q},$$
  and carry out the remaining feasibility checks from that lemma. For all sufficiently large $n$, Lemma 4.7 supplies the required rows and measurement matrices, with
  $$r = \Theta\left(\frac{\sqrt{\log n'}}{(\log \log n')^2}\right), \qquad Q = \Theta\left(\frac{\log n'}{\log \log n'}\right), \qquad R = O{k,c}(\sqrt{\log n'}), \qquad D \leqslant (2n')^{1/128}.$$

  On every branch we may use the original precision $\ell = n + 1$, since even the unrestricted count is smaller than $2^\ell$. As $n' \geqslant n/2$, both $\ell$ and $m_{\mathrm{test}}$ are $O_c(n')$. Thus $d_H = O_{k,c}(n' R)$, $J = O_{k,c}(n' R / Q) + 1$, and (3.16), in dimension $n'$, has exponent
  $$O_{k,c}\left(\frac{n' (\log \log n')^2}{\sqrt{\log n'}}\right) = O_{k,c}\left(\frac{n (\log \log n)^2}{\sqrt{\log n}}\right).$$
  All substitution data, coefficient arrays, and interpolation systems have total representation length $n^{O_{k,c}(1)}$ bits. Multiplying the per-branch running time by at most $2^{n / \sqrt{\lambda}}$ leaves the displayed exponential bound unchanged, so summing the branch answers gives the required running time.

  To implement the construction for every input size, the algorithm checks its numerical hypotheses using integer arithmetic. In addition to the preliminary guards above, it checks $2(b + w)D^2 \leqslant M'$ and $2Qr^2 \leqslant n'$ from Lemma 4.5, the endpoints of $I$, $R \geqslant 32$, $6R \leqslant Q$, and the binomial tail bound in (4.8), which can be tested exactly. If any check fails, the algorithm abandons the branched computation and checks the original equations directly on all $2^n$ assignments. For fixed $k, c$, the bounds just proved and Lemma 4.8 show that a failure can occur only for finitely many $n$. This fallback is therefore absorbed in the theorem's constants.

  To combine the branch counts within the stated space bound, we process the branches one at a time. We initialize an integer accumulator $Z = 0$ and add each branch's answer to it. The construction and Proposition 5.3 use $n^{O_{k,c}(1)}$ bits of space on each branch. Disjointness gives $0 \leqslant Z \leqslant 2^n$ throughout, and the final value is $N(P)$, as claimed.

Source-to-Lean mapping (Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean)

1. Per-branch neutral-augmented scope invariants, exact schedule guard, and ReplacementDesign bridge:
   • Defines executable well-formedness and neutral-augmented scope metrics (checkVarsLt, checkCanonicalMonomial, checkCanonicalEquation, checkCanonicalSystem, scopeWidthOn, sysMaxDegree, branchMaxFactorIncidence, branchMaxFactorWidth, branchAugmentedIncidence), all certified under plain Turing.MultiTapeTM.ComputableInPolyTime (@[fun_prop]).
   • Connects the list-level metrics to the neutral-augmented scope family branchNeutralScope via sum_card_branchNeutralScope, varIncidence_branchNeutralScope_le, card_branchNeutralScope_le, and branchAugmentedIncidence_le_mul.
   • Defines BranchEvalInput, encBranchEvalInput, prepareBranchEvalInput, checkBranchFeasible, and guardedBranchSolver, proving schedule soundness (feasible_of_checkBranchFeasible), concrete Section 4 Cslib.LinearAlgebra.ReplacementDesign existence (exists_replacementDesign_of_checkBranchFeasible), the cleared parity-polynomial specialization bridge (emod_ediv_design_eq_rootCount_of_checkBranchFeasible), and uniform eventual passage across $1 \le \beta \le \beta_0$ (exists_threshold_checkBranchFeasible_eq_true).
2. Uniform top-level heavy-branched sparse $\mathbb{F}_2$ counter and semantic exactness:
   • Defines SparseSystemInput, encSparseSystemInput, mkPaperSparseInput (instantiating $s_{\mathrm{div}} = \lceil \sqrt{\lambda} \rceil$ and $b_0 = \lceil M / n \rceil \lceil \sqrt{\lambda} \rceil$ via ParameterCheck.heavyIncidenceCutoff), checkTopFeasible, toBranchInput, and countSparsePolySystem (dispatching HeavyBranchFold.countByBranching over guardedBranchSolver when checkTopFeasible holds and ExhaustiveCountFallback.countSystemExhaustive otherwise).
   • Proves unconditional agreement between ExhaustiveCountFallback.countSystemExhaustive and HeavyBranchFold.rootCount (countSystemExhaustive_eq_rootCount), unconditional pointwise exactness (guardedBranchSolver_eq_rootCount, countSparsePolySystem_eq_rootCount, countSparsePolySystem_le_two_pow), and the canonical bridge to Cslib.BitString.commonZeroCount on Fin n (countSparsePolySystem_eq_commonZeroCount), alongside Markov heavy-variable bound discharge (length_heavyVarList_le_div_of_incidence), automatic feasibility of mkPaperSparseInput for $n \ge \max(N_0, 2)$ (checkTopFeasible_mkPaperSparseInput_of_le), reduced-branch invariants (reduced_branch_invariants), and polylogarithmic degree transfer (clog_pow_le_clog_pow_two_mul).
3. Native time and independent polynomial-workspace certificates:
   • Constructs guardedBranchCertificate, maxReducedCost, guardedBranchingCertificate, and sparsePolyCounterCertificate, proving independent polynomial workspace preservation (polyBounded_guardedBranchCertificate_space, polyBounded_sparsePolyCounterCertificate_space), per-branch finite-threshold fallback absorption (exists_guardedBranchCertificate_time_le), the feasible-regime $(2^{|S|} + 1) \cdot (\operatorname{poly} + R_{\mathrm{branch}})$ multi-branch runtime bound (sparsePolyCounterCertificate_time_le_of_feasible), and real-exponent $O((|\operatorname{enc}(x)| + 1)^e \cdot \lceil 2^{E(x)} \rceil)$ family absorption (exists_real_exp_bound_countSparsePolySystem).
4. Context-carrying §6.3 CNF parity-system wrapper:
   • Defines compileContextParityInput, countContextParity, and contextParityCertificate over encPair encC (encList encBits) via Cslib.Complexity.compileParitySystemBounded, proving polynomial workspace preservation (polyBounded_contextParityCertificate_space), compositional compatibility with Cslib.Logic.PL.CNF.GreedyContext.greedyCertificate, and unconditional agreement with Cslib.BitString.numPassing (countContextParity_eq_numPassing).

Deviations / Non-claims

• Scope covers the §5.5 heavy-branched sparse $\mathbb{F}_2$ polynomial-system zero counter and its §6.3 context-carrying parity-system wrapper, parameterized over a supplied Proposition 5.3 bounded-incidence branch evaluator (branchEval : BranchEvalInput → ℕ); the internal Proposition 5.3 / §5.4 truncated-parity Taylor-interpolation branch evaluator itself and the final §6.3–6.4 #k-SAT assembly belong to sibling and downstream slices of Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226.

• In §5.5 (p. 38), neutral singleton factors ${v}$ increase each free variable's restricted factor incidence by $1$, so branchMaxFactorIncidence computes $b = \max_{v &lt; n'} \operatorname{varDegree}(v, \mathrm{eqs}') + 1 \le b_0 + 1$ (matching ReplacementParams.varIncidence_branchAugmentedScope_le). On reduced branches where checkBranchFeasible fails, guardedBranchSolver falls back per branch to ExhaustiveCountFallback.countSystemExhaustive on the $n'$-variable reduced system (absorbed identically into polynomial overhead once $n' &lt; N_1$, while top-level guard failures fall back directly to $2^n$ exhaustive search on the original $n$-variable system).

• emod_ediv_design_eq_rootCount_of_checkBranchFeasible parameterizes the modular precision by an arbitrary $\ell &gt; n'$, so downstream Proposition 5.3 and §5.5 callers can instantiate either Proposition 5.3's per-branch precision $\ell = n' + 1$ (printed p. 37) or §5.5's shared precision $\ell = n + 1$ when $n' \le n$ (printed p. 39).

• Existing notions considered:

  • Cslib.BitString.commonZeroCount, Cslib.BitString.withNeutralFactors, Cslib.BitString.withNeutralScope, Cslib.BitString.withNeutralFactors_univ, Cslib.BitString.card_withNeutralScope_le, Cslib.BitString.totalIncidence_withNeutralFactors_le, Cslib.BitString.emod_ediv_eval_zero_clearedParityTruncatedSum_design_eq_commonZeroCount (Complexity/Foundations/BooleanAnalysis/SparseReplacementDesign.lean), and Cslib.Complexity.SubexponentialSAT.ReplacementParams.branchAugmentedScope (Complexity/Computability/Complexity/FineGrained/SparseBranchSchedule.lean): provide the noncomputable Finset-based neutral scope augmentation, neutral incidence bounds, and cleared parity-polynomial zero-counting theorems; branchNeutralScope specializes withNeutralScope directly to Fin eqs'.length ⊕ Fin n' over HeavyBranchFold.toFinsetEquation, while the executable list metrics (scopeWidthOn, sysMaxDegree, branchMaxFactorIncidence, branchMaxFactorWidth, branchAugmentedIncidence) and checkers (checkVarsLt, checkCanonicalMonomial, checkCanonicalEquation, checkCanonicalSystem) compute the corresponding quantities and well-formedness guards on encoded List (List (List ℕ)) inputs in ComputableInPolyTime.
  • Cslib.Complexity.SubexponentialSAT.ParameterCheck.heavyIncidenceCutoff, Cslib.Complexity.SubexponentialSAT.ParameterCheck.chooseBeta, Cslib.Complexity.SubexponentialSAT.ParameterCheck.computeScheduleParams, and Cslib.Complexity.SubexponentialSAT.ParameterCheck.checkScheduleFeasible (Complexity/Computability/PolyTime/FineGrained/ParameterCheck.lean, feat(PolyTime/FineGrained): add polytime parameter schedule and exact feasibility checks #1305): reused directly inside prepareBranchEvalInput, checkBranchFeasible, and mkPaperSparseInput to select $\beta$, compute $(r, Q, R, A_0)$, compute $b_0$, and decide Lemma 4.7–4.8 schedule feasibility (BranchEvalInput, encBranchEvalInput, SparseSystemInput, and encSparseSystemInput package the exact unary/binary native encodings connecting the top-level driver to the Proposition 5.3 branch evaluator).
  • Cslib.GenericRAM.HeavyBranchFold.heavyVarList, Cslib.GenericRAM.HeavyBranchFold.prepareBranch, Cslib.GenericRAM.HeavyBranchFold.BranchInput, Cslib.GenericRAM.HeavyBranchFold.countByBranching, and Cslib.GenericRAM.HeavyBranchFold.countByBranching_computableInO (Complexity/Computability/GenericRAM/Native/HeavyBranchFold.lean, feat(GenericRAM/Native): add heavy-variable branch fold and sparse polynomial substitution #1306), together with Cslib.GenericRAM.ExhaustiveCountFallback.countSystemExhaustive, Cslib.GenericRAM.ExhaustiveCountFallback.guardedBranchOfPolyTime, and Cslib.GenericRAM.ExhaustiveCountFallback.exists_real_exp_bound_of_guarded_fallback (Complexity/Computability/GenericRAM/Native/ExhaustiveCountFallback.lean, feat(GenericRAM/Native): add streaming exhaustive counting fallbacks and guard absorption #1311): reused directly by toBranchInput, checkTopFeasible, guardedBranchSolver, guardedBranchCertificate, maxReducedCost, guardedBranchingCertificate, countSparsePolySystem, and sparsePolyCounterCertificate without duplicating BooleanFold streaming or exhaustive evaluation.
  • Cslib.Complexity.compileParitySystemBounded (Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean), Cslib.BitString.numPassing (Complexity/Logics/Propositional/CNF/ParityTests.lean), and Cslib.Logic.PL.CNF.GreedyContext.greedyCertificate (Complexity/Computability/PolyTime/CNF/GreedyParityContext.lean): reused directly by compileContextParityInput, countContextParity, and contextParityCertificate to package the (ctx, rows) ↦ ℕ counter interface required by §6.3 greedy parity-row selection.

Validation and review

• Tested revision: 1e1fc67e900d400eda81e23495b9ce921df35def
• Verification commands run locally:
  • LEAN_NUM_THREADS=4 lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts (passed, 0 warnings)
  • LEAN_NUM_THREADS=4 lake exe runLinter Complexity.Computability.PolyTime.BooleanAnalysis.SparsePolyCounter ComplexityTests.SparsePolyCounter (passed)
  • LEAN_NUM_THREADS=4 lake exe mk_all --check (passed)
  • LEAN_NUM_THREADS=4 lake exe lint-style (passed)
  • LEAN_NUM_THREADS=4 lake exe checkInitImports (passed)
  • python3 scripts/check_hygiene.py --check-simp (passed)
  • python3 scripts/check_tidy_surface.py (passed, zero new public ComputableTidilyInPolyTime declarations)
  • python3 scripts/check_changed_files.py (passed)
  • python3 scripts/parallel_defs.py (passed, 0/28 advisories)
  • python3 scripts/audit_queries.py duplicates Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean (passed, 0 matches)
  • python3 -B scripts/build_abstracts.py --check (passed)
  • python3 scripts/check_pr_names.py --strict (passed)
• Concrete nonvacuity coverage in ComplexityTests/SparsePolyCounter.lean: empty systems ($2^n$, including $n = 0$), tautology $[[]] = 2^3$, and contradiction $[[[]]] = 0$ across both branched and fallback thresholds; single-equation and multi-equation 4- and 5-variable sparse $\mathbb{F}_2$ systems with nonempty heavyVarList exercising BranchOutcome.tautology, BranchOutcome.contradiction, and BranchOutcome.reduced branch compaction against a poison branch oracle (poisonBranchEval returning 999999 if ever invoked on $n' &lt; 20$) and instantiating countSparsePolySystem_eq_commonZeroCount; mkPaperSparseInput and neutral-augmented scope metric checks; fallback boundary tests for small $n$, excess heavy variables, unsorted/duplicate non-canonical equations, and out-of-range variable indices; countContextParity_eq_numPassing on a 3-variable CNF parity system; and compositional fun_prop, polyBounded_sparsePolyCounterCertificate_space, contextParityCertificate, and GreedyContext.greedyCertificate synthesis checks.
• Independent pre-PR mathematical and manuscript-fidelity review: independently reviewed by a separate non-author session across mathematical fidelity against [OpenAI2026ETH] (§2.9 Theorem 2.2 pp. 20–21, §5.5 pp. 38–39, §6.3 p. 43), native Turing.MultiTapeTM.PolyBounded workspace and fallback-absorbed runtime contracts, API reuse, and full 6-gate scripts/check.sh validation.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: Unaffected. This PR adds Complexity.Computability.PolyTime.BooleanAnalysis.SparsePolyCounter and ComplexityTests.SparsePolyCounter toward Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226 without modifying any declaration or statement in abstracts/catalogue.json. Verified with python3 -B scripts/build_abstracts.py --check.
• Independent abstract review (reviewer, exact source revision, findings/resolutions): Not applicable (no abstract or abstracts/catalogue.json entry changed).
• PDF artifact/run and source/PR-head revisions; rendered-page and declaration-link checks: Not applicable (no abstract or rendering changed).

AI assistance

AI-assisted (Gemini) under human direction (@antonkov); all Lean proofs and concrete test instances were mechanically checked by Lean 4.

[SamuelSchlesinger]

Coordinator coordinator-codex-01a16ab8: claiming independent outside review at 1e1fc67e900d400eda81e23495b9ce921df35def, using a nonauthor math/API reader plus coordinator native-resource/integration coverage. We will reuse the existing supplier reviews and hosted validation; no duplicate broad build. Please link the stated pre-PR review with its exact revision and coverage if that evidence is not yet public, so unchanged coverage can be adopted. The conditional supplier interface and remaining unconditional #1226 assembly will be checked explicitly; this claim does not approve an endpoint.

[SamuelSchlesinger]

coordinator-codex-01a16ab8 — FINAL APPROVED at 1e1fc67e900d400eda81e23495b9ce921df35def. Separate nonauthor mathematics review plus coordinator resource review found no blocker: canonical restriction/cancellation, neutral incidence b₀ + 1, declared-variable counts, uniform certificates, independent workspace, and bounded-size fallback absorption are sound under the displayed callback premises. The pinned §5.5 mapping was checked. No duplicate Lean build.

This is a conditional supplier: feasible-branch evaluator correctness/time and the family’s fast-regime bound still need the concrete Proposition 5.3 assembly. Small concrete tests exercise exhaustive fallback and meaningful heavy-branch outcomes; they do not demonstrate a correct fast evaluator. Independent truth-table checks reproduced their counts.

Exact hosted CI passes all six gates, ratchet and changed-file checks; title passes. Fresh head matches, main target, non-draft and MERGEABLE/CLEAN. Shared handoff already carries readiness; no duplicate queue request.

Nonblocking wording follow-ups remain: qualify “unconditional exactness” by the supplied evaluator assumption, and call the generic E ≥ 0 absorption theorem “real-exponent” rather than “subexponential.”

[SamuelSchlesinger]

Nonblocking wording: this is real-exponent constant absorption; E is only nonnegative, with no sublinear-growth premise. The eventual client can specialize it to the subexponential exponent. Dropping “Subexponential” here would match the theorem’s general scope.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): exact-head validation is complete at 1e1fc67e900d400eda81e23495b9ce921df35def: CI40471567520 passes all six gates, ratchet and changed-file checks; title passes. The independent source/API/resource approval covers this unchanged head. Queue-ready subject to fresh preflight, preserving that review’s conditional-evaluator scope. I am carrying the readiness record in the single shared packet; no duplicate audit or queue mutation.