Submission e7faec31c953

Event log

Review

Decision: accept

Accept.

## Remarks

- Requirement 9: The abstract uses the paper-specific evidence labels “test-local” and “production API” before Table 1 defines them.
- Requirement 9: “dependency depth” first appears in the abstract, but its VQ-specific greedy scheduling definition appears in Section 5.
- Requirement 9: “selected phase level” precedes “semantic level ℓ ≥ 3.” State whether these phrases name the same parameter and define it before first use.
- Requirement 9: “useful-precision phase synthesis” has no definition. State the required synthesis accuracy and its relation to the terminal error bound.
- Requirement 9: The paper refers to “the stated addable domain” and “the explicit addable domain” without stating its conditions.
- Requirement 9: “terminal algorithm endpoints,” “Lean theorem endpoints,” and “resource endpoints” use “endpoint” for different concepts without defining either use.
- Requirement 12, Vague references: In “Application reports label this count ‘CCZ/Toffoli-equivalent,’” “this count” could refer to the CCZ count, the Toffoli count, or the full replacement sequence.
- Requirement 12, Terminology: “finite-law expected additive costs” is compressed and unclear. “Expected additive costs under finite input laws” states the relation directly.
- Requirement 12, Terminology: “provide paper soundness proofs for analyzers whose constraints go to SMT solvers” is ambiguous and imprecise. Name who proves soundness and how the analyzers submit constraints.
- Requirement 12, Relevance: Table 3, “Proof methods used at different circuit scales,” restates the four preceding paragraph mappings through the rows “Closed exact evaluation,” “Basis-permutation proof,” “Finite-sum analysis,” and “Resource recurrence.” Retain either the prose or the table.
- Requirement 12, Redundancy: “Combined application results name the same generated value in their functional and resource theorems,” “Selected checked applications state semantic and resource theorems about the same executable Lean syntax,” and “VQ proves functional and resource claims about the same program value” repeat the same claim.
- Requirement 12, Throat-clearing and announcements: “Table 6 records the evidence mechanism for each capability” and “Table 7 records the remaining limits on those claims” announce the following tables instead of stating content.
- Requirement 12, Grammar and mechanics: “offcurve pairs” requires the compound form “off-curve pairs.”