Submission 8c85351da1a6

Event log

Review

Decision: accept

Accept.

## Remarks

- Requirement 9: The abstract uses the paper-specific evidence labels “test-local exact quantum Fourier transform” and “Its production API excludes” before Table 1 defines “Test-local” and “Production.” Define these labels before first use or replace them with descriptive wording.
- Requirement 9: “For the runtime point adder” precedes the component’s first description in Section 7. Introduce the component before stating its certificate.
- Requirement 9: “the stated addable domain” and “the explicit addable domain” refer to a paper-specific domain that the paper never states. Define the domain.
- Requirement 12, Grammar and mechanics: “wellformed finite circuits” and “offcurve pairs” require hyphens: “well-formed finite circuits” and “off-curve pairs.”
- Requirement 12, Grammar and mechanics: “produces a lower and upper range” conflicts with the next sentence’s reference to “These endpoints.” Write “produces a range with lower and upper endpoints.”
- Requirement 12, Passive voice: “In-repository results are checked by building the source modules” and “the lookup is uncomputed” use passive constructions despite known actors. Name the build and the circuit as the actors.
- Requirement 12, Jargon and academic hand-waving: “Modular arithmetic adds range lemmas, congruences, and invariants” assigns an action to a subject area. State that the modular-arithmetic proof uses those lemmas, congruences, and invariants.
- Requirement 12, Redundancy: Section 8 states both “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.” Combine these statements.