CompanionCappedReturnProgram.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Binary program for a total capped return

The strict return scan is followed by the supplied initial code on a missing return. Both operations have polynomial binary realizers.

def OAI.ContingencyTables.CompanionCappedReturnProgram.optionDefault line 20
def OAI.ContingencyTables.CompanionCappedReturnProgram.optionDefaultRealizer line 22
theorem OAI.ContingencyTables.CompanionCappedReturnProgram.polynomial_optionDefault line 26
abbrev OAI.ContingencyTables.CompanionCappedReturnProgram.TotalReturnInput line 31
def OAI.ContingencyTables.CompanionCappedReturnProgram.totalReturnCode line 33
def OAI.ContingencyTables.CompanionCappedReturnProgram.totalReturnCodeRealizer line 36
theorem OAI.ContingencyTables.CompanionCappedReturnProgram.polynomial_totalReturnCode line 39

theorem OAI.ContingencyTables.CompanionCappedReturnProgram.totalReturnCode_encode line 47

Source documentation

The binary result is the encoding of the same defaulted first return.

theorem totalReturnCode_encode (A : Instance I J)
    (S : PlainIndex (TwoLiftStates.pairs : List (Pair A))) (xs : List (State A)) :
    totalReturnCode ((pairCatalog A,xs.map (fun T => encodeSet (coordinateEquiv A) T.val)),
      encodeSet (coordinateEquiv A) S.val.val)=
      encodeSet (coordinateEquiv A)
        (returnDefault (plainPredicate TwoLiftStates.pairs) S xs).val.val := by
…

Mentions: OAI.ContingencyTables.TwoLiftStates.pairs, OAI.ContingencyTables.CompanionCappedReturnProgram.totalReturnCode

theorem OAI.ContingencyTables.CompanionCappedReturnProgram.totalReturnCode_recorded line 60
Source documentation
In particular the program computes the literal finite-word return experiment, not an independently specified trace sampler.
```
theorem totalReturnCode_recorded (A : Instance I J) (C K j k n : ℕ)
    (hK : 1≤K) (hW : 100*A.d*K≤A.W) (xi : ℚ)
    (v : Grid (I := Fin (CompanionOracleDensity.dimension A)) K)
…
```
Mentions: OAI.ContingencyTables.CompanionOracleDensity.dimension