pith. machine review for the scientific record. sign in
structure definition def or abbrev

RSPhysicalThesisDataLogic

show as:
view Lean formalization →

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)

  27structure RSPhysicalThesisDataLogic where
  28  primeLedgerLogic : PrimeLedgerLogicCert
  29  primeLedgerClassical : PrimeLedgerCert
  30  eulerPartition : EulerLedgerPartitionCert
  31  completedLedger : CompletedZetaLedgerCert
  32  zeroDefect : ArgumentPrincipleSensorCert
  33  realizableLedger : EulerRealizableLedgerCert
  34  boundaryTransport : BoundaryTransportCert
  35  t1Boundary : T1BoundaryExclusionCert
  36
  37/-- Forget the recovered-prime wrapper to the current decomposed data bundle. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.