CircuitEncoding.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Truth-table encoding and substitution for residue circuits

Any decoded residue equality is a Boolean function of its block of bits. Its explicit disjunctive normal form has depth at most two and size at most 1 + 2^B (1+B). Substituting such forms into the actual circuit syntax increases depth by at most two and multiplies size by this bound.

def OAI.TwoPointCorrelations.AC0Circuit.substitute line 20

Source documentation

Replace each positive or negative input literal by a circuit.

def substitute {n m : ℕ} (σ : Fin n → Bool → AC0Circuit m) : AC0Circuit n → AC0Circuit m
  | .literal i positive => σ i positive
  | .andGate children => .andGate (fun i => substitute σ (children i))
  | .orGate children => .orGate (fun i => substitute σ (children i))

Mentions: OAI.TwoPointCorrelations.AC0Circuit

lemma OAI.TwoPointCorrelations.AC0Circuit.substitute_eval line 25
lemma OAI.TwoPointCorrelations.AC0Circuit.substitute_depth line 34
lemma OAI.TwoPointCorrelations.AC0Circuit.substitute_size line 56
def OAI.TwoPointCorrelations.AC0Circuit.assignmentTerm line 75
Source documentation
Conjunction specifying one assignment on a selected block of bits.
```
def assignmentTerm {n B : ℕ} (v : Fin B → Fin n) (z : BooleanCube B) : AC0Circuit n :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.AC0Circuit
def OAI.TwoPointCorrelations.AC0Circuit.falseCircuit line 79
Source documentation
The constant false circuit, used for rejected rows of a truth table.
```
def falseCircuit (n : ℕ) : AC0Circuit n := .orGate (fun i : Fin 0 => Fin.elim0 i)
```
Mentions: OAI.TwoPointCorrelations.AC0Circuit
lemma OAI.TwoPointCorrelations.AC0Circuit.literal_eval_true line 81
lemma OAI.TwoPointCorrelations.AC0Circuit.assignmentTerm_eval_true line 85
lemma OAI.TwoPointCorrelations.AC0Circuit.falseCircuit_eval line 98
def OAI.TwoPointCorrelations.AC0Circuit.truthTable line 102
Source documentation
Explicit DNF with one possible conjunction for each of the 2^B rows.
```
noncomputable def truthTable {n B : ℕ} (v : Fin B → Fin n)
    (F : BooleanCube B → Bool) : AC0Circuit n :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.AC0Circuit
lemma OAI.TwoPointCorrelations.AC0Circuit.truthTable_eval line 108
lemma OAI.TwoPointCorrelations.AC0Circuit.assignmentTerm_depth line 123
lemma OAI.TwoPointCorrelations.AC0Circuit.assignmentTerm_size line 126
lemma OAI.TwoPointCorrelations.AC0Circuit.truthTable_depth line 129
lemma OAI.TwoPointCorrelations.AC0Circuit.truthTable_size line 142
def OAI.TwoPointCorrelations.AC0Circuit.encodeInputs line 156
Source documentation
Encode each residue input using a truth table on its own selected bits.
```
noncomputable def encodeInputs {n m B : ℕ} (v : Fin n → Fin B → Fin m)
    (F : Fin n → BooleanCube B → Bool) (c : AC0Circuit n) : AC0Circuit m :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.AC0Circuit
lemma OAI.TwoPointCorrelations.AC0Circuit.encodeInputs_eval line 161
lemma OAI.TwoPointCorrelations.AC0Circuit.encodeInputs_depth line 168
lemma OAI.TwoPointCorrelations.AC0Circuit.encodeInputs_size line 173