OAI/Analysis/CircleDomains/Probability/PriorPositiveBarrierLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full positive code law from failure of a small compatible barrier. The countable extraction is invoked for every fusion test; the final law keeps the quantitative occupation, fixed-mark visit, and tuple bounds.

  1. theorem OAI.CircleDomainRigidity.positive_code_law_of_no_small_level_barrier line 22