two_zpow_pos
The lemma asserts that 2 raised to any integer power remains strictly positive over the reals. Recognition Science authors cite it when constructing computable approximations for derived constants such as phi and alpha inverse. The proof reduces to a single invocation of the positivity tactic.
claimFor every integer $n$, the inequality $2^n > 0$ holds in the real numbers.
background
The declaration sits inside the module that resolves the classical-constructive tension in Recognition Science. The module distinguishes proof machinery (which may be classical) from output computability (which must remain algorithmic for constants). Reals are treated as the completion of rationals, so every real admits rational approximations of arbitrary precision; the lemma supplies the strict positivity needed to bound those approximations.
proof idea
The proof is a one-line wrapper that applies the positivity tactic. This tactic automatically discharges the goal once the base 2 and the exponent n are recognized as positive or integer, respectively.
why it matters in Recognition Science
The lemma feeds the rational_computable instance and the three surrounding Computable instances for reals, naturals, and integers. Those instances close the classical-constructive gap described in the module documentation by showing that Recognition Science constants remain computable reals. It thereby supports the broader claim that algorithmic accessibility holds independently of the classical logic used in the surrounding proofs.
scope and limits
- Does not establish computability for arbitrary real-valued functions.
- Does not remove noncomputable markers from Mathlib definitions.
- Applies only to the specific base 2 and integer exponents.
- Does not address convergence rates beyond the supplied epsilon.
Lean usage
instance (n : ℕ) : Computable (n : ℝ) where approx := ⟨fun _ => n, by intro k; simp only [Rat.cast_natCast, sub_self, abs_zero]; exact two_zpow_pos _⟩formal statement (Lean)
91lemma two_zpow_pos (n : ℤ) : (0 : ℝ) < (2 : ℝ) ^ n := by
proof body
Tactic-mode proof.
92 positivity
93
94/-! ## Classical approximation: every real has fast rational approximations
95
96`Real` in Mathlib is constructed as a completion of `ℚ`, so (classically) every
97real number admits rational approximations at any prescribed precision. This is
98enough to satisfy our existential `Computable` predicate. -/
99
100instance (x : ℝ) : Computable x where
101 approx := by
102 classical
103 refine ⟨fun n => Classical.choose (exists_rat_btwn (a := x - (2 : ℝ) ^ (-(n : ℤ)))
104 (b := x + (2 : ℝ) ^ (-(n : ℤ))) (by
105 have hpos : (0 : ℝ) < (2 : ℝ) ^ (-(n : ℤ)) := two_zpow_pos (-(n : ℤ))
106 linarith)), ?_⟩
107 intro n
108 -- Unpack the chosen rational bounds.
109 have hpos : (0 : ℝ) < (2 : ℝ) ^ (-(n : ℤ)) := two_zpow_pos (-(n : ℤ))
110 have hbtwn :=
111 Classical.choose_spec (exists_rat_btwn (a := x - (2 : ℝ) ^ (-(n : ℤ)))
112 (b := x + (2 : ℝ) ^ (-(n : ℤ))) (by linarith))
113 -- `hbtwn` gives: x - ε < q and q < x + ε.
114 have hleft : x - (Classical.choose (exists_rat_btwn (a := x - (2 : ℝ) ^ (-(n : ℤ)))
115 (b := x + (2 : ℝ) ^ (-(n : ℤ))) (by linarith)) : ℝ) < (2 : ℝ) ^ (-(n : ℤ)) := by
116 linarith [hbtwn.1]
117 have hright : -(2 : ℝ) ^ (-(n : ℤ)) < x - (Classical.choose (exists_rat_btwn
118 (a := x - (2 : ℝ) ^ (-(n : ℤ))) (b := x + (2 : ℝ) ^ (-(n : ℤ))) (by linarith)) : ℝ) := by
119 linarith [hbtwn.2]
120 have : |x - (Classical.choose (exists_rat_btwn
121 (a := x - (2 : ℝ) ^ (-(n : ℤ))) (b := x + (2 : ℝ) ^ (-(n : ℤ))) (by linarith)) : ℝ)|
122 < (2 : ℝ) ^ (-(n : ℤ)) := by
123 exact abs_lt.mpr ⟨hright, hleft⟩
124 simpa using this
125
126/-- Natural numbers are trivially computable. -/
127instance (n : ℕ) : Computable (n : ℝ) where
128 approx := ⟨fun _ => n, by
129 intro k
130 simp only [Rat.cast_natCast, sub_self, abs_zero]
131 exact two_zpow_pos _⟩
132
133/-- Integers are computable. -/
134instance (n : ℤ) : Computable (n : ℝ) where
135 approx := ⟨fun _ => n, by
136 intro k
137 simp only [Rat.cast_intCast, sub_self, abs_zero]
138 exact two_zpow_pos _⟩
139
140/-- Rationals are computable (constant approximation). -/