RootedBooleanKernel.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Selected-root Boolean row law and full-history perturbation

lemma OAI.ContingencyTables.RootedBooleanPhase.word_probability line 25
lemma OAI.ContingencyTables.RootedBooleanPhase.independent_decision line 32
lemma OAI.ContingencyTables.RootedBooleanPhase.lazy_probability line 59

theorem OAI.ContingencyTables.RootedBooleanPhase.transition_mass line 69

Source documentation

Every nontrivial output probability factors into its lazy bit, unique neighbor code, and the actual rounded two-oracle acceptance.

theorem transition_mass (A : Instance I J) (R : RootedCompletion.Selection A.T) (C : ℕ) (hC : 0<C) (K j k : ℕ)
    (hK : 1≤K) (hW : 100*A.d*K≤A.W) (hB : (K:ℝ)=binWidth A C)
    (hj : j≤rationalHeight A C) (xi : ℚ) (hx0 : 0<xi) (hx1 : xi<1)
    (v : Grid (I := Fin (dimension A)) K) (w : Pair A → Pair A → ℚ)
…

Mentions: OAI.ContingencyTables.RootedCompletion.Selection

def OAI.ContingencyTables.RootedBooleanPhase.referenceChain line 123
Source documentation
The exact target row is the source Metropolis chain, slowed by its dyadic neighbor-code padding. The stationary distribution is unchanged.
```
def referenceChain (A : Instance I J) (R : RootedCompletion.Selection A.T) (j : ℕ) (hp : 0<Fintype.card (Labels A))
    (w : Pair A → Pair A → ℚ) (hw : ∀ p q,0<w p q) : FiniteChain (State A) :=
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection
lemma OAI.ContingencyTables.RootedBooleanPhase.chain_eq line 129
theorem OAI.ContingencyTables.RootedBooleanPhase.referenceChain_eq_completed line 140
Source documentation
The degree completion used to prove the signature and concentration theorems leaves every state and transition of the literal chain intact.
```
theorem referenceChain_eq_completed (A : Instance I J) (R : RootedCompletion.Selection A.T) (j : ℕ)
    (hp : 0<Fintype.card (Labels A)) (w : Pair A → Pair A → ℚ)
    (hw : ∀ p q,0<w p q) :
    referenceChain A R j hp w hw=
      metropolisChain pairs PairedLabels.fresh (pairs_ne_nil A hp) PairedLabels.cover
        (fun p q => (w p q:ℝ))
        (DegreeCompletion.completeDegree (RootedAnnealing.weight A R j)
          (pairs : List ((Labels A×Bool)×(Labels A×Bool))).length)
        (fun p q => by exact_mod_cast hw p q)
        (DegreeCompletion.completeDegree_positive _ _ (RootedWarmStart.actual_degree A R j).1) := by
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedBooleanPhase.referenceChain, OAI.ContingencyTables.PairedLabels.fresh, OAI.ContingencyTables.PairedLabels.cover, OAI.ContingencyTables.DegreeCompletion.completeDegree, OAI.ContingencyTables.RootedAnnealing.weight, OAI.ContingencyTables.DegreeCompletion.completeDegree_positive, OAI.ContingencyTables.RootedWarmStart.actual_degree
def OAI.ContingencyTables.RootedBooleanPhase.targetChain line 165
theorem OAI.ContingencyTables.RootedBooleanPhase.target_mass line 170
lemma OAI.ContingencyTables.RootedBooleanPhase.distance_le_off_diagonal line 190
lemma OAI.ContingencyTables.RootedBooleanPhase.average_abs line 203
theorem OAI.ContingencyTables.RootedBooleanPhase.row_distance line 213
Source documentation
The complete transition row loses at most half the acceptance error. The diagonal is controlled by conservation of probability, rather than an additional independent error assumption.
```
theorem row_distance (A : Instance I J) (R : RootedCompletion.Selection A.T) (C : ℕ) (hC : 0<C) (K j k : ℕ)
    (hK : 1≤K) (hW : 100*A.d*K≤A.W) (hB : (K:ℝ)=binWidth A C)
    (hj : j≤rationalHeight A C) (xi : ℚ) (hx0 : 0<xi) (hx1 : xi≤1/4)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger
def OAI.ContingencyTables.RootedBooleanPhase.pathLaw line 269
def OAI.ContingencyTables.RootedBooleanPhase.targetPathMass line 277

theorem OAI.ContingencyTables.RootedBooleanPhase.path_distance_bound line 286

Source documentation

The error controls the whole recorded phase history, not merely its last state. Every step uses a disjoint fresh oracle/acceptance word.

theorem path_distance_bound (A : Instance I J) (R : RootedCompletion.Selection A.T) (C : ℕ) (hC : 0<C) (K j k : ℕ)
    (hK : 1≤K) (hW : 100*A.d*K≤A.W) (hB : (K:ℝ)=binWidth A C)
    (hj : j≤rationalHeight A C) (xi : ℚ) (hx0 : 0<xi) (hx1 : xi≤1/4)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…

Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger

def OAI.ContingencyTables.RootedBooleanPhase.recordedWalk line 307
Source documentation
The same finite step word records the newly sampled state, so the history law is physically realized by the concatenated step words.
```
def recordedWalk (A : Instance I J) (R : RootedCompletion.Selection A.T) (C K j k N 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
theorem OAI.ContingencyTables.RootedBooleanPhase.recordedWalk_law line 314