eulerLedgerScalarState
plain-language theorem explainer
The definition supplies the Euler ledger scalar state for a defect sensor at step N. It returns the constant 1 when charge is zero and the realized collapse scalar 1 over 1 plus annular cost otherwise. Researchers working on unified RH cite this scalar when establishing the ontological dichotomy between zero-charge realizability and nonzero-charge divergence. The definition proceeds by a direct case split on sensor charge.
Claim. For a defect sensor $s$ with integer charge $c$ and real part $r$, the Euler ledger scalar state at step $N$ is defined by $e(s,N) := 1$ if $c=0$, and $e(s,N) := 1/(1 + A_N)$ otherwise, where $A_N$ denotes the annular cost of the canonical defect sampled family mesh at level $N$.
background
In the Unified RH module the Euler ledger scalar state acts as the scalar proxy inside the physically realizable ledger component of the T1-bounded architecture. A DefectSensor is the structure carrying an integer charge (multiplicity of a zeta zero) and its real part; the module replaces earlier bounded-total-cost attempts with three components: cost divergence for nonzero charge, Euler trace admissibility, and the realizable ledger whose T1 defect stays bounded. The upstream realizedDefectCollapseScalar supplies the nonzero-charge case via the explicit formula 1/(1 + annularCost((canonicalDefectSampledFamily sensor hm).mesh N)). The local setting is the T1-bounded realizability architecture whose proof chain runs from euler_trace_admissible through PhysicallyRealizableLedger to the ontological dichotomy.
proof idea
The definition is a direct conditional expression: test whether sensor.charge equals zero and return 1, otherwise invoke the upstream realizedDefectCollapseScalar on the sensor, the nonzero-charge witness, and N. No tactics or reductions are required; it is a simple case split that inherits positivity and other properties from the collapse scalar.
why it matters
This scalar is the central object in the unified RH chain. It is invoked directly by the ontological_dichotomy theorem, which equates charge zero with T1-bounded defect and thereby supplies the RS ontological argument for RH. It also feeds charge_zero_cost_scalar_t1_bounded, euler_collapse_boundary_transport, and the positivity and equality lemmas. In the framework it realizes the physically realizable ledger component, closing the link between Euler instantiation data and the T1 boundary condition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.