I.R17 — Gap Declaration

Gap declaration: what remains unearned at the end of Book I — CIC type formation rules, CIC structural rules at the meta-level, funext/propext as kernel axioms. These are starting conditions, not defects. Book III's enrichment ladder (E0->E1->E2->E3) will progressively internalize the proof theory.