7 What remains valid after a revision
On this page · Permalink · Source line 803
A mathematical proof can remain true while no longer applying to the installed system.
On this page · Permalink · Source line 804
A certificate for ordinary integer addition is not a certificate for an operation with the same printed name and a different implementation. A grammar quotient depends on the grammar order. A comparison depends on the actual controller and the prices used to value its events. These are distinct dependencies.
7.1 Reuse follows semantic dependencies
On this page · Permalink · Source line 807
Let an artifact state be \(a=(a_1,\ldots,a_d)\). A finite directed acyclic graph represents claimed guarantees. For vertex \(v\), let \(D_v\) be its direct artifact dependencies and let \(\operatorname{pa}(v)\) be its parent guarantees. The declaration is semantically complete if the meaning of its claim and local verification rule is determined by those components and parent claims. External assumptions are included explicitly as premises.
After changing \(a\) to \(a'\), mark a vertex stale when a direct input changes and propagate staleness to all descendants. Call the resulting set \(\Delta\).
Theorem 7.1: Selective reuse with complete dependencies
Assume the graph is finite and acyclic, direct dependencies are semantically complete, local rules are sound, and the applicable external premises hold. Assume also that every old witness established its old claim before the revision. Old witnesses still establish every claim outside \(\Delta\). Re-establishing affected claims in topological order, using revised values and established parents, restores the corresponding revised claims. Without an affected parent's re-establishment, this reuse rule supplies no justification for its dependent claim.
Read proof · Recorded Lean scope · Permalink · Source line 812
Proof
A vertex outside \(\Delta\) has unchanged direct values and no stale parent. In topological order, induction shows that every parent retains its meaning and proof. Completeness of the dependency declaration leaves the local argument applicable. For a stale vertex, once its revised parents are established, soundness of the newly checked local rule gives the revised conclusion. A second topological induction proves restoration. An unchecked parent leaves a missing premise, so the rule alone cannot justify a dependent conclusion. This is not a proof that the conclusion is false.
Source relationship. [SII], Theorem 24.1. It is a theorem about a declared complete dependency graph, not a method that infers complete dependencies from arbitrary programs.
Counterexample 7.2: A missing dependency defeats a perfect replay
A stored claim is \(u=v\), initially with both values zero. Its registry records only \(u\). Change \(v\) to one. A flawless comparison with the recorded \(u\) still passes, while the claim is false. A hash or replay cannot recover the premise the registry omitted.
Adding the universal repair from the preceding chapter changes a successful-repair set. It invalidates a cardinality certificate and any dependent performance statement. It need not invalidate an arithmetic equation used elsewhere. A new valid repair also does not inherit the old controller's speed comparison. Rechecking can legitimately conclude that the new route is slower, cheaper, or incomparable under the stated resources.
7.2 Semantic improvement and resource improvement are separate
On this page · Permalink · Source line 831
Fix named additive event types. Let \(K\ge0\) be an extra preparation vector, let \(s_i\) be the old-minus-new per-use vector for workload type \(i\), and let \(n_i\) count its uses. The net event difference is
A nonnegative price vector \(w\) converts these events into one declared additive measure. Storage capacity, peak memory, and elapsed time need their own models unless a justified conversion is specified.
Proposition 7.3: Which gains survive every admitted price?
The saving \(w\cdot\Delta\) is nonnegative for every nonnegative price vector if and only if every coordinate of \(\Delta\) is nonnegative. If prices lie in the convex hull of a finite nonempty set \(W\), their minimum saving equals \(\min_{w\in W}w\cdot\Delta\).
Read proof · Recorded Lean scope · Permalink · Source line 838
Proof
A componentwise nonnegative vector has nonnegative inner product with every nonnegative vector. If coordinate \(j\) is negative, assigning price one only to that coordinate gives a negative result. This proves the first assertion. A point in the stated convex hull is a convex combination of its listed prices, so its saving is the same convex combination of their savings. It cannot be smaller than the minimum listed value, and a listed minimizer attains that value.
Source relationship. [SII], Proposition 25.1. No hardware performance law follows from this additive accounting identity.
For the source's checked weighted-search comparison, the event difference is \((1552,1552,-1868)\) in reads, rational additions, and comparisons. Equal prices give \(1236\) saved units. Prices \((1,0,1)\) give a loss of \(316\). Both conclusions concern the same valid controller. The main text uses this as a transparently rechecked source calculation, not as a new measured timing result.
7.3 Evidence across an adaptive sequence
On this page · Permalink · Source line 848
A procedure that searches many candidates can select a favorable error in its evaluator. The right statement must therefore condition on the information that produced the candidate, not merely repeat a marginal error bound for a candidate fixed in advance.
Proposition 7.4: A conditional error budget for a lineage
Let \(\mathcal H_{j-1}\) contain the information available before attempt \(j\). Suppose the event \(A_j\) of accepting a false claim satisfies
for deterministic nonnegative \(\delta_j\). Then the probability of ever accepting any false claim is at most \(\delta\), even when candidates and the stopping time depend on earlier history.
Read proof · Recorded Lean scope · Permalink · Source line 851
Proof
Taking expectations gives \(\Pr(A_j)\le\delta_j\). A union bound gives the result for every finite set of attempts. The finite unions increase to the event of any false acceptance, so continuity of probability gives the infinite statement. Stopping removes attempted events and cannot enlarge their union.
Source relationship. [SII], Proposition 26.1. The mathematical input is conditional validity of each actual attempt. A numerical error schedule alone does not establish that premise.
This proposition is not an empirical result about a population of agents. It explains what evidence would need to remain valid when an evaluator is used adaptively. Deterministic exact checks in this book are not treated as statistical samples and are not assigned confidence intervals through this formula.
What is now available
On this page · Permalink · Source line 866
A revision can preserve its meaning, identify stale obligations, and state its resource advantage under explicit prices. None of this yet determines what several participants can know together or which authority they should exercise. The final technical chapter keeps information sharing and institutional permissions separate while applying the same preservation discipline.