two_zpow_pos
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.