This note isolates the instantiation layer of the EA(t,r) program. Its purpose is narrower than a transfer theorem: it does not claim that F*AGI satisfies EA(t,r), does not restate the family note, and does not re-derive the transcript-to-notebook pipeline. Instead, it explains what a concrete instantiation must supply: a family-side defect invariant, a strong local forcing mechanism on critical supports, and a structural no-trapping statement preventing premature exposure under partial assignments. The note includes a worked expander-parity prototype realization supported by the project materials, where defects are attached to parity-obstructed components and no-trapping is witnessed by expansion. This realization is presented only as a prototype model instantiation of the template, not as a theorem about F*AGI. The final sections list the open family-specific obligations required for a later transport to the frozen family/interface layer.
Jonatan Muñoz Rodriguez (Fri,) studied this question.