Completeness non-vacuity: concrete OutstandingZiskPredicates instance from a real trace (completeness sibling of #74)

[codygunton]

Goal

Non-vacuity for the completeness endpoint: exhibit a concrete
OutstandingZiskPredicates instance, from a real ZisK execution, for which
EventualCompleteness holds outright. This is the completeness sibling of #74
(which does the same for the soundness trace surface).

Why it's MVP

A reader convinced by root_completeness must know it is not vacuous — that the
quantified z (ZisK's real decode/lower/row/opcode surface) is actually
inhabited by a real machine, not just an abstract record nobody can produce.
Without an instance, "ZisK covers everything Sail accepts" is a statement about a
possibly-empty domain.

Scope

1. Build a concrete z from real extracted ZisK predicates (decoder #162: prove the extracted RV64IM decoder in-build (raw word → opcode), kernel-soundly #164,
   lowering Discharge aeneasBridgeTrust: connect the real Aeneas extraction in-build (replace the loose cross-workspace coupling) #111/RomImageBinding: bind the in-build Aeneas decode pins to the committed program (make #111 load-bearing in root_soundness) #159, and the Extend Aeneas extraction to cover ZisK table data + witness builders (reduce hand-modeled Lean) #108-backed row/opcode/contract predicates once
   available).
2. Discharge the five obligations at that concrete z (or the subset available;
   keep the Extend Aeneas extraction to cover ZisK table data + witness builders (reduce hand-modeled Lean) #108-blocked ones explicit).
3. A checked-in instantiation file under the semantic-gate glob, following the
   trust/consistency/* witness pattern, applying root_completeness (or
   skeletal_root_completeness) to the concrete z.

Acceptance

• At least one checked instantiation of the completeness endpoint on a concrete
  z derived from a real trace fragment.
• No new axioms / no sorry; trust ledgers consistent.

Blocks #154. Sibling of #74. Depends on #108 for full (non-degenerate) coverage.