Submission 5cb2754fb77b

Event log

Review

Decision: accept
Classification (automatic): Logic in Computer Science (cs.LO)

Accepted.

## Remarks

- Requirement 9: “an exact 2n-round termination bound” uses `n` without defining it. The map “|x, y⟩ ↦ |x, xy mod q⟩” introduces `x`, `y`, and `q` before stating their domains.
- Requirement 9: “Its width is 4n + 5B + 5 + max(n + 5, wa + 1)” leaves `wa` undefined, and “at w = 16” leaves `w` undefined.
- Requirement 9: “If Hk(z) denotes the retained high part” neither defines `k` nor specifies the retained-high-part function precisely, although the following success predicate depends on it.
- Requirement 9: “For the i = 0 branch” uses `i` without defining what it indexes or selects.
- Requirement 9: The paper uses the project-specific terms “VQ,” “AddsMod specification,” “raw reversible gates,” and “compiled primitive gates” without defining them before use. State the relevant interfaces, gate-count bases, and compilation rule.
- Requirement 12, Register and Terminology: “physical lookup–subtraction phase,” “first physical phase,” and “physical five-bit compression family” describe generated logical circuit syntax without defining “physical.” Use “circuit” if that is the intended meaning.
- Requirement 12, Sentences and paragraphs: “The family proof handles full blocks and a final block containing one or two genuine choices, without applying artificial padding choices” stands as a one-sentence paragraph. Combine it with the following paragraph.
- Requirement 12, Throat-clearing and Metaphor: “The remaining theorem boundary is specific” announces the following list and uses “boundary” figuratively. “Paper-specific boundary” and “committed evidence boundary” repeat the same metaphor. State the verified scope or remaining obligations directly.
- Requirement 12, Metaphor and Terminology: “The complete schedule and resource formulas reside in” uses a code-location metaphor, while “principal source endpoints” and “public endpoints” use undefined project jargon. Name the Lean modules or declarations directly.
- Requirement 12, Register: “Three choices therefore have 27 valid values” assigns the values to the choices rather than to their ordered triples. State that a block of three choices has 27 possible values.
- Requirement 12, Register and clarity: “Lean reports a subset of three standard dependencies” names no containing set and leaves unclear whether the three listed dependencies are exhaustive. State either that Lean reports those three dependencies or identify the larger set.