IndisputableMonolith.NumberTheory.EulerCarrierRealizability

   1import IndisputableMonolith.Unification.UnifiedRH
   2
   3/-!
   4# Euler Carrier Realizability
   5
   6The Euler carrier is already realized in `UnifiedRH.lean` as a
   7T1-bounded ledger.  This module extracts that result into the file layout used
   8by the RH-from-RCL derivation plan.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace NumberTheory
  13
  14open IndisputableMonolith.Unification.UnifiedRH
  15
  16/-- Euler trace admissibility is available for every defect sensor. -/
  17theorem euler_trace_admissible_concrete (sensor : DefectSensor) :
  18    EulerTraceAdmissible sensor :=
  19  euler_trace_admissible sensor
  20
  21/-- The Euler ledger is physically realizable in the T1-bounded sense. -/
  22noncomputable def euler_ledger_realizable (sensor : DefectSensor) :
  23    PhysicallyRealizableLedger sensor :=
  24  euler_physically_realizable sensor
  25
  26/-- Certificate for Euler carrier realizability. -/
  27structure EulerRealizableLedgerCert where
  28  admissible : ∀ sensor : DefectSensor, EulerTraceAdmissible sensor
  29  realizable : ∀ sensor : DefectSensor, PhysicallyRealizableLedger sensor
  30
  31/-- The proved Euler realizability certificate. -/
  32noncomputable def eulerRealizableLedgerCert : EulerRealizableLedgerCert where
  33  admissible := euler_trace_admissible_concrete
  34  realizable := euler_ledger_realizable
  35
  36end NumberTheory
  37end IndisputableMonolith
  38