def definition def or abbrev

`argumentPrincipleSensorCert`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  41def argumentPrincipleSensorCert : ArgumentPrincipleSensorCert where
  42  witnessed_phase_family := fun sensor hm =>

proof body

Definition body.

  43    honest_argument_principle_phase_family sensor hm
  44  zero_gives_charged_sensor := zeta_zero_gives_charged_sensor
  45
  46end NumberTheory
  47end IndisputableMonolith

used by (2)

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

logicData_of_boundaryTransport in IndisputableMonolith.NumberTheory.LogicRH_From_RCL decl_use
rsPhysicalThesisData_of_boundaryTransport in IndisputableMonolith.NumberTheory.RSPhysicalThesisDecomposition decl_use

depends on (3)

Lean names referenced from this declaration's body.

honest_argument_principle_phase_family in IndisputableMonolith.NumberTheory.ArgumentPrincipleProved decl_use
ArgumentPrincipleSensorCert in IndisputableMonolith.NumberTheory.ArgumentPrincipleSensor decl_use
zeta_zero_gives_charged_sensor in IndisputableMonolith.NumberTheory.ArgumentPrincipleSensor decl_use