theorem proved term proof

`eulerDet2FactorComplex_ne_zero`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 462theorem eulerDet2FactorComplex_ne_zero {s : ℂ} (hs : 0 < s.re)
 463    (p : Nat.Primes) :
 464    eulerDet2FactorComplex p s ≠ 0 := by

proof body

Term-mode proof.

 465  unfold eulerDet2FactorComplex
 466  refine mul_ne_zero ?_ (Complex.exp_ne_zero _)
 467  exact one_sub_eulerPrimePowerComplex_ne_zero hs p
 468
 469/-- Away from the pole at `1` and away from zeros of `ζ`, the reciprocal zeta
 470function is genuinely holomorphic. This gives the actual analytic object that a
 471future phase-lift witness should sample on circles. -/

depends on (21)

Lean names referenced from this declaration's body.

reciprocal in IndisputableMonolith.Algebra.CostAlgebra decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
phase in IndisputableMonolith.Foundation.EightTick decl_use
reciprocal in IndisputableMonolith.Foundation.LedgerForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
future in IndisputableMonolith.Foundation.TimeEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
eulerDet2FactorComplex in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
one_sub_eulerPrimePowerComplex_ne_zero in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
Primes in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
zeta in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use