RootedBooleanPhase.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual finite-word Metropolis steps using the selected-root oracle

def OAI.ContingencyTables.RootedBooleanPhase.step line 20
Source documentation
The realized step evaluates the current and proposed weights from separate words, then uses a third independent word for its rational coin.
```
def step (A : Instance I J) (R : RootedCompletion.Selection A.T) (C K j k : ℕ)
    (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (xi : ℚ)
    (v : Grid (I := Fin (dimension A)) K) (w : Pair A → Pair A → ℚ)
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection
theorem OAI.ContingencyTables.RootedBooleanPhase.step_eq_iff line 36
Source documentation
A nontrivial move uses exactly its proposal code and the fresh acceptance experiment. Failed codes and the independent holding bit contribute only to the diagonal.
```
theorem step_eq_iff (A : Instance I J) (R : RootedCompletion.Selection A.T) (C K j k : ℕ)
    (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (xi : ℚ)
    (v : Grid (I := Fin (dimension A)) K) (w : Pair A → Pair A → ℚ)
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection
def OAI.ContingencyTables.RootedBooleanPhase.transitionLaw line 63
def OAI.ContingencyTables.RootedBooleanPhase.walk line 70
theorem OAI.ContingencyTables.RootedBooleanPhase.walk_law line 79
Source documentation
The actual flattened word gives independent repeated transitions; its law follows from the accepted finite-word walk construction.
```
theorem walk_law (A : Instance I J) (R : RootedCompletion.Selection A.T) (C K j k n : ℕ)
    (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (xi : ℚ)
    (v : Grid (I := Fin (dimension A)) K) (w : Pair A → Pair A → ℚ) (S : State A) :
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection