defectSensorCenter
The function extracting the geometric center for a defect sensor returns the complex number obtained by coercing the sensor's stored real part. Analysts instantiating the Euler product as a concrete carrier in the recognition science cost framework cite this when initializing circle-based sampling of zeta reciprocals or Euler factors. The definition is realized by a direct type coercion from the real component.
claimLet $s$ be a defect sensor that stores only a real part. The associated center is the complex number whose real part equals the value stored in $s$ and whose imaginary part is zero.
background
The EulerInstantiation module realizes the abstract RS carrier and sensor framework from AnnularCost and CostCoveringBridge by means of the Euler product for the zeta function. It proceeds from prime sums and Hilbert-Schmidt norms through convergence of the logarithmic derivative to satisfaction of the EulerCarrier and RegularCarrier interfaces, thereby enabling the cost-covering axiom and a conditional Riemann hypothesis. A defect sensor is the geometric object that tracks a sampling location; in this instantiation the sensor is restricted to the real axis and records only its realPart field. Upstream structures include the eight-tick phases (periodic with period $2^3$) and the J-cost calibration from PhiForcingDerived.
proof idea
One-line wrapper that coerces the realPart field of the input sensor to the complex numbers.
why it matters in Recognition Science
This definition supplies the center required by the downstream circle-sampling functions that replace abstract phase families with concrete samples of zeta reciprocals on circles. It therefore occupies the geometric entry point in the module's instantiation chain from primes to carrier satisfaction. The construction aligns with the framework's use of eight-tick phases and real-axis proxies for defect tracking.
scope and limits
- Does not compute or store an imaginary part for the center.
- Does not depend on specific numerical values of the Euler-Mascheroni constant.
- Applies only inside the defect-sensor layer of the Euler-product instantiation.
- Does not itself perform any sampling or phase-family replacement.
Lean usage
noncomputable def sample (s : DefectSensor) (r θ : ℝ) : ℂ := circleMap (defectSensorCenter s) r θformal statement (Lean)
370noncomputable def defectSensorCenter (sensor : DefectSensor) : ℂ :=
proof body
Definition body.
371 (sensor.realPart : ℂ)
372
373/-- Sample a point on a circle around the current sensor center. This is the
374geometric entry point for replacing abstract phase families by actual samples of
375`ζ⁻¹` or Euler factors on circles. -/