eulerScalarProxy
plain-language theorem explainer
eulerScalarProxy supplies a positive real scalar state for any defect sensor at refinement depth N, obtained by attenuating the normalized Euler gap by the factor 1/(N+1) and taking the reciprocal. Researchers constructing T1-bounded ledger instances for the Euler carrier in the Unified RH architecture cite this definition when instantiating PhysicallyRealizableLedger. The definition is a direct algebraic expression that assembles the carrier value, derivative bound, and admissible radius into a single state variable.
Claim. For a defect sensor $s$ recording charge multiplicity and real part $σ_0$, the Euler scalar proxy at depth $N$ is the positive real $x_N = 1 / (1 + g(s)/(N+1))$, where the normalized stiffness $g(s)$ equals the product of the carrier logarithmic-derivative bound and the admissible strip radius divided by the carrier value at $σ_0$.
background
The Unified RH module replaces earlier total-cost assertions with a three-component architecture: cost divergence forced by nonzero charge, Euler trace admissibility proved from carrier data, and a physically realizable ledger whose scalar state carries a uniform T1 defect bound. A DefectSensor is the structure holding the integer charge (zero multiplicity) and real part of a hypothetical zero location inside the critical strip. The upstream eulerScalarGap definition packages three Euler ingredients into one dimensionless quantity: gap(sensor) = carrierDerivBound(sensor.realPart) * eulerCarrierRadius(sensor) / carrierValue(sensor.realPart).
proof idea
This is a direct definition. It evaluates the expression 1 / (1 + eulerScalarGap sensor / (N + 1 : ℝ)) using the already-proved positivity of eulerScalarGap.
why it matters
The definition supplies the scalarState field for the eulerPhysicallyRealizableLedger instance, which asserts that the Euler carrier satisfies the PhysicallyRealizableLedger interface. It is invoked by eulerScalarProxy_pos, eulerScalarProxy_defect_bounded, and physicallyRealizableLedger_not_boundaryApproaching, thereby closing the Euler path in the T1-bounded realizability chain. Within the Recognition framework this step links the Euler instantiation data to the prohibition on boundary approach enforced by the law of existence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.