primorial_one
plain-language theorem explainer
The declaration establishes that the primorial of 1 equals 2. Number theorists constructing initial prime products within the Recognition Science arithmetic layer would cite this as the base case. The proof reduces immediately to reflexivity on the definitional equality.
Claim. $ primorial(1) = 2 $
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for Dirichlet inversion. Statements remain minimal to permit later addition of deeper algebraic layers. No upstream lemmas are required for this base equality.
proof idea
The proof is a one-line term that applies reflexivity to the definitional equality.
why it matters
This supplies the initial value for primorial constructions that feed into prime-product arguments in the number-theory component of the monolith. It precedes application of Möbius or squarefree predicates. No downstream uses or open questions are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.