module module high

`IndisputableMonolith.NumberTheory.EulerInstantiation`

The EulerInstantiation module defines the set of primes as a subset of natural numbers together with prime sums, Hilbert-Schmidt norms, and related carrier objects for the Euler product. Researchers working on the analytic trace and zeta-ledger bridges cite it as the arithmetic base layer for the Recognition Science treatment of the Riemann hypothesis. The module assembles these objects from imported constants, annular costs, and sampled traces with no internal proofs.

claimLet $P = {p in mathbb{N} | p text{ is prime}}$. The module supplies $text{PrimeSum}(sigma) = sum_{p in P} p^{-sigma}$, the squared Hilbert-Schmidt norm of the associated operator, and the Euler carrier $C(s) = det_2(I - A(s))^2 = prod_p (1 - p^{-s})^2 exp(2 p^{-s})$ on the half-plane Re$(s) > 1/2$.

background

Recognition Science places this module inside the number-theory layer that supports the cost-covering bridge for the Riemann hypothesis. It imports the fundamental time quantum $tau_0 = 1$ tick from Constants and the phi-weighted cost $phiCost(u) := cosh((log phi) u) - 1 = J(phi^u)$ from AnnularCost. DefectSampledTrace supplies the annular meshes attached to hypothetical zeta defects, while EulerCarrierComplex upgrades the real-axis carrier to a holomorphic non-vanishing function on Re$(s) > 1/2$. CostCoveringBridge and SampledTrace provide the surrounding architecture that eliminates prior axioms.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds AnalyticTrace, ArgumentPrincipleProved, CarrierBudgetComparison, ConcreteEulerLedger, ZetaLedgerBridge, and UnifiedRH. It supplies the concrete prime-based ledger and Euler carrier required for the three-component architecture that replaces the former OntologicalPrimeLedger with bounded annular cost. It fills the arithmetic-to-ledger identification step in the RH closure plan and enables the carrier-defect budget comparison on the same circles.

scope and limits

Does not prove convergence of the Euler product for Re(s) <= 1.
Does not locate any zeta zeros or establish zero-free regions.
Does not perform numerical evaluation of sums or determinants.
Does not contain analytic continuation arguments.
Does not discharge any hypothesis_interface or scaffolding stubs.

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