Block 12 — proof guide
Machine-Native Reasoning · Reviewed Core 0.2 · Core 7.3
1. Signed events before monetary or computational valuation
For a finite event type E, saving delta w = sum_i w(i) delta(i). Positive delta means old minus revised. The coordinates may be counts of different event kinds; a scalar requires the explicitly supplied linear conversion w. No intrinsic comparison of incomparable units is inferred.
all_nonnegative_prices_iff proves both directions. Nonnegative coordinates and prices yield nonnegative summands. For the converse, price a single negative coordinate at one and all others at zero. This explicit counter-price gives that coordinate as the entire value. No normalization of prices is required. The zero price is permitted, so no event vector is strictly advantageous at every nonnegative price. The empty event type is handled without inventing a coordinate.
consistent_unit_change proves that multiplying each event coordinate by a nonzero unit factor and dividing its price by the same factor preserves the value. Positive unit factors preserve nonnegative prices. Changing only one of those numbers changes the stated comparison.
2. The actual convex hull and an attained minimum
The price family uses Mathlib's convexHull Real W. For fixed delta and a proposed lower bound b, the set of prices with saving at least b is convex: linearity changes a convex combination of prices into the same convex combination of their values. hull_lower_bound_iff applies the minimality of the convex hull, proving that a lower bound holds on the hull exactly when it holds on every generating price.
finite_price_minimum reuses the established Planning.finiteMin and its attainment theorem. A listed minimizer belongs to the hull. Every hull value is at least its value by the preceding convex argument. The conclusion is IsLeast on the actual image of the hull. Thus both lower bound and membership/attainment are proved. The result needs a finite nonempty generator set; it does not assume that every listed generator is an extreme point. The convex conclusion itself does not require nonnegative generators, although operational price applications normally do.
Main endpoints: ResourcePrices.all_nonnegative_prices_iff, finite_price_minimum, listed_hull_minimizer.
3. Preparation and complete fixed workloads
Ledger supplies natural setup counts, natural workload multiplicities and natural old/revised event counts. Ledger.delta embeds counts into the reals before subtraction. delta_eq_total_difference proves that the net is exactly old total minus revised total, including setup. It never uses truncated natural subtraction for a saving.
For setup K, multiplicities n and per-use difference s, the source equation is
delta_i = sum_j n_j s_ji - K_i.
saving_net interchanges two finite sums and distributes multiplication. The priced total is the sum of priced use savings minus priced setup. workload_robust_iff applies the all-price theorem to this complete delta. Omitting setup cannot improve a guarantee at nonnegative prices. Negative per-use coordinates are not discarded.
For N repetitions of one use, amortization_iff proves the strict threshold N > priced_setup / priced_per_use when the per-use saving is strictly positive. If per-use saving is nonpositive and preparation costs are nonnegative, repetition cannot produce a positive net saving. This is a fixed workload and price contract, not a forecast of future use. Time-dependent prices must be retained as additional coordinates or accounted for before aggregation.
4. The compiler connection uses inherited counters
PriceExamples.fullCounts and streamCounts project the actual PrefixExamples.fullEight and streamEight search results. counter_binding derives their values from the unchanged Block10 theorem: 184 and45 versus153 and198. The same program result and validity theorem are retained. Embedding in signed arithmetic gives (31,-153), so priced_scan gives 31r-153t for arbitrary real read and test prices.
Equal prices yield -122. Prices(5,1) yield2. The convex hull generated by(5,1) and(8,1) has minimum2, attained at(5,1). A price such as(1,1) lies outside that declared family and is not protected by its positive bound.
The extra setup of200 test events is explicitly hypothetical. actualWorkload N uses the exact old/revised natural counters and this added charge. Its old totals are184N reads and45N tests; its revised totals are153N reads and198N+200 tests. Its signed delta is proved equal to paid N. The exact minimum over the same convex price family is2N-200. Strict uniform improvement holds exactly whenN>100. AtN=100 the minimum is zero, not positive. Under equal prices every use instead loses work.
The source book's vector(1552,1552,-1868) is included only as a supplied ledger whose two printed scalar valuations are rechecked. Its older generating experiment is not rerun or inferred from the new compiler instance.
Endpoints: PriceExamples.priced_scan, actual_workload_delta, actual_workload_totals, paid_hull_minimum, robust_reuse_threshold, source_ledger_arithmetic.
5. A correct calculation can certify a loss
PriceRevision instantiates the unchanged Block11 dependency system. Node0 asserts equality and validity of the actual returned controller. Node1 asserts that the recorded integer quote equals the actual event-count saving. Node2 asserts that the quote is correct and nonnegative. The direct artifact values are the read price and the recorded quote; capacity-test price is fixed at one. The dependency and checker remain fixed while those input values change.
The local checker accepts node2's sign only after node1 is established. meanings_complete proves the declared dependency system semantically complete, including cases with false quotes. old_established obtains actual old claims from sound checks before reuse.
Starting with read price5 and quote2, changing only the price to1 makes node1 stale; node2 is reached by forward invalidation. The old quote is rejected, and the benefit node is blocked. With the quote corrected to-122, the calculation is rechecked successfully and the benefit claim is rejected. Node0's witness is reused in both cases. every_stage_sound imports the actual generic replay theorem for every intermediate stage, not just the final displayed labels. restored_negative_real_saving connects the newly established integer quote to the real valuation from Core7.3.
This is an exact finite instance, not a host service that infers dependencies or authenticates market or hardware prices. The fixed program remains a hypothesis of this instance. A changed program, interpretation, event meter or graph requires the corresponding dependencies to change.
6. What this block does not infer
The price theorem does not make two counters a complete hardware cost model. Preparation, dispatch, allocation, acquisition, checking, controller bytes, storage limits, memory peaks and elapsed time are not free; they are absent from the isolated two-counter comparison unless separately supplied. The hypothetical setup account is not a measured recovery of all these costs.
The linear map is fixed across old and new routes. Minima over a listed convex family do not cover arbitrary nonconvex or nonlinear performance effects. A checked calculation is not proof of a positive advantage. Semantic validity, resource value and external model adequacy remain separate.
The formal proof uses exact integer/real arithmetic and classical finite minimizer selection. It is not a floating-point implementation, independent proof kernel, upstream source rebuild or mathematical priority claim.