totient_pos
plain-language theorem explainer
The theorem establishes that Euler's totient function is strictly positive for every positive integer. Number theorists building arithmetic-function tools inside the Recognition Science number-theory layer would cite this result before applying inversion formulas or counting arguments. The proof is a direct term-mode reduction that unfolds the local wrapper and invokes the standard positivity fact from the underlying library.
Claim. For every positive integer $n$, the Euler totient function satisfies $0 < ϕ(n)$.
background
The declaration lives in the module that supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for later Dirichlet algebra. The totient wrapper is defined simply as totient n := Nat.totient n. The upstream structure for from UniversalForcingSelfReference records structural properties required for meta-realization and self-reference axioms, though it is not invoked inside this particular positivity statement.
proof idea
The proof is a one-line wrapper. It simplifies using the definition of totient to expose the Mathlib predicate, then applies Nat.totient_pos.mpr directly to the hypothesis that n is positive.
why it matters
This result is the direct parent of the equivalence totient_pos_iff that appears immediately afterward in the same file. It supplies the basic positivity claim needed for safe use of totient in prime-related counting within the Recognition Science arithmetic-functions scaffolding. No direct connection to the forcing chain T0-T8 or the phi-ladder is present, but the lemma stabilizes the number-theory interface that may later support mass formulas or other applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.