Skip to content

docs/proof-debt.adoc: QuantumCNO §(d) table breaks asciidoctor (literal |0⟩ pipes); y_not_cno comment cites a stale triage line #166

Description

@hyperpolymath

Finding

asciidoctor docs/proof-debt.adoc fails to render the ledger:

asciidoctor: ERROR: proof-debt.adoc: line 204: dropping cells from incomplete row detected end of table

Pre-existing on main (line 204 at 3c8796a; line 216 on the #165 branch after its additions). The Phase 2d QuantumCNO §(d) table carries literal |0⟩ ket notation inside cells (+|0⟩+ at the CNOT_gate_unitary row and the neighbouring unitary_inverse_property row). The +…+ passthrough protects the text from inline formatting but not from the table cell separator, so asciidoctor sees an extra | and truncates the row.

Second, smaller record-hygiene item in the same area: the leading comment on Axiom y_not_cno (proofs/coq/lambda/LambdaCNO.v:399) cites "triage row LambdaCNO.v:356"; the axiom has drifted to line 399 and the triage doc is now .adoc, so the pointer is stale. The trusted-base gate does not read it (it keys on AXIOM: with a colon, or on a path mention in docs/proof-debt.adoc), which is how #165 first went red when an unrelated sentence containing the path was rewritten.

Acceptance criteria

  • asciidoctor -o /dev/null docs/proof-debt.adoc exits 0 with no ERROR: line (escape the pipes with \| or {vbar}, or use a a| cell / |=== with an explicit cols separator).
  • The rendered QuantumCNO table shows the same number of rows as the source has |<line> entries (11 §(c) + the §(d) rows).
  • y_not_cno's leading comment either carries AXIOM: (with the colon) or cites the current proofs/coq/lambda/LambdaCNO.v:<line> and docs/proof-debt-triage.adoc row.
  • Mutant: re-introducing one bare | inside a cell reproduces the dropping cells error.

🤖 Generated with Claude Code

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    documentationDocs, prose, diagrams, READMEs, ADRsproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debt

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions