Propose capacity guards before table appends

Guard an approved ADD 1 and adjacent equal-width character MOVE into one fixed OCCURS table before changing the count. Derive capacity from the declaration and reject negative counts or counts at or above capacity through an approved existing terminal exit. Require exact source and COPY snapshots, disjoint ordinary storage and an explicit count-of-stored-rows contract. Require a bounded local integer witness for an invalid destination subscript. Unknown values and unsupported arithmetic do not establish a finding. Preserve disjoint integer facts across a prior equal-width character table write only when every possible subscript is proven in bounds. Prove the generated condition over all integers and prove that every accepted increment fits the counter and produces a valid table subscript. Preserve the original increment and write and all bytes outside the inserted guard. Add no period and discard no row silently. Keep findings when an unproven exit or unsupported insertion layout prevents a proposal. Application team review remains required.