fix(dead_candidate_scan): stop one unbalanced backtick in docs/index.md from hiding citations

[phasetr]

What was wrong

Markdown code spans are paired positionally, so one unbalanced backtick does not
merely lose its own span: it inverts the parity of the rest of its line. Prose is
then read as a citation and the citations are read as prose, and nothing warns.

Measured on main 075bcd39:

• docs/index.md:1809 is a single 52186-character progress row that spells
  `ContinuousOn`.continuousAt` with three backticks where two were meant
  (they sit at columns 9925/9938/9952). From column 9952 on the parity is
  inverted: the line contributes 218 tokens and none of them names
  magnetizationAlongExhaustion, though the raw line spells it six times.
• Consequence at verdict level: magnetizationAlongExhaustion_differentiable_beta_gen
  came out safe-to-delete with the reason "no citation in the scanned
  documentation", while docs/index.md:1809 cites it as
  `magnetizationAlongExhaustion_continuous_beta_gen` + `_differentiable_beta_gen` + ...
• docs/index.md:1200/:1201 carry the sibling shape, a code span opened on one
  line and closed on the next, which `[^`\n]+` cannot match under any
  pairing; it hid latticeBallBoundaryEdges_card_le_sphere and
  latticeSphere_card_le' as tokens.
• Those three are the only lines with an unpairable backtick in README.md,
  docs/**/*.md and tex/proof-guide.tex as of 075bcd39. README.md:66/:69
  are fence delimiters and pair off.

A second, independent hole sat behind the first: _differentiable_beta_gen
matches three declarations (correlation / magnetization / susceptibility), so
even with the tokens restored the family-label rule attributed the citation to
nobody and the verdict stayed safe-to-delete.

A third hole, one level up, was found by review of this branch and is fixed in
17074732: the fenced alternative of _MD_TOKEN_RE is re.DOTALL and
unbounded, so an unbalanced run of three or more backticks pairs with the next
run anywhere in the file and its body swallows every line in between — and
crediting the whole match then let the very match that hides those citations
certify their backticks as read. Measured counterexample:

text = "start ```\ncite `_alpha_gen` here\nand `beta{,_two}_gen`\nend ```\n"
unpaired_backticks(text) == {}          # clean bill of health
_markdown_source(...).tokens == []      # both citations gone

Both shapes are the fragment ones (a brace alternation, an elided suffix) with
no verbatim fallback: the fenced body is split on whitespace and _nameish
rejects the pieces that still carry a backtick.

What changed

scripts/dead_candidate_scan.py plus its tests and fixtures header; no Lean, no
docs/, no tex/, no CI wiring.

• unpaired_backticks(text) returns every backtick no code span absorbed, keyed
  by line. A well-formed span carries no backtick inside it, so it exonerates
  nothing but its own delimiters. A fenced match is credited with its two
  delimiters and never with its body, so the text above now reports
  {2: 2, 3: 2} and both citations are recovered. A fenced block that
  legitimately quotes a backtick is charged too: the price is one coverage
  warning plus one superset re-read, both keep-only.
• unbalanced_fence_run(text) reports an odd number of fence runs. It catches
  the one shape the backtick count cannot: a six-backtick run reads as a fenced
  match with an empty body, so every backtick pairs off while the file is still
  malformed. Charge-only, like the rest of the coverage warnings — it reaches
  neither a verdict nor the exit code.
• _markdown_source does not skip a flagged line — skipping drops exactly
  the citations with no verbatim fallback. It re-reads the line with
  pairing_independent_tokens, which splits on backticks: every code-span body
  is a maximal backtick-free substring of its line, so the split is a superset
  of the bodies any pairing can produce. The re-read can add citations and
  cannot drop one. The defect is still reported, in a coverage warnings, Markdown backtick parity block, so the Markdown gets repaired rather than
  worked around.
• elided_prefix_matches treats a suffix citation whose elided prefix is spelled
  out on the same line as a shorthand for the siblings that share that prefix,
  rather than a family label attributed to nobody. A family label on a line that
  elides nothing still rescues nobody.
• LIMITATIONS gains L10 (backtick parity, fences included) and L11 (family
  labels); the module docstring gains the corresponding fifth design rule.

Corrections made after review (389b91f5 → 17074732)

Two numeric claims shipped in 389b91f5 were false as written and are replaced
by the measurement:

• elided_prefix_matches and L11 said charging every family-label match
  "leaves no reachable safe-to-delete verdict at all". Measured by applying
  that mutant to the real file and sweeping all 10965 declarations: it leaves
  232 (published 6731 / uncertain 1467 / load-bearing 2535 / safe 232), a
  collapse from 1458 (84%), not an elimination. The rejection stands on the 84%
  collapse plus --expect FAIL (1 of 18), and the source now says that. The
  fragment census quoted alongside it (514 of 742 … 5253 of 11000) did not
  reproduce either and is restated as measured: 531 of the 759 distinct
  fragment-shaped tokens that resolve at all match two declarations or more,
  union 5895 of 11000.
• The same docstring said a genuine family label (_ferromagnetic, _pos)
  "elides no prefix anyone spelled out and is unaffected". Measured on the real
  documentation, _ferromagnetic is charged 155 times and _pos 9
  times. Counterfactual on the 223 _ferromagnetic candidates: rule off leaves
  92 safe-to-delete, rule off for _ferromagnetic only leaves 60,
  rule on leaves 47 — so that one label accounts for 13 of the 45 that move
  and other elided fragments on the same rows for the remaining 32. The
  docstring now states this instead of denying it. (The 932 declarations
  figure is likewise replaced: the rule makes 2206 charges over 1077
  distinct declarations.)

The 84%/232 correction does not change the decision, and neither correction
changes a line of classifier behaviour.

Measurements

Run on this branch against main 075bcd39.

• docs/index.md coverage warnings: 3 (:1200, :1201, :1809); the run
  reports 0 recovered tokens on :1200, 2 on :1201, 277 on :1809.

• The 10 declarations of IsingModel/AmbientLattice/BetaDerivativeMagnetization.lean:
  before, 3 published / 6 load-bearing / 1 safe-to-delete; after, 5 published /
  4 load-bearing / 1 uncertain / 0 safe-to-delete. The one that moved is
  magnetizationAlongExhaustion_differentiable_beta_gen, now charged by
  shorthand docs/index.md:1809: `_differentiable_beta_gen` .

• Whole-library sweep, all 11000 non-anonymous declarations classified (10965
  distinct names) on main and on 17074732: 235 verdicts move, and every move is
  toward keeping —

  move	count
  safe-to-delete -> uncertain	142
  safe-to-delete -> load-bearing	53
  safe-to-delete -> published-result	20
  load-bearing -> published-result	9
  uncertain -> load-bearing	9
  uncertain -> published-result	2

  No move has safe-to-delete as its target, and the after-safe set is a strict
  subset of the before-safe set. Totals: safe 1673 -> 1458, uncertain 561 -> 692,
  load-bearing 2031 -> 2084, published 6700 -> 6731. Documentation family labels
  844 -> 512.

• The fence repair is not reachable on the current corpus and changes nothing
  there: no fenced body in README.md or docs/**/*.md contains a backtick, and
  every scanned Markdown file has an even number of fence runs. The same
  10965-declaration sweep on 389b91f5 and on 17074732 is identical —
  0 verdicts moved, safe stays 1458, family labels stay 512. README.md:66
  and :69 already carry fences, so one added or removed delimiter reproduces
  the counterexample.

• _ferromagnetic family calibration (--pattern '_ferromagnetic$', 223
  candidates): 92/44/52/35 -> 47/77/64/35 safe/uncertain/load-bearing/published;
  45 candidates leave safe-to-delete, 33 to uncertain and 12 to
  load-bearing through the delete-closure. Zero-consumer count is unchanged at
  112. FamilyCalibrationTest and the fixtures header are refreshed together;
  the header had also drifted, still carrying 263/132/143 from main 0922a812.

Tests

• 15 new cases: MarkdownBacktickParityTest (12) and ElidedFragmentTest (3).
  They cover the synthetic parity flip, the swallowed fenced block and its
  recovered tokens, the run-parity check and the six-backtick shape it alone
  catches, the real docs/index.md warnings and recovered tokens, the end-to-end
  verdict of the declaration the defect offered up for deletion, and both sides
  of the elision rule. test_balanced_lines_and_fences_raise_nothing asserted
  the old silence on a fence whose body quotes a backtick and is rewritten to the
  fail-closed expectation.

• python3 scripts/dead_candidate_scan.py --self-test: 94 tests, pass (90 on
  389b91f5, 79 on main).

• python3 scripts/dead_candidate_scan.py --expect scripts/audit/dead_candidate_fixtures.tsv:
  18 rows, pass.

• python3 scripts/test_audit_gate.py: 166 tests, pass (1 skipped).
  python3 scripts/test_citation_audit.py: 150 tests, pass. Neither module
  imports dead_candidate_scan; the only coupling is test_audit_gate.py's
  import-contract check, and the from audit_gate import (...) list is unchanged.

• Weakening mutants, each applied alone and reverted, guard tests re-run:

  mutant	result
  M1 drop the pairing-independent recovery	RED, 4 failures
  M2 make unpaired_backticks return {}	RED, 8 failures + 1 error
  M3 restore "a 2+-match fragment is attributed to nobody"	RED, 3 failures
  M4 charge every match of every family label	RED, 5 failures, fixtures FAIL 1 of 18
  M5 credit a fenced match with its whole span	RED, 2 failures

  M5 is new with this round and turns red exactly the two tests that pin the
  fence repair: test_a_backtick_inside_a_fence_is_charged_not_exonerated and
  test_the_swallowed_citations_are_recovered_and_reported.

• lake build was not run: no Lean source is touched by this branch.

Scope notes

• The unbalanced backtick in docs/index.md:1809 is still there. Repairing the
  Markdown is editorial and stays out of this branch, which only stops the
  scanner from reading the damaged line as evidence of absence.
• Two shapes stay outside the superset step and are recorded as L10: a code
  span opened on one line and closed on the next is unmatchable in either
  pairing (both lines still raise the warning), and prose read as a citation by
  the re-read can only add uncertain, never remove it.
• Three review findings are deliberately left as recorded rather than changed
  here. elided_prefix_matches uses a lexical startswith with no identifier
  boundary (58 charges over 47 sites today, and an identifier-boundary variant
  changes 0 of 10965 verdicts); the elision rule's locality bound is the
  documentation line, which on a 52186-character progress row is wide; and
  test_the_real_index_raises_its_three_warnings pins line numbers that an
  editorial Markdown repair would move. All three are over-keep or editorial, so
  none can produce a false safe-to-delete.
• Follow-up on this branch: the retracted figures had survived in the
  ElidedFragmentTest docstring of scripts/test_dead_candidate_scan.py
  ("5253 of 11000 declarations, no reachable safe-to-delete"). It now states
  the measured 5895 of 11000 and the collapse from 1458 verdicts to 232,
  matching dead_candidate_scan.py; grep -rn "5253\|no reachable" over the
  worktree finds no other copy.

🤖 Generated with Claude Code