euler_physically_realizable
plain-language theorem explainer
The declaration supplies the PhysicallyRealizableLedger instance for any DefectSensor under the Euler carrier. Boundary-transport and ontology-interface results cite it to obtain the admissible scalar proxy with uniform T1-defect bound. The proof is a one-line wrapper that invokes typeclass inference on the EulerTraceAdmissible data.
Claim. For every defect sensor $s$, the Euler carrier yields a physically realizable ledger whose scalar proxy state $x_N$ satisfies $x_N > 0$ for all $N$ and admits a uniform bound $K$ such that the T1 defect of $x_N$ is at most $K$.
background
In the Unified RH module the architecture splits into cost divergence, Euler trace admissibility, and physical realizability. PhysicallyRealizableLedger sensor is the class requiring an admissible Euler trace, a positive scalar-state map, and a uniform bound on the T1 defect of that state. The module replaces earlier total-cost assertions with this three-component structure so that the Euler proxy remains bounded away from the T1 boundary on its own.
proof idea
The definition is a one-line wrapper that applies infer_instance to discharge the PhysicallyRealizableLedger class using the EulerTraceAdmissible instance and the scalar proxy construction already available for the Euler carrier.
why it matters
It supplies the proved realizability half of the ontology interface, feeding concreteEulerLedgerOntologyInterface, euler_ledger_realizable, and the boundary-transport certificates. The declaration closes the Euler-carrier segment of the T1 architecture, leaving only the external EulerBoundaryBridgeAssumption for divergence-to-boundary transport. It supports the claim that realizable Euler ledgers cannot approach the T1 boundary without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.