23 Recursive proof cubes and expansion depth
On this page · Permalink · Source line 2037
A visible proof step is rarely atomic. A lemma opens into definitions and sublemmas. A computation opens into algorithms, parameters, and exact checks. A citation opens into another dependency graph. Proof Path Theory treats this as recursive refinement.
Definition 23.1: Proof packet and refinement
A proof packet is a node presented at one resolution. A refinement replaces that node by a finite subfield whose certified target reconstructs the original node on the declared scope.
A refinement preserves the certified target on its declared scope. Preservation of other tasks requires a separate recovery condition. Let \(R_d:\mathscr A\to\mathcal R_d\) be the representation scheme at depth \(d\). A sufficient condition is a map
If a task factors as \(q=d_q\circ R_d\), then
Hence \(R_d\preceq_{{\mathcal Q}}R_{d+1}\). Repeated refinements satisfying this condition give the recoverability chain. For a restricted task family, preserving its supported tasks directly can suffice without recovering the entire preceding representation.
A longer derivation is not automatically a richer archive. It may reconstruct the same conclusion while omitting an example, a failed approach, or a provenance record. Those losses must be assessed against the declared task family.
Let \(r_d\geq0\) be a declared unresolved-work score and \(c_d\geq0\) the cumulative cost. These are model inputs. A small \(r_d\) is not, without another theorem, a certificate of a nearly valid proof. The word cube names the layered presentation, not a cubical complex supplied with additional geometric axioms.
Definition 23.2: Goal-relative depth objective
For goal \(g\) with weights \(\alpha_g,\beta_g\ge0\), define
An optimal expansion depth is any minimizer of \(J_g\).
Theorem 23.3: Expansion depth is goal dependent
The same proof object can have different optimal expansion depths for different goals.
Proof
Take a proof object with exactly two available depths \(d_1<d_2\), with \(r_{d_2}<r_{d_1}\) and \(c_{d_2}>c_{d_1}\). Direct subtraction shows that \(d_2\) is preferred exactly when
The goal \((\alpha_g,\beta_g)=(1,0)\) strictly prefers \(d_2\), whereas \((0,1)\) strictly prefers \(d_1\). Since these are the only available depths, each preference is a global optimum. If both weights vanish, every depth is optimal. No division by a possibly zero weight is needed.
A practical stopping rule selects the first depth satisfying
The first condition uses a declared tolerance. The second applies only at \(d\geq1\) with \(c_d>c_{d-1}\) and compares the most recent reduction with its extra cost. Zero-cost refinements require separate handling. These stopping rules do not generally minimize \(J_g\) over all remaining depths.
Figure 25 and the worked example in Section 24.6 give explicit costs and unresolved-work scores for three goals.
Deeper is not automatically better. A formal checker may need primitive steps. A specialist paper may cite a standard theorem. A teaching account may expand only the conceptual bottleneck. An archive may retain a failed branch that neither certificate requires.