16 Latent bridge graphs
On this page · Permalink · Source line 1615
A proof field records certified dependencies. A latent bridge graph records possible future transfers. The two graphs have different logical roles.
Definition 16.1: Latent bridge graph
A latent bridge graph is a finite directed graph
whose nodes include retained proof objects, omitted proof objects, and anticipated future targets. An edge \(x\to y\) means that \(x\) has been declared a possible transfer route toward \(y\). The edge may be certified, conjectural, or exploratory, but its status must be recorded.
Let \(S\subseteq W\) be the retained starting set. Let \(F\subseteq W\) be a future target set with weights \(w_f\ge0\).
Definition 16.2: Future reach utility
The weighted future reach of \(S\) is
This quantity measures declared reach, not truth. A conjectural edge can increase modeled reach without certifying the target. The ledger must keep those statuses separate.
16.1 Bridge criticality and dominators
On this page · Permalink · Source line 1642
Definition 16.3: Bridge-critical node
A node \(v\) is bridge critical for target \(f\) relative to starts \(S\) when \(f\) is reachable from \(S\) in \({\mathcal B}\) and becomes unreachable after \(v\) is removed.
In graph language, \(v\) dominates an initially reachable \(f\) relative to \(S\) when every directed path from \(S\) to \(f\) passes through \(v\). Paths of length zero are allowed in the reachability convention. Standard graph terminology is used throughout [4].
Theorem 16.4: Criticality equals domination
Assume \(f\) is reachable from \(S\). A node \(v\notin S\) is bridge critical for \(f\) if and only if \(v\) dominates \(f\) relative to \(S\).
Proof
If \(v\) dominates \(f\), every path from \(S\) to \(f\) uses \(v\). Removing \(v\) removes every such path, so \(f\) becomes unreachable. Conversely, if removing \(v\) makes \(f\) unreachable, then there could not have been a path from \(S\) to \(f\) avoiding \(v\). Therefore every path used \(v\), which is exactly domination.
Corollary 16.5: Weighted criticality
For \(v\notin S\), the utility lost by deleting \(v\) is the total weight of initially reachable future targets dominated by \(v\):
Deleted target vertices are counted as unreachable.
A node may have low verification value for the current theorem and high domination value for future targets. This is the precise form of the claim that a forgotten step can remain mathematically important after it has lost its role in the original certificate.