Lean proof spine

Spine II: Value bundles and goal transport

Source: context/lean_proof_graphs/02-value-transport.dot

Rendered with Graphviz (same sources as the book). Click a node for details; sub-spine boxes (Spine I–IV) open the matching sub-diagram.

Nodes in this graph

P14 Bundle factorization (proof)
P15 Policy ≠ geometry (proof)
P17 Labels ≠ bearer map (proof)
P18 Marginals ≠ tradeoffs (proof)
P20 Intentional MDL gain (proof)
P21 Transport gain (proof)
P22a Full ⇒ semantic transport (proof)
P22b Semantic ≠ full transport (proof)
P37 Goal laundering (proof)
MB2 Bundle identifiability (bridge)
MB3 Bearer import (bridge)
Exports: BundleTransport, BearerTransport, transport / laundering counterexamples (other)
P16 (proof)
P19 (proof)
FCIRL (other)