docs(gh62): round-8 lean redesign — 20→14 closures, 7 NOT-NEEDED β with empirical evidence (refs #62)

Round-8 absorption-aware redesign of the AspectJ grammar coverage change.
Three empirical audits (APK AJC inspection, compiled .aj audit, coverage-weaver
overlap analysis — synthesised in docs/analise_sintese_macro.md) showed that
seven of round-7's twenty closures attacked constructions the upstream pipeline
absorbs before they reach the dexlib2 instrumenter.

Reclassified to NOT-NEEDED β (absorbed upstream):
- §4.G condition() — JavaMOP compiler folds into *RuntimeMonitor.*Event(...)
- §4.S __STATICSIG — JavaMOP compiler expands; generic_new audit PASS 2026-05-26
- §4.A adviceexecution() — vacuously true in dexlib2 inline-call emission model
- §4.RT aspectjlang substrate (~600 LOC) — coverage-weaver absorbs Coverage.aj
- §4.JP thisJoinPoint bindings (~250 LOC) — composite absorption upstream
- §4.CV Coverage.aj end-to-end — coverage-weaver byte-for-byte equivalent
- §4.WW within(*..Log)/within(Coverage+) — coverage-weaver PackageFilter absorbs

In-change closures: 14 (§4.{W,O,R,N,V,X,TT,AT,Y,T,B,D,I,E}).
- §4.I if() switched from in-weaver DEX lowering to MonitorRuntime.evaluateIf
  runtime delegation (D13 — eliminates Java sub-grammar parser, no VerifyError
  surface; six of six cross-LLM reviews flagged the lowering plan as BLOCKER).
- §4.E execution() RESTORED as full matcher+emitter per user decision 2026-05-26
  for defensive shipping (current corpora absorption removes consumers but future
  specs may use execution() positively).

New first-class verdict path β formalised by D12 + INV-INS-96 (Upstream Absorption
Verdict Requirement): the matrix Evidence column names the absorber stage with
empirical evidence; AbsorptionClaimsContractTest enforces the three-property
contract (source demand ≥ 1, pipeline demand == 0, absorber file exists).

Scope: ~2 000 LOC (round-7) → ~1 015 LOC (round-8). Matrix archives with zero
SILENT-GAP rows. Cross-repo coordination reduced to a single namedPointcuts
schema field (§4.D, archive precondition in tasks §0.5).

Artifact diff:
- deferred.md NEW (replaces removed ledger.md per D9 round-7 elimination); §2.2.1
  carries the 7 path-β reclassifications with named absorbers and evidence anchors;
  Appendix records the Three Empirical Audits.
- proposal.md: "Why" 5→4 silent-failure classes; closures 20→14; SourceDemand +
  PipelineDemand split in corpus-demand table; round-8 absorption section added.
- specs/instrumentation/spec.md: Removed Requirements "AspectJ Runtime Substrate"
  and "thisJoinPoint Bindings End-to-End"; added Requirement "Upstream Absorption
  Verdict"; closure count 13→14 after §4.E restoration; INV-INS-96/97/98 new;
  INV-INS-99 SUPERSEDED.
- design.md: D9 rewritten (round-8 absorption-aware); D10 marked SUPERSEDED;
  D11 narrowed (single-entry-per-descriptor symbol table); D12 (path β first-
  class) + D13 (if() runtime delegation) new. Corrected stale anchors
  (NotWithinPC:343-359 → PointcutMatcher.java:343-358) and inflated if() count
  (8/16/0/37 → 0/0/0/8).
- tasks.md: Removed §4.G/S/A/RT/JP/CV/WW closure tasks; modified §4.E (RESTORED
  full closure), §4.I (runtime delegation), §4.D (~120 LOC narrowed); added 6
  NOT-NEEDED β assertion-test tasks (§4.G'..§4.WW'); §0.5 archive precondition
  for namedPointcuts schema; race-condition fix moves SHA snapshot from §7.4a
  into §1.4 (same commit as deferred.md).
- ledger.md DELETED (round-7 had already removed; this commit captures the
  delete that staged late).

openspec validate --strict: PASS.

Author: phtcosta