diff --git a/experiments/ramanujan_28/submission/HOW_THE_SOLUTION_WAS_FOUND.md b/experiments/ramanujan_28/submission/HOW_THE_SOLUTION_WAS_FOUND.md
index 38a4a98..b41d32e 100644
--- a/experiments/ramanujan_28/submission/HOW_THE_SOLUTION_WAS_FOUND.md
+++ b/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: