PhysicalMachineMass.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.SplitMachine.passed line 23
Source documentation
Filtering the actual chronological query at each clock tick. No collection of answers for unselected/counterfactual moduli occurs in this predicate.
```
noncomputable def passed (x : Basis c) : (t : ℕ)→Trace n t→Prop
  | 0,_=>True
  | t+1,h=>passed x t h.1 ∧ UniversalSplit.passed (M.query.eval (M.config x t h.1)) h.2
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.SplitMachine.Trace, OAI.ExactQuantumFactoring.UniversalSplit.passed
lemma OAI.ExactQuantumFactoring.SplitMachine.state_normalized line 27
theorem OAI.ExactQuantumFactoring.SplitMachine.passed_mass line 38
Source documentation
Exact physical-history probability for a clocked network controller. This is unconditional in its update network and retains all quantum scratch.
```
theorem passed_mass (hn : 128≤n) (x : Basis c) (t : ℕ) :
    outcomeMass (M.passed x t) (M.state x t)=
      ((Completion.target n:ℝ)^(n^5+1))^t := by
…
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.Completion.target
def OAI.ExactQuantumFactoring.SplitMachine.physicalPassed line 57
Source documentation
The on-support passing event in the retained concrete physical registers. An efficient retrospective Boolean validator is still needed before using it as a circuit-controlled phase; this definition does not provide one by fiat.
```
noncomputable def physicalPassed (x : Basis c) (t : ℕ) (z : Basis (M.width t)) : Prop :=
…
```
Mentions: OAI.ExactQuantumFactoring.Basis
lemma OAI.ExactQuantumFactoring.SplitMachine.physicalPassed_encoded line 60
theorem OAI.ExactQuantumFactoring.SplitMachine.program_passed_mass line 67