24 Worked finite examples
On this page · Permalink · Source line 2098
The accompanying repository contains three canonical JSON proof fields and several auxiliary models. The examples are small enough to inspect by hand and complete enough to exercise the formal distinctions.
24.1 A fixed AND-DAG
On this page · Permalink · Source line 2103
The field examples/and_dag.json has required premise \(A\), a definition \(D\), lemmas \(L_1\) and \(L_2\), and target \(B\). It also contains a worked example, a failed route, and a boundary case. The unique verification core is
The optional nodes have zero declared verification value for \(B\) and positive discovery, meaning, or bridge value. This is the executable instance behind Figure 17.
24.2 Two certified proofs
On this page · Permalink · Source line 2111
The field examples/alternative_proofs.json contains a short route and a richer explanatory route. The short route has storage cost \(1\), while the richer route has storage cost \(3\) and larger meaning and discovery values. Exact certificate search chooses
when the objective is storage cost alone. A teaching compiler may rationally choose the other route because it uses a different objective.
24.3 Set Cover encoded as certificate selection
On this page · Permalink · Source line 2119
The field examples/set_cover_certificate.json contains four optional source lemmas and four obligations. Exact search returns the certificate using \(S_1\) and \(S_3\), with total cost \(2\). The particular optimum is not important. The example demonstrates how local alternative derivations create a global combinatorial selection problem.
24.4 Bridge retention
On this page · Permalink · Source line 2123
The bridge experiment uses ten candidate nodes and sixteen weighted future targets. For budgets zero through five, the script computes both the exact optimum and the greedy solution. The generated data are stored in data/retention_comparison.csv. On this instance the two curves coincide. The theorem guarantees only the worst-case \((1-1/e)\) factor.
24.5 Correlated review and audit capacity
On this page · Permalink · Source line 2127
For one hundred equicorrelated reviewers with \(\rho=0.1\),
The audit example begins with backlog \(10\). Arrivals \(4\) and capacity \(5\) clear the queue. Equal rates hold the backlog at \(10\). Arrivals \(6\) and capacity \(5\) increase it by one per cycle.
| Object | Computed result | Mathematical role |
|---|---|---|
| AND-DAG | unique five-node core | Theorem 5.3 |
| Alternative field | minimum cost \(1\) | exact finite search |
| Set Cover field | minimum cost \(2\) | Theorem 6.2 encoding |
| Bridge model | greedy and exact curves | Theorems 17.1–17.2 |
| Review model | \(n_{\mathrm{eff}}\) formula | Theorem 20.1 |
| Audit model | three queue regimes | Theorem 22.1 |
24.6 An expansion-depth calculation
On this page · Permalink · Source line 2156
For depths \(0\) through \(6\), take unresolved-work scores \((1,0.55,0.30,0.18,0.12,0.09,0.075)\) and costs \((0,0.25,0.65,1.2,2.1,3.5,5.5)\). The declared weights \((\alpha,\beta)=(1,0.75)\), \((2.5,0.35)\), and \((5,0.15)\) give minimizing depths \(1\), \(3\), and \(4\), respectively. Their minimum objective values are \(0.7375\), \(0.87\), and \(0.915\). These follow by evaluating \(\alpha r_d+\beta c_d\) at the seven available depths. The labels certificate, teaching, and archive name these three supplied objectives rather than measured preferences of actual readers.
24.7 An independently checkable decoder
On this page · Permalink · Source line 2176
Take two archives with the same certificate output but different retained side answers. The following code executes the collision alternative. It then checks the result without running the producer again.
from proof_path_theory import factor_task, verify_factorization
encoding = {"archive0": "certificate", "archive1": "certificate"}
task = {"archive0": "0", "archive1": "1"}
result = factor_task(encoding, task)
assert not result.sufficient
assert verify_factorization(encoding, task, result)The witness names both archives. It is evidence that this declared task cannot be recovered from this encoding on this domain. It says nothing about whether the shared proof certificate is valid. The package's new worked script also prints the positive decoder, the protected-rule obstruction, and the semantic-cover derivations.