CompanionBooleanKernel.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The actual Boolean phase row and its Metropolis comparison

The unused proposal words produce precisely a holding slowdown. Fresh weight estimates and the independent bounded coin contribute only their proved row error; no sampler-implementation hypothesis is used.

lemma OAI.ContingencyTables.CompanionBooleanPhase.word_probability line 26
lemma OAI.ContingencyTables.CompanionBooleanPhase.independent_decision line 33
lemma OAI.ContingencyTables.CompanionBooleanPhase.lazy_probability line 60

theorem OAI.ContingencyTables.CompanionBooleanPhase.transition_mass line 70

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) (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 → ℚ)
…

def OAI.ContingencyTables.CompanionBooleanPhase.referenceChain line 124
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) (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.CompanionBooleanPhase.State
lemma OAI.ContingencyTables.CompanionBooleanPhase.chain_eq line 130

theorem OAI.ContingencyTables.CompanionBooleanPhase.referenceChain_eq_completed line 141

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) (j : ℕ)
    (hp : 0<Fintype.card (Labels A)) (w : Pair A → Pair A → ℚ)
    (hw : ∀ p q,0<w p q) :
    referenceChain A j hp w hw=
      metropolisChain pairs PairedLabels.fresh (pairs_ne_nil A hp) PairedLabels.cover
        (fun p q => (w p q:ℝ))
        (DegreeCompletion.completeDegree (CompanionAnnealing.weight A j)
          (pairs : List ((Labels A×Bool)×(Labels A×Bool))).length)
        (fun p q => by exact_mod_cast hw p q)
        (DegreeCompletion.completeDegree_positive _ _ (actual_degree A j).1) := by
…

Mentions: OAI.ContingencyTables.CompanionBooleanPhase.referenceChain, OAI.ContingencyTables.PairedLabels.fresh, OAI.ContingencyTables.PairedLabels.cover, OAI.ContingencyTables.DegreeCompletion.completeDegree, OAI.ContingencyTables.CompanionAnnealing.weight, OAI.ContingencyTables.DegreeCompletion.completeDegree_positive

def OAI.ContingencyTables.CompanionBooleanPhase.targetChain line 166
theorem OAI.ContingencyTables.CompanionBooleanPhase.target_mass line 171
lemma OAI.ContingencyTables.CompanionBooleanPhase.distance_le_off_diagonal line 191
lemma OAI.ContingencyTables.CompanionBooleanPhase.average_abs line 204
theorem OAI.ContingencyTables.CompanionBooleanPhase.row_distance line 214
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) (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.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger
def OAI.ContingencyTables.CompanionBooleanPhase.pathLaw line 270
def OAI.ContingencyTables.CompanionBooleanPhase.targetPathMass line 278

theorem OAI.ContingencyTables.CompanionBooleanPhase.path_distance_bound line 287

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) (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.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger

def OAI.ContingencyTables.CompanionBooleanPhase.recordedWalk line 308
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) (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.CompanionBooleanPhase.State
theorem OAI.ContingencyTables.CompanionBooleanPhase.recordedWalk_law line 315