theorem proved term proof

`direct_rh_from_EBBA_via_analytic`

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

formal statement (Lean)

 438theorem direct_rh_from_EBBA_via_analytic
 439    (bridge : Unification.UnifiedRH.EulerBoundaryBridgeAssumption) :
 440    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=

proof body

Term-mode proof.

 441  rh_from_zero_free_criterion (zeroFreeCriterion_of_EBBA bridge)
 442
 443end AnalyticTrace
 444end NumberTheory
 445end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
rh_from_zero_free_criterion in IndisputableMonolith.NumberTheory.AnalyticTrace decl_use
zeroFreeCriterion_of_EBBA in IndisputableMonolith.NumberTheory.AnalyticTrace decl_use
WitnessedDefectSensor in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
EulerBoundaryBridgeAssumption in IndisputableMonolith.Unification.UnifiedRH decl_use