PhysicalTreeMass.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.NodeMachine.passed line 22
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 ∧ NodeKernel.passed (M.query.eval (M.config x t h.1)) h.2
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.NodeKernel.passed
lemma OAI.ExactQuantumFactoring.NodeMachine.state_normalized line 26
theorem OAI.ExactQuantumFactoring.NodeMachine.passed_mass line 37
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))^(2*n))^t := by
…
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.Completion.target
def OAI.ExactQuantumFactoring.NodeMachine.physicalPassed line 56
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.NodeMachine.physicalPassed_encoded line 59
theorem OAI.ExactQuantumFactoring.NodeMachine.program_passed_mass line 66