4 The ambient proof field and the meaning of failure
On this page · Permalink · Source line 365
A finished proof is rarely the only route the researcher could have explored. An archive often contains sketches that were never completed, arguments that failed because of a specific hypothesis, conjectured bridges that remain untested, and genuinely refuted local constructions. It is tempting to call this whole archive a proof, but doing so would erase the distinction between a certified result and a record of exploration. The ambient proof field provides a more precise language: it is the declared field of reachable or recorded mathematical states and typed candidate transitions in which certified proof paths form a distinguished subfield.
The finite hypergraph model permits failed_route, boundary_case, and counterexample nodes. Their presence is useful, but none is a logically justified global nonexistence claim by itself. A failed search is not necessarily a proof of impossibility. A counterexample to one proposed lemma is not necessarily a counterexample to the goal. An exact obstruction must have a declared scope and a checkable witness.
Definition 4.1: Scoped branch assessment
Let \({\mathcal P}\) be a finite typed proof field with declared premises \(A\) and target \(t\). An exploratory branch is a finite sequence of candidate justifications whose certification and outstanding obligations are explicitly recorded. Its assessment is one of the following, relative to stated premises and rules:
Open: obligations remain unresolved.
Abandoned: exploration stopped without a certificate of impossibility.
Locally refuted: a checked counterexample or obstruction excludes a stated intermediate step under specified hypotheses.
Certified: the selected justifications meet the declared proof certificate conditions.
An assessment is a record of the branch, not a truth value assigned to every possible proof of \(t\).
Proposition 4.2: Local failure does not imply global failure
A finite proof field may contain a locally refuted branch to target \(t\) while also containing a certified derivation of \(t\) from its declared premises.
Proof
Take a premise \(A\) and two alternative candidate derivations of \(t\). Let the first use a proposed intermediate lemma \(L\) that has a checked counterexample, so the corresponding justification is not certified. Let the second use a distinct certified justification from \(A\) to \(t\). The certified closure reaches \(t\) by the second route. The failed first route remains a valid record of unsuccessful exploration, but cannot negate the existence of the second certificate. The same example can be represented by the alternative justification hypergraph developed earlier.
The logical lesson is substantive for machine reasoning. A search timeout, budget exhaustion, invalid intermediate conjecture, or failure to find a proof all have different meanings. Only a certificate whose conclusion explicitly concerns nonexistence under a declared model and scope licenses a nonexistence claim. This is especially important when a failed branch is used to prune an automated search. Pruning the refuted step may be safe, while pruning its entire goal may discard a genuine proof.
Proposition 4.3: Scoped refutation survives unchanged context
Suppose a witness \(w\) is verified by a sound checker to refute the predicate \(L\) under assumptions \(A\). In any later archive revision that retains the same interpretation of \(L\), the same assumptions, and the checker's verification rules, \(w\) remains a refutation of \(L\). No conclusion follows about different predicates, altered assumptions, or alternative branches to a different goal.
Proof
The verification of \(w\) depends only on the declared predicate, assumptions, and checking rules. An append-only collection of unrelated exploratory records does not alter those inputs. Therefore the same verification remains valid. When any of those inputs changes, the earlier check no longer certifies the revised claim without an explicit comparison theorem.
This is a qualified stability principle, not a general theorem that proof search is decidable. The append-only derivability result of Section 18 concerns certified edges. The present proposition concerns the narrower persistence of a checked counterexample under a fixed interpretation. Both retain scope as part of the mathematical data.