TreeReadOnly.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactQuantumFactoring.parallelProgram_prefix_target line 19
Source documentation
Parallel fresh work does not alter the prefix protected by the left program.
```
lemma parallelProgram_prefix_target {p q n : ℕ} (P : List (Instruction p))
    (Q : List (Instruction q)) (hn : n≤p) (hP : ∀ o∈P,n≤o.target.val) :
    ∀ o∈parallelProgram P Q,n≤o.target.val := by
…
```
Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.parallelProgram
lemma OAI.ExactQuantumFactoring.parallelProgram_interval_target line 34
Source documentation
The branch register preceding an otherwise read-only prefix introduces only targets before that prefix, never in it.
```
lemma parallelProgram_interval_target {p q n : ℕ} (P : List (Instruction p))
    (Q : List (Instruction q)) (hQ : ∀ o∈Q,n≤o.target.val) :
    ∀ o∈parallelProgram P Q,o.target.val<p ∨ p+n≤o.target.val := by
…
```
Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.parallelProgram
lemma OAI.ExactQuantumFactoring.PhysicalTree.paddedProgram_prefix_target line 45
lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterProgram_interval_target line 51
def OAI.ExactQuantumFactoring.PhysicalTree.inputWires line 61
Source documentation
The original input is the n-wire interval immediately following the fresh branch coin. This definition is independent of N.
```
def inputWires (n : ℕ) : Finset (Fin (quarterWidth n)) :=
…
```
Mentions: OAI.ExactQuantumFactoring.PhysicalTree.quarterWidth
lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterProgram_readOnly line 64
lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterProgram_respects_input line 71
Source documentation
This is global input invariance, not merely a clean-input statement.
```
lemma quarterProgram_respects_input (n N : ℕ) :
    RespectsSector (inputSector (inputWires n) (quarterZero n N)) (programMatrix (quarterProgram n)) :=
…
```
Mentions: OAI.ExactQuantumFactoring.RespectsSector, OAI.ExactQuantumFactoring.inputSector, OAI.ExactQuantumFactoring.PhysicalTree.inputWires, OAI.ExactQuantumFactoring.PhysicalTree.quarterZero, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.PhysicalTree.quarterProgram