module module high

`IndisputableMonolith.NumberTheory.EulerInstantiation`

EulerInstantiation supplies the set of primes as a subset of the naturals together with prime sums and Hilbert-Schmidt norms that instantiate the real-axis Euler carrier for the Recognition Science zeta construction. Analytic-trace and RH-bridge modules cite it for the concrete arithmetic data. The module consists entirely of definitions and supporting lemmas with no top-level theorem.

claimLet $\mathbb{P} \subset \mathbb{N}$ be the set of prime numbers. The module also introduces the prime-sum function over $\mathbb{P}$ and the squared Hilbert-Schmidt norm on the associated carrier operator.

background

The module sits inside the NumberTheory domain and imports the RS time quantum $\tau_0$, the J-cost framework, annular sampling, and the cost-covering bridge. Its immediate purpose is to realize the real-axis Euler product that EulerCarrierComplex later lifts to the half-plane Re$(s) > 1/2$. The supplied doc-comment identifies the central object as the set of primes inside $\mathbb{N}$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the arithmetic foundation consumed by AnalyticTrace, ArgumentPrincipleProved, CarrierBudgetComparison, ConcreteEulerLedger, ZetaLedgerBridge, and UnifiedRH. These modules use the prime data to eliminate former axioms and close the ledger-to-zeta identification required for the T1-bounded realizability architecture.

scope and limits

Does not define or prove properties of the Riemann zeta function itself.
Does not contain the complex-analytic Euler carrier.
Does not address defect sampling or annular cost bounds.
Does not implement the argument principle or contour integration.

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NumberTheory.AnalyticTrace module_import
IndisputableMonolith.NumberTheory.ArgumentPrincipleProved module_import
IndisputableMonolith.NumberTheory.CarrierBudgetComparison module_import
IndisputableMonolith.NumberTheory.ConcreteEulerLedger module_import
IndisputableMonolith.NumberTheory.ZetaLedgerBridge module_import
IndisputableMonolith.Unification.UnifiedRH module_import

depends on (7)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.NumberTheory.AnnularCost module_import
IndisputableMonolith.NumberTheory.CostCoveringBridge module_import
IndisputableMonolith.NumberTheory.DefectSampledTrace module_import
IndisputableMonolith.NumberTheory.EulerCarrierComplex module_import
IndisputableMonolith.NumberTheory.SampledTrace module_import

declarations in this module (81)

def Primes L56
def PrimeSum L60
def HilbertSchmidtNormSq L66
theorem hilbert_schmidt_convergent L72
theorem eigenvalue_lt_one L78
theorem eigenvalue_pos L85
def det2Factor L94
def det2LogFactor L101
theorem det2_log_factor_bound L107
theorem det2_log_summable L134
theorem det2_product_convergent L175
def carrierLog L184
def carrierValue L189
theorem carrier_log_convergent L193
theorem carrier_pos L198
theorem carrier_nonvanishing L206
def carrierDerivTerm L215
def carrierDerivBound L220
theorem carrierDerivTerm_nonneg L224
theorem carrierDerivBound_summable L241
theorem carrierDerivBound_finite L298
theorem carrierDerivBound_pos L302
theorem carrier_zeta_identity L324
theorem zeros_in_continuation L333
def primeLog L342
def eulerPrimePowerComplex L347
def eulerDet2FactorComplex L352
def eulerPrimeLogDerivTermComplex L358
def zetaReciprocal L364
def defectSensorCenter L370
def defectSensorCirclePoint L376
def zetaReciprocalOnSensorCircle L380
theorem defectSensorCirclePoint_re L385
theorem defectSensorCirclePoint_mem_strip L392
theorem norm_eulerPrimePowerComplex L402
theorem norm_eulerPrimePowerComplex_lt_one L422
theorem norm_eulerPrimePowerComplex_lt_one_on_sensorCircle L438
theorem one_sub_eulerPrimePowerComplex_ne_zero L450
theorem eulerDet2FactorComplex_ne_zero L462
theorem zetaReciprocal_differentiableAt L472
theorem norm_eulerPrimePowerComplex_eq_rpow L481
theorem norm_eulerPrimeLogDerivTermComplex_le L490
theorem norm_form_eq_carrierDerivTerm L510
theorem norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm L522
theorem eulerPrimeLogDerivTermComplex_summable L535
theorem analyticAt_riemannZeta L546
theorem zetaReciprocal_meromorphicAt L555
theorem meromorphicOrderAt_zetaReciprocal L562
theorem zetaReciprocal_order_at_zero L570
structure remembers L579
structure WitnessedDefectSensor L581
theorem zetaReciprocal_local_factorization L612
def eulerQuantitativeFactorization L624
theorem eulerQuantitativeFactorization_logDerivBound L658
theorem eulerQuantitativeFactorization_center L668
theorem eulerQuantitativeFactorization_order L678
def eulerCarrierInstance L691
def eulerRegularCarrier L702
theorem euler_regular_carrier_covers_strip L712
def EulerBudgetUpgradeTarget L722
theorem euler_budget_upgrade_extends_regular L729
def eulerZeroTrace L740
def eulerBudgetedCarrier L750
theorem euler_budget_upgrade_target L767
def eulerCostCoveringPackage L772
theorem argument_principle_sampling L786
def DeprecatedDefectAnnularCostBounded L815
theorem defect_annular_cost_bounded_inconsistent L826
theorem rh_from_complex_analysis_axioms L842
theorem rh_no_zeros_in_strip L852
theorem defect_bounded_impossible L862
def zetaDefectSensor L876
theorem sensor_carrier_compatible L886
structure EulerInstantiationCert L902
def mkEulerInstantiationCert L921
theorem euler_rh_conditional L936
theorem riemann_hypothesis_euler_conditional L943
def eulerSampledBudgetedCarrier L959
theorem eulerSampledBudgetedCarrier_scale_zero L969
def eulerSampledPackage L974

… and 1 more