RecordedHistory.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The same-history deferred-filter argument of Section 6, at the level of finite complex amplitudes with all old registers retained. These are proved lemmas for the main construction, not assumptions replacing that construction.

def OAI.ExactQuantumFactoring.RecordedHistory.appendState line 18
Source documentation
A fresh controlled computation appends a register, retaining the old one.
```
noncomputable def appendState {H Y : Type*} (ψ : H → ℂ) (fresh : H → Y → ℂ) : H × Y → ℂ :=
…
```
lemma OAI.ExactQuantumFactoring.RecordedHistory.append_mass line 21

lemma OAI.ExactQuantumFactoring.RecordedHistory.append_constant_mass line 41

Source documentation

The normalized state of idle old work need not be known; exact local mass on each passing passed suffices. No conditioning on future verification occurs.

lemma append_constant_mass {H Y : Type*} [Fintype H] [Fintype Y]
    (ψ : H → ℂ) (fresh : H → Y → ℂ) (passed : H → Prop) (pass : H → Y → Prop)
    (z : ℝ) (hlocal : ∀ h, passed h → outcomeMass (pass h) (fresh h) = z) :
    outcomeMass (fun hy : H × Y => passed hy.1 ∧ pass hy.1 hy.2) (appendState ψ fresh) =
      outcomeMass passed ψ * z := by
…

Mentions: OAI.ExactQuantumFactoring.RecordedHistory.appendState

lemma OAI.ExactQuantumFactoring.RecordedHistory.append_normalized line 58
abbrev OAI.ExactQuantumFactoring.RecordedHistory.History line 68
Source documentation
An ordered history, stored with the most recent outcome first.
```
abbrev History (Y : Type*) (t : ℕ) := Fin t → Y
```
def OAI.ExactQuantumFactoring.RecordedHistory.historyState line 70
def OAI.ExactQuantumFactoring.RecordedHistory.historyPass line 75
lemma OAI.ExactQuantumFactoring.RecordedHistory.outcomeMass_equiv line 80
lemma OAI.ExactQuantumFactoring.RecordedHistory.history_mass line 89
Source documentation
Exactly z at every passing history gives exactly z^L, including all padded slots. The hypotheses are local unconditioned fresh-register laws, not an assumption about eventual successful completion.
```
lemma history_mass {Y : Type*} [Fintype Y]
    (fresh : ∀ t, History Y t → Y → ℂ)
    (pass : ∀ t, History Y t → Y → Prop) (z : ℝ)
    (hlocal : ∀ t h, historyPass pass t h → outcomeMass (pass t h) (fresh t h) = z) :
    ∀ L, outcomeMass (historyPass pass L) (historyState fresh L) = z^L := by
…
```
Mentions: OAI.ExactQuantumFactoring.RecordedHistory.History, OAI.ExactQuantumFactoring.RecordedHistory.historyPass, OAI.ExactQuantumFactoring.RecordedHistory.historyState

lemma OAI.ExactQuantumFactoring.RecordedHistory.deferred_event_eq line 108

Source documentation

The two filters are evaluated on the SAME recorded outcome and coins. This proposition is independent of any stochastic representation of the runs.

lemma deferred_event_eq {Run Data : Type*} (trueData : Data)
    (produced : Run → Option Data) (verified : Run → Prop)
    (tests : Data → Run → Prop)
    (hallGood : ∀ r, tests trueData r → produced r = some trueData ∧ verified r)
    (hunique : ∀ r d, produced r = some d → verified r → d = trueData) :
    (fun r => ∃ d, produced r = some d ∧ verified r ∧ tests d r) =
      (fun r => tests trueData r) := by
…

Mentions: OAI.ExactQuantumFactoring.trueData

lemma OAI.ExactQuantumFactoring.RecordedHistory.deferred_mass_eq line 123