Affordable Region Agreement

Abstract

An affordable finite-region patch forces agreement for a loss-minimal candidate.

Theorem 1.1 (Affordable regions contain no remaining disagreement).

$$\begin{array}{c}\forall Output,Loss:\mathrm{Type},\\ [\mathrm{Preorder}(Loss)],\\ \forall truth,g:\mathbb{N}\to Output,\\ \forall record,P:\mathrm{Finset}\left(\mathbb{N}\right),\\ \forall complexity:(\mathbb{N}\to Output)\to \mathbb{N},\forall price:\mathrm{Finset}\left(\mathbb{N}\right)\to \mathbb{N},\\ \forall budget,overhead:\mathbb{N},\forall loss:(\mathbb{N}\to Output)\to Loss,\\ (\forall n:\mathbb{N},n\in record\Rightarrow g(n)=\mathrm{truth}(n)),\\ \mathrm{complexity}((n:\mathbb{N}\mapsto \mathrm{ite}\left(n\in P,\mathrm{truth}(n),g(n)\right)))\le \mathrm{complexity}(g)+\mathrm{price}(P)+overhead,\\ \mathrm{complexity}(g)+overhead\le budget,\\ (\forall h:\mathbb{N}\to Output,\mathrm{Nonempty}\left(P\right)\Rightarrow (\forall n:\mathbb{N},\neg (n\in P)\Rightarrow h(n)=g(n))\Rightarrow (\forall n:\mathbb{N},n\in P\Rightarrow h(n)=\mathrm{truth}(n))\Rightarrow (\exists n:\mathbb{N},n\in P\wedge g(n)\ne \mathrm{truth}(n))\Rightarrow \mathrm{loss}(h)<\mathrm{loss}(g)),\\ (\forall h:\mathbb{N}\to Output,(\forall n:\mathbb{N},n\in record\Rightarrow h(n)=\mathrm{truth}(n))\Rightarrow \mathrm{complexity}(h)\le budget\Rightarrow \mathrm{loss}(g)\le \mathrm{loss}(h)),\\ \mathrm{price}(P)\le budget-\mathrm{complexity}(g)-overhead\Rightarrow \forall n\in P,g(n)=\mathrm{truth}(n).\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Computability/DescriptionComplexity/AffordableRegionAgreement.affordable_region_agreement (✓ std3). ∎

Source. Repository-derived.

Commentary.

The candidate and truth are total functions on the natural numbers. A finite record fixes their observed values, while a finite region P specifies the values replaced by the truth function.

The patch-cost premise bounds the corrected function by the candidate complexity plus price(P) and a fixed overhead. The accounting premise makes the natural-number subtraction explicit, so an affordable patch remains within the stated budget and stays consistent with the record.

Loss is valued in an arbitrary preorder. Correcting a genuine disagreement on a nonempty region, while changing nothing outside it, is assumed to strictly lower loss. This contradicts candidate minimality among all record-consistent functions within budget, forcing pointwise agreement.

Pinned Mathlib has no universal-machine or description-complexity theorem with these semantics. The proof therefore exposes cost and loss behavior as hypotheses and reuses only finite-set patching, natural arithmetic, and preorder contradiction.

References

• Truth anchor: D5/S0/Computability/DescriptionComplexity/AffordableRegionAgreement.affordable_region_agreement