CanonicalOperationDegree.lean

1 import RealizationBoundaries.ComputableNormalCodes
2 import RealizationBoundaries.OracleCopyOperations
3 
4 /-! # The exact oracle degree of the fixed natural-name addition operation -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace RealizationBoundaries
8 
9 /-- Fix the concrete canonical copy produced by the native normal-form construction. -/
10 def canonicalPairedCopy (a : ℕ → Bool) : OracleGroupCopy a (pairedGroup a) :=
11   pairedOracleCopy a a (TuringReducible.refl _)
12 
13 /-- The actual addition function on its fixed bijective natural names. -/
14 def canonicalPairedAddition (a : ℕ → Bool) (k : ℕ) : ℕ :=
15   (canonicalPairedCopy a).add k.unpair.1 k.unpair.2
16 
17 /-- This fixed operation, rather than only the abstract group's least copy degree,
18 has precisely the selector's oracle strength. -/
19 theorem canonicalPairedAddition_oracle_iff (a X : ℕ → Bool) :
20     OracleComputable X (canonicalPairedAddition a) ↔ SelectorReducible a X := by
21   constructor
22   · intro h
23     let c := canonicalPairedCopy a
24     let d : OracleGroupCopy X (pairedGroup a) :=
25       { names := c.names
26         zero := c.zero
27         add := c.add
28         zero_spec := c.zero_spec
29         add_spec := c.add_spec
30         add_computable := h }
31     exact oracle_unmarked_copy_reduces a X d
32   · intro ha
33     exact (canonicalPairedCopy a).add_computable.change_oracle ha
34 
35 end RealizationBoundaries

Back to source controls