RetrospectiveLists.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactQuantumFactoring.dataResidueGood_exists line 17
def OAI.ExactQuantumFactoring.dataGoodList line 31
lemma OAI.ExactQuantumFactoring.dataGoodList_correct line 34
lemma OAI.ExactQuantumFactoring.canonical_list_words line 45
Source documentation
The source canonical list has the CRT unit in the first field and zero in all remaining fields (including the final unused word).
```
lemma canonical_list_words {m n : ℕ} (hm : m≠0) (hb : m < 2^n) (p₀ : Component m) :
    ListSlots.canonical hm hb p₀=TransitionWords.encode
      (fun i : Fin (n^5) => natBasis n (if i.val=0 then (canonicalUnit hm p₀ : ZMod m).val else 0)) := by
…
```
Mentions: OAI.ExactQuantumFactoring.Component, OAI.ExactQuantumFactoring.ListSlots.canonical, OAI.ExactQuantumFactoring.TransitionWords.encode, OAI.ExactQuantumFactoring.canonicalUnit
def OAI.ExactQuantumFactoring.dataCanonicalList line 67
Source documentation
A direct fixed-field validator: read field zero, test its supplied-factor CRT congruences, and check every other field and the unused word is zero.
```
noncomputable def dataCanonicalList (data : FactorData) (m n : ℕ) (hn : 0<n)
    (y : Basis (Completion.transitionWidth n)) : Prop :=
…
```
Mentions: OAI.ExactQuantumFactoring.FactorData, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.Completion.transitionWidth
lemma OAI.ExactQuantumFactoring.basis_eq_natBasis line 73
lemma OAI.ExactQuantumFactoring.dataCanonicalList_correct line 84
def OAI.ExactQuantumFactoring.Completion.test line 110
Source documentation
Equivalent form of dyadic completion for a retrospective, data-based test of the guessed string. No canonical output is used during preparation.
```
def test {α : Type*} {W t d : ℕ} (good : α→Prop) (guessGood : Basis W→Prop)
    (s z : ℚ) (r : Raw α W t d) : Prop :=
…
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.Completion.Raw
lemma OAI.ExactQuantumFactoring.Completion.test_eq_passed line 114
def OAI.ExactQuantumFactoring.dataListPassed line 120
lemma OAI.ExactQuantumFactoring.dataListPassed_correct line 128
Source documentation
Same integer, same raw outcome, same retention coin. A verified occurrence record suffices even when the request is only a divisor of that occurrence.
```
lemma dataListPassed_correct {M n : ℕ} (hM : 0<M) (m : Basis n)
    (hm : 2 ≤ (bitsValue m).toNat) (hd : (bitsValue m).toNat∣M) (hn : 0<n)
    (r : PhysicalListSlots.Result n) :
    dataListPassed (trueData M) m hn r ↔
      PhysicalListSlots.passed m (by omega) (UniversalSplit.firstComponent hm) r := by
…
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.PhysicalListSlots.Result, OAI.ExactQuantumFactoring.dataListPassed, OAI.ExactQuantumFactoring.trueData, OAI.ExactQuantumFactoring.PhysicalListSlots.passed, OAI.ExactQuantumFactoring.UniversalSplit.firstComponent