two_zpow_pos
plain-language theorem explainer
The lemma shows that 2 raised to any integer power remains strictly positive in the reals. Authors constructing Computable instances for reals, integers, and rationals in the constructive-logic discussion cite it to justify error bounds. The proof reduces in one step to the positivity tactic.
Claim. For every integer $n$, $2^n > 0$ holds in the real numbers.
background
The ConstructiveNote module separates classical proof machinery from the computability of derived constants. It defines the Computable predicate via an approx field that supplies rational approximations inside an error of $2^{-k}$. The local setting is the claim that Turing computability of outputs such as φ and α^{-1} survives classical axioms in the proof layer.
proof idea
The proof is a one-line wrapper that applies the positivity tactic.
why it matters
The lemma supplies the positivity fact required by the rational_computable instance, which demonstrates constant rational approximations. It therefore supports the module's resolution that RS constants remain computable. The result touches the framework distinction between proof style and output computability without engaging the J-cost or phi-ladder structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.