PhysicalHistory.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.prefixWires line 22
Source documentation
Every previously retained bit, not merely the original N, is read-only for an appended fresh transition. The transition may use them as controls.
```
def prefixWires (p q : ℕ) : Finset (Fin (p+q)) := Finset.univ.filter (fun i => i.val<p)
```
lemma OAI.ExactQuantumFactoring.append_prefix_sector line 24
def OAI.ExactQuantumFactoring.freshColumn line 38
theorem OAI.ExactQuantumFactoring.retained_column line 44
Source documentation
Actual gate program, sector by sector. All unused/tail amplitudes are kept: this is not a normalized conditional state or a measurement hypothesis.
```
theorem retained_column {p q : ℕ} (P : List (Instruction (p+q)))
    (hP : ReadOnly (prefixWires p q) P) (h : Basis p) (z : Basis q) :
    (programMatrix P).mulVec (basisVector (Fin.append h z))=
      encodeState (fun y => Fin.append h y) (freshColumn P z h) := by
…
```
Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.ReadOnly, OAI.ExactQuantumFactoring.prefixWires, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.freshColumn
theorem OAI.ExactQuantumFactoring.retained_step line 73
Source documentation
Coherent retained-work lemma used at every adaptive slot. A single actual fixed-gate P acts correctly on an arbitrary (possibly entangled) old history.
```
theorem retained_step {p q : ℕ} (P : List (Instruction (p+q)))
    (hP : ReadOnly (prefixWires p q) P) (z : Basis q) (ψ : Basis p→ℂ) :
    (programMatrix P).mulVec (encodeState (fun h => Fin.append h z) ψ)=
      encodeState (appendEquiv p q) (RecordedHistory.appendState ψ (freshColumn P z)) := by
…
```
Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.ReadOnly, OAI.ExactQuantumFactoring.prefixWires, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.appendEquiv, OAI.ExactQuantumFactoring.RecordedHistory.appendState, OAI.ExactQuantumFactoring.freshColumn
theorem OAI.ExactQuantumFactoring.freshColumn_normalized line 91
Source documentation
Each fresh column is normalized automatically by the verified unitary gate semantics, even when no local transition succeeds.
```
theorem freshColumn_normalized {p q : ℕ} (P : List (Instruction (p+q)))
    (hP : ReadOnly (prefixWires p q) P) (z : Basis q) (h : Basis p) :
    ∑ y,Complex.normSq (freshColumn P z h y)=1 := by
…
```
Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.ReadOnly, OAI.ExactQuantumFactoring.prefixWires, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.freshColumn
theorem OAI.ExactQuantumFactoring.retained_constant_mass line 105
Source documentation
Constant passing mass for an actual read-only physical transition on an arbitrary superposition of retained histories. The test is on the same output registers; no collapse or conditional renormalization is used.
```
theorem retained_constant_mass {p q : ℕ} (P : List (Instruction (p+q)))
    (hP : ReadOnly (prefixWires p q) P) (z : Basis q) (ψ : Basis p→ℂ)
    (passed : Basis p→Prop) (pass : Basis p→Basis q→Prop) (a : ℝ)
    (hlocal : ∀ h, passed h → outcomeMass (pass h) (freshColumn P z h)=a) :
    outcomeMass (fun x => let hy := (appendEquiv p q).symm x
…
```
Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.ReadOnly, OAI.ExactQuantumFactoring.prefixWires, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.freshColumn, OAI.ExactQuantumFactoring.appendEquiv