CompanionBooleanPhase.lean`

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The companion phase walk driven by disjoint bounded Boolean words

abbrev OAI.ContingencyTables.CompanionBooleanPhase.State line 19
def OAI.ContingencyTables.CompanionBooleanPhase.proposalBits line 21
lemma OAI.ContingencyTables.CompanionBooleanPhase.proposal_codes line 23
def OAI.ContingencyTables.CompanionBooleanPhase.proposal line 32
Source documentation
Each valid exchange neighbor has one code. Every unused code holds the current state; the full transition has another independent lazy bit.
```
def proposal (A : Instance I J) (S : State A) (bits : Fin (proposalBits A) → Bool) : Option (State A) :=
…
```
Mentions: OAI.ContingencyTables.CompanionBooleanPhase.State, OAI.ContingencyTables.CompanionBooleanPhase.proposalBits
lemma OAI.ContingencyTables.CompanionBooleanPhase.proposal_mass line 36
def OAI.ContingencyTables.CompanionBooleanPhase.stepBits line 42
def OAI.ContingencyTables.CompanionBooleanPhase.stepWordEquiv line 46
def OAI.ContingencyTables.CompanionBooleanPhase.step line 56
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) (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 → ℚ)
…
```
theorem OAI.ContingencyTables.CompanionBooleanPhase.step_eq_iff line 72
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) (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 → ℚ)
…
```
def OAI.ContingencyTables.CompanionBooleanPhase.transitionLaw line 99
def OAI.ContingencyTables.CompanionBooleanPhase.walk line 106
theorem OAI.ContingencyTables.CompanionBooleanPhase.walk_law line 115
Source documentation
The actual flattened word gives independent repeated transitions; its law follows from the finite-word walk construction.
```
theorem walk_law (A : Instance I J) (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.CompanionBooleanPhase.State
lemma OAI.ContingencyTables.CompanionBooleanPhase.dyadic_size_le_twice line 125
def OAI.ContingencyTables.CompanionBooleanPhase.slowdown line 139
theorem OAI.ContingencyTables.CompanionBooleanPhase.slowdown_bounds line 144
Source documentation
The unused proposal codes slow the source chain by at most two; they do not change its stationary law.
```
theorem slowdown_bounds (A : Instance I J) (hp : 0 < Fintype.card (Labels A)) :
    (1/2:ℝ) ≤ slowdown A ∧ slowdown A ≤ 1 := by
…
```
Mentions: OAI.ContingencyTables.CompanionBooleanPhase.slowdown