OAI/Analysis/CircleDomains/Selection/TrueChainConcatenation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite chain containing only true paths concatenates to one allowed true path with exactly the same full cost. This supplies the initial stage.

  1. theorem OAI.CircleDomainRigidity.exists_path_of_true_paid_chain line 21