docs(p28): state the actual motivation -- the problem was used as an instrument

Adds the framing that explains the disproportionate machinery: Problem 2.8 was
approached as a test case for an existing pipeline (encoding, exact-arithmetic
verification, excluded-route registry), not as an isolated puzzle. A well-posed
external problem with an objectively checkable answer is a good defect-finding
instrument because it cannot be argued with.

That is why a Coq-and-Lean treatment of leading zeros sits under a pi formula:
absurd overhead for one limit, reasonable for a codec other work depends on.
Same for the mutation testing, authority tags, and impossibility registry.

Notes the congruence with the challenge's own section 1, which presents these
problems as benchmark instruments with structured verification.

Adds 'What the exercise found', since if the problem is an instrument then the
defects it exposed are part of the result:
  - defects in the argument, repaired pre-release (false ODE-normalisation
    uniqueness, invalid norm-inequality direction, unproved holomorphy in the
    maximum-modulus step, Birkhoff-Poincare as a black box, an untied scalar
    operator that could have been a surrogate, Q/P vs P/Q orientation)
  - defects in the verification machinery -- the failures that let bad results
    pass (checks succeeding with the CAS absent, quo_rem trusting a zero
    remainder, irreducibility/GCD standing in for arguments)
  - defects still open, found during independent replay (run_checks.sh exit-code
    inversion, the false assertion at line 107, the Sage 10.9 coercion error
    masking it, and the Lean-only radix DFA facing regeneration erasure)

The last group is left open rather than tidied away: a validated tool would not
still be producing these, and the point of running the instrument is that it is.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WY6SfRYvm8zFKMX9GcjS8u

experiments/ramanujan_28/submission/HOW_THE_SOLUTION_WAS_FOUND.md

@@ -10,6 +10,30 @@ leading zeros in positional notation sitting underneath a modular-forms problem.
 Each was forced by something. This document records the path so the choices can
 be read as reasoning rather than guessed at.
 
+## Why this problem, and why the machinery is out of proportion to it
+
+One structural thing should be said up front, because it explains most of what
+otherwise looks excessive.
+
+Problem 2.8 was not approached as an isolated puzzle. It was used as a **test
+case for an existing pipeline** — a body of tooling for encoding mathematical
+objects, verifying identities in exact arithmetic, and recording excluded routes.
+A well-posed external problem with an objectively checkable answer is a good
+instrument for finding defects in that kind of tooling, because it cannot be
+argued with: either the certificates reproduce the official data or they do not.
+
+That is why the infrastructure is disproportionate to a single limit. A
+Coq-and-Lean treatment of leading zeros in positional notation is absurd
+overhead for one π formula, and entirely reasonable for a codec that other work
+depends on. The same applies to the mutation testing, the per-claim authority
+tags, and the registry of proved-impossible routes.
+
+This motivation is also congruent with the challenge's own stated purpose: §1
+presents these problems as benchmark instruments with structured verification,
+precisely because "candidate formulas for constants can often be tested to
+thousands of digits, so numerical validation is immediate and objective." Used
+that way here, in both directions.
+
 ## The starting position
 
 The challenge supplies, for Problem 2.8:
@@ -166,6 +190,54 @@ rather than an impression:
 Recording exclusions as first-class results, with witnesses, is what stopped the
 search from cycling back through settled ground.
 
+## What the exercise found
+
+Since the problem was used as an instrument, the defects it exposed are part of
+the result. They fall into three groups.
+
+**Defects in the argument, found by adversarial replay and repaired before
+release** (full table in `ADVERSARIAL_AUDIT.md`). The substantive ones:
+
+- an ODE-normalisation *uniqueness* claim that was simply false — the exponent
+  `2n` supplies an additional analytic branch, so uniqueness was replaced by
+  base/generic/top coefficient induction;
+- a transfer-norm inequality applied with an invalid exponent direction for the
+  fourth column;
+- a maximum-modulus step that assumed holomorphy of a quotient where formal
+  divisibility only gave a local removable germ;
+- Birkhoff–Poincaré used as a black box for three columns, hiding the
+  exceptional hyperplane, the dominant functional, and denominator
+  non-vanishing — replaced by an explicit stable-graph contraction;
+- a scalar one-step operator not yet tied to the challenge matrix, which could
+  have described a surrogate;
+- the orientation recorded as `Q/P` when the challenge asks for `P/Q`.
+
+**Defects in the verification machinery itself** — the ones that matter most for
+a tool being validated, because they are the failures that let bad results pass:
+
+- checks that could succeed while the CAS was absent, treating a stored
+  transcript as evidence. Fixed by making dependency-free verifiers mandatory;
+- Ore divisions using `quo_rem`, trusting a zero remainder instead of exhibiting
+  a cleared factorisation;
+- irreducibility and GCD calls standing in for arguments.
+
+**Defects still open at the time of writing**, found during independent replay
+(detailed in `ADVERSARIAL_REVIEW_AGAINST_CHALLENGE_RULES.md`):
+
+- `run_checks.sh` exits 1 on any machine *with* SageMath installed, because
+  `set -euo pipefail` makes the declared-optional cross-checks fatal. The script
+  therefore passes without the optional tooling and fails with it;
+- a false assertion in `p28_lattice_hypotheses_certificate.sage` — component 1
+  reads `216 + 154x` where the true value is `216 + 262x`. Non-load-bearing: the
+  identity below it is correct;
+- a Sage 10.9 parent-coercion error that was *masking* the previous item;
+- the radix DFA exists only in `Radix.lean` while that repository regenerates
+  Lean from `coq/*.v`, so a regeneration would silently erase it.
+
+The last group is the honest state of things rather than a finished story. A
+tool that had been validated would not still be producing these; the point of
+running the instrument is that it is still finding them.
+
 ## Limits of the method
 
 **The encoding is not compression.** Measured: