BLOCK11_PROOF_GUIDE.md
Machine Native Reasoning
BLOCK11_PROOF_GUIDE.md
1 # Block 11 — mathematical route through selective reuse
2
3 **Source:** Machine-Native Reasoning, Reviewed Core 0.2, Theorem 7.1, printed page 26. The book and the forty-six predecessor substantive Lean modules are unchanged.
4
5 ## 1. A finite closure, not a declared list of stale names
6
7 A graph assigns each claim `v` its finite parent set and finite direct artifact-input set. Artifact coordinates may have different types. An environment is a dependent function assigning one value to each coordinate. `Graph.view` is the literal restriction to the declared direct inputs.
8
9 The root set contains exactly vertices with at least one changed direct value. Write `S_0` for that set and set
10
11 S_(k+1) = S_k union {v : some parent of v belongs to S_k}.
12
13 Each stage contains the previous one. Every strict growth adds a vertex, so a fixed point occurs within `card V - card S_0` strict rounds. The implemented closure uses `card V` rounds, not a supplied stopping witness. Once fixed, the sequence stays fixed. The proof identifies the computed result with the inductively defined finite forward paths from the changed roots.
14
15 Thus a nonstale vertex has equal direct restrictions and no stale parent. A separate theorem makes the closure the least forward-closed set containing the roots. This construction does not require acyclicity. It works on a cyclic graph too, but closure of changes does not make circular proof dependencies sound.
16
17 **Endpoints:** `Dependency.bounded_stabilization`, `closure_stable`, `closure_least`, `closure_iff_reach`, `Graph.nonstale_view`, `Graph.nonstale_parents`.
18
19 ## 2. What semantic completeness actually says
20
21 `System` contains a claim predicate, an external-premise predicate, a typed local Boolean checker, and a universal soundness theorem. The checker receives only the local restriction and its own witness. Local soundness requires the applicable external premise and already established parent claims before deriving the child claim.
22
23 `System.Complete` is a different condition: equal direct restrictions, equivalent parent claims and equivalent external premises imply equivalent local claim meanings. It is a formal assumption for the general theorem and an actual proof for the example. It is not replaced by equal filenames, digests, cache identifiers or a diagram label.
24
25 `Established a v w` contains all three obligations: the actual local check passes on `a`, the applicable external premise holds, and the old claim is already established. The source's old-witness premise is consequently explicit. A separate topological induction derives establishment from local check results and external premises when all parents are grounded in an acyclic graph. Two circular implications cannot bootstrap it.
26
27 ## 3. Selective reuse
28
29 A topological rank is a map to natural numbers that strictly increases from every parent to its child. It is an explicit acyclicity certificate. Strong induction on that rank transports claim meaning outside the stale closure. The direct restrictions agree there, and every parent lies outside the closure as well.
30
31 The original witness is copied without changing it. Its Boolean check agrees because its actual input restriction agrees. The old established claim transfers through the proved meaning equivalence. The new external premise is required, not manufactured by that equality.
32
33 **Endpoint:** `Dependency.System.selective_reuse`.
34
35 The argument remains a conditional mathematical statement. A graph or checker change is not silently included in a value-only revision of the same `System`. Its semantic correspondence would need to be established separately.
36
37 ## 4. Partial restoration is an actual finite procedure
38
39 The replay table uses seven distinct constructors: pending, missing evidence, rejected witness, blocked by parents, blocked by external premise, reused witness and newly rechecked witness. Staleness is a separate set property, not one of those truth judgments.
40
41 Initially every unaffected vertex holds its exact old witness and every affected vertex is pending. At rank layer `k`, only affected vertices of that rank are reconsidered. The procedure checks parent availability, the supplied external flag, the presence of a new witness, and the result of its actual local checker in that order. Vertices at the same rank have no dependency edges between them under the rank certificate. The computation ends after one more than the largest rank.
42
43 `replay_sound` proves by induction that every exported witness has its revised interpretation at every intermediate layer, even if other vertices fail or lack evidence. A blocked or rejected table entry supplies no negation of its intended claim. When every affected vertex has a passing revised witness and an available external premise, topological induction proves readiness below each completed rank. `restoration` combines this readiness with soundness to obtain an actual established witness for every vertex.
44
45 This is not a proof that proof search can always find those new witnesses. Nor is an execution timeout a completed failure of proof existence. Rank iteration and finite input comparison are mathematical operations, not measurements of host time or storage.
46
47 **Endpoints:** `System.replay_sound`, `replay_unaffected`, `replay_complete`, `restoration`, `finish_sound`.
48
49 ## 5. The outer admission boundary
50
51 Blindly copying an unaffected witness is unsafe if its external premise is unavailable. The admitted interface therefore checks both the supplied topological rank and the external flags of every unaffected vertex. If either fails, it returns `none` rather than a table claiming reuse. On affected vertices an unavailable flag produces a blocked-external outcome.
52
53 `admitted_reuse_and_restoration` ties any admitted output to the actual old established snapshot, semantic completeness and soundness of the external flags. The flags do not prove the external facts. A caller must supply the theorem connecting true flags to the declared premises. This separation is especially important for physical observations, delegated permissions and unverified service contracts.
54
55 ## 6. The repair-language instance
56
57 The example has five claim vertices and three artifact inputs:
58
59 | Claim | Direct inputs | Parent claims |
60 |---|---|---|
61 | Arithmetic identity | None | None |
62 | Singleton counting scope | Repair-language selector | None |
63 | General controller lower bound | None | Counting scope |
64 | Actual controller validity | Repair selector and controller selector | None |
65 | Actual controller profile | Controller selector and expected-profile record | Controller validity |
66
67 The repair selector chooses the already formalized `BinaryExamples.eight` or `BinaryExamples.universalRepair`. Only the success predicate changes. The controller selector chooses the inherited balanced tree or one immediate repair. The lower-bound claim quantifies over every finite horizon, every support and every valid controller. The profile is the actual `HardInquiry.Model.profile` of the selected tree, not a Boolean merely named 'profile'.
68
69 The declared dependency registry is proved complete. The lower-bound claim is equivalent to the counting scope in this particular two-model family. Its failure under universal repair is proved by the actual one-step controller. The profile computation is proved independent of the changed acceptance relation, while its claim still requires the selected controller's validity.
70
71 Changing only the repair language has direct roots `{scope, validity}` and exact stale closure `{scope, lower bound, validity, profile}`. The arithmetic identity is unaffected. A first replay with missing profile evidence returns:
72
73 | Vertex | Actual outcome |
74 |---|---|
75 | Arithmetic identity | Reused |
76 | Counting scope | Rejected |
77 | General lower bound | Blocked by its rejected parent |
78 | Old balanced controller validity | Rechecked successfully |
79 | Its still-true profile | Missing evidence |
80
81 A second snapshot installs an immediate repair and changes the expected-profile record to `(1,1)`. Its validity and profile are both rechecked. The previous generic counting bound remains false. Retaining the old `(4,15)` profile record instead causes rejection, even though the newly installed controller is valid. No old speed or value comparison is silently restored.
82
83 **Endpoints:** `RevisionExamples.meanings_complete`, `old_established`, `addition_sound`, `replacement_sound`, `replacement_actual_controller`, `obsolete_profile_rejected`.
84
85 ## 7. Mathematically distinct failure modes
86
87 The scalar omitted-input example keeps the recorded value `u` unchanged, changes an unrecorded `v`, and turns `u=v` from true to false. Local replay still passes. The source proves that the corresponding completeness assertion is false.
88
89 The cyclic example has two false claims and two sound implication rules, each conditional on the other. Every local Boolean check can pass, but neither old claim is established and no topological rank exists. The admission gate rejects every proposed rank.
90
91 Additional examples separate stale from false, missing evidence from false, rejection of a malformed witness from refutation, a true child from an available parent proof, and exact artifact equality from equality of an arbitrary fingerprint. The actual ordered compiler from Block10 supplies the example that a changed query order can change the literal returned tree.
92
93 These are universal or exact finite Lean statements. They are not statistical trials, learned dependency discovery, or an automatically verified host certificate manager.