CompanionCanonicalEncoding.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A common explicit encoding for initialization and proposals

Cells follow cellEnum, their copies follow increasing finite indices, and each copy contributes its false and true coordinates consecutively. The polynomial initializer computes exactly this encoding of the actual initial draw. The same order may therefore be used by the proposal scan.

def OAI.ContingencyTables.CompanionCanonicalEncoding.copyEquiv line 25
def OAI.ContingencyTables.CompanionCanonicalEncoding.pairEquiv line 28
def OAI.ContingencyTables.CompanionCanonicalEncoding.coordinateOrder line 31
lemma OAI.ContingencyTables.CompanionCanonicalEncoding.encodeSet_reindex line 35
lemma OAI.ContingencyTables.CompanionCanonicalEncoding.initial_preimage line 42
Source documentation
Reindexing the physical initial draw gives the independent cell choices used by the actual list initializer.
```
lemma initial_preimage (A : Instance I J) (B : ℕ)
    (bits : Fin (initialBits A B) → Bool) :
    (pairEquiv A).symm ⁻¹' (draw A B bits).val.val=
      encode (cellCapacity A) (drawChoices (cellCapacity A) B bits) := by
…
```
Mentions: OAI.ContingencyTables.CompanionCanonicalEncoding.pairEquiv
theorem OAI.ContingencyTables.CompanionCanonicalEncoding.initialCode_eq line 63
Source documentation
The polynomial binary initializer emits precisely the code of the literal PlainIndex output with its distributional error bound.
```
theorem initialCode_eq (A : Instance I J) (B : ℕ) (hB : 0<B)
    (bits : Fin (initialBits A B) → Bool) :
    CanonicalInitialEncoding.initialCode ((List.ofFn (cellCapacity A),B),List.ofFn bits)=
      encodeSet (coordinateOrder A) (draw A B bits).val.val := by
…
```
Mentions: OAI.ContingencyTables.CanonicalInitialEncoding.initialCode, OAI.ContingencyTables.CompanionCanonicalEncoding.coordinateOrder
theorem OAI.ContingencyTables.CompanionCanonicalEncoding.canonicalProposal_law line 72
Source documentation
The canonical initializer encoding can be fed directly to an arithmetic proposal with the same dyadic transition law.
```
theorem canonicalProposal_law (A : Instance I J) (S : CompanionBooleanPhase.State A) :
    FirstSuccess.mapLaw
      (FirstSuccess.uniformLaw (α := Fin (CompanionBooleanPhase.proposalBits A) → Bool))
…
```
Mentions: OAI.ContingencyTables.CompanionBooleanPhase.State, OAI.ContingencyTables.FirstSuccess.mapLaw, OAI.ContingencyTables.FirstSuccess.uniformLaw, OAI.ContingencyTables.CompanionBooleanPhase.proposalBits