External formalization bridge · P0
GapEntropy → BanditRLlib graph slice
Externally kernel-checked declarations are mapped against BanditRLlib's BAI, probability and information-theoretic routes without being promoted to local proof dependencies.
Verification boundary. The external project is frozen at a pinned commit and uses a different Lean toolchain. External/source nodes and conceptual-overlap edges remain overlays; only BanditRLlib's own compiled nodes inherit local verification status.
Loading graph…
No matching branch is visible.
Edge semantics
External theorem-internal dependencies are source evidence inside the external slice. Links from BanditRLlib probability/information routes to external nodes are explicitly conceptual-overlap or frontier-closure edges, not imports. A future local port must reclassify each edge as exact reuse, adapter-needed, new local lemma, or conceptual only.