No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
477noncomputable instance eulerPhysicallyRealizableLedger (sensor : DefectSensor) :
478 PhysicallyRealizableLedger sensor where
479 admissible := euler_trace_admissible sensor
proof body
Definition body.
480 scalarState := eulerScalarProxy sensor
481 scalarStatePos := eulerScalarProxy_pos sensor
482 scalarDefectBounded := eulerScalarProxy_defect_bounded sensor
483
484/-- Explicit theorem form of the Euler realizability instance. -/
depends on (12)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
admissible
in IndisputableMonolith.Information.Thermodynamics
decl_use
-
DefectSensor
in IndisputableMonolith.NumberTheory.CostCoveringBridge
decl_use
-
eulerScalarProxy
in IndisputableMonolith.Unification.UnifiedRH
decl_use
-
eulerScalarProxy_defect_bounded
in IndisputableMonolith.Unification.UnifiedRH
decl_use
-
eulerScalarProxy_pos
in IndisputableMonolith.Unification.UnifiedRH
decl_use
-
euler_trace_admissible
in IndisputableMonolith.Unification.UnifiedRH
decl_use
-
PhysicallyRealizableLedger
in IndisputableMonolith.Unification.UnifiedRH
decl_use