totient_twohundredten
plain-language theorem explainer
The theorem asserts that Euler's totient function applied to 210 equals 48. Number theorists inside the Recognition Science framework would cite this value when evaluating arithmetic invariants for 210 = 2·3·5·7. The proof is a one-line native decision that directly evaluates the totient definition.
Claim. $varphi(210) = 48$, where $varphi$ is Euler's totient function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the totient. The totient wrapper is defined directly as the standard natural-number totient. Upstream results include the J-cost structure from PhiForcingDerived, the ledger factorization from DAlembert, and the spectral emergence structure whose doc-comment states that |Aut(Q3)| = 48 total fermionic degrees of freedom.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the totient at 210.
why it matters
This concrete evaluation supplies an arithmetic fact that aligns with the 48 appearing in the spectral emergence structure as the count of fermionic degrees of freedom. It sits in the arithmetic-functions layer without advancing the forcing chain or phi-ladder steps. No downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.