Block11 assumption and scope review
Admitted source result: Core7.1 only. Core7.3,7.4 and the other six remaining book results retain their unformalized status.
| Obligation | Formal location | What is established | What is not inferred |
|---|---|---|---|
| Actual changed inputs | Graph.view, changedRoots | Typed value restriction and exact inequality | A hash is injective or a filename binds semantics |
| Forward closure | closure_iff_reach | Computed closure equals finite forward reachability | Discovery of omitted edges |
| Finite convergence | bounded_stabilization | At most card V minus initial cardinality strict rounds | Efficient practical graph traversal |
| Acyclic proof order | Graph.Ranked, replayGuard | Every supplied parent rank is lower | An ungrounded implication cycle proves its own premises |
| Semantic locality | System.Complete | Required as a theorem premise; proved for the actual example | Automatic dependency extraction from arbitrary code |
| Sound checker | System.sound | A passing local check plus actual parents and external premises establishes the claim | A passing flag alone proves anything |
| Old establishment | Established, established_from_checks | Correct old check, old external premise and old claim retained | Mere source presence or archived PASS text |
| External applicability | selective_reuse, checkedFinish | Explicit new premises; admission blocks unassured copying | Independent authentication of a provider's flags |
| Partial replay | replay_sound | Every returned witness sound at every stage | Rejected/missing/blocked means mathematically false |
| Complete restoration | restoration | All vertices restored when actual new witnesses and premises pass | Existence or efficient discovery of such witnesses |
| Fixed snapshot | replay parameters a,b,System | Every layer uses the same revised artifact values and rule types | Concurrent host mutation or crash-safe commit protocol |
| Existing controller integration | RevisionExamples | Actual model, Tree, Valid, profile and general lower-bound semantics | Reformalization of a separate historical Python implementation |
| Updated profile | obsolete_profile_rejected | Old numerical target not inherited by a new valid controller | A universal repair preserves an old performance claim |
All finite carrier empty cases are permitted by the generic graph result. Restoration's layer count uses one plus the maximum rank, with the empty supremum zero. This is an upper bound on a defined computation, not a claim about its byte storage. Artifact and witness coordinate types can be heterogeneous; they remain fixed across a revision. A schema or rule change must be represented inside the declared inputs where appropriate or treated with a new checked correspondence.
The source theorem does not require a unique minimal set of semantically changed claims. Staleness is exact for the declared graph. Some stale claims can remain true, and some accepted earlier witnesses can revalidate unchanged. The new theorem preserves this distinction.