def
definition
zeroFreeCriterion_of_EBBA
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.AnalyticTrace on GitHub at line 432.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
bridge -
from -
honestPhaseCostBridge_of_EBBA -
ZeroFreeCriterion -
zeroFreeCriterion_of_honestPhaseCostBridge -
EulerBoundaryBridgeAssumption
used by
formal source
429 exact Unification.UnifiedRH.unified_rh bridge sensor.toDefectSensor (by simpa using hm))
430
431/-- The ontology bridge also supplies a complete `ZeroFreeCriterion`. -/
432noncomputable def zeroFreeCriterion_of_EBBA
433 (bridge : Unification.UnifiedRH.EulerBoundaryBridgeAssumption) :
434 ZeroFreeCriterion :=
435 zeroFreeCriterion_of_honestPhaseCostBridge (honestPhaseCostBridge_of_EBBA bridge)
436
437/-- Direct witnessed-sensor RH from the ontology bridge through the analytic route. -/
438theorem direct_rh_from_EBBA_via_analytic
439 (bridge : Unification.UnifiedRH.EulerBoundaryBridgeAssumption) :
440 ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
441 rh_from_zero_free_criterion (zeroFreeCriterion_of_EBBA bridge)
442
443end AnalyticTrace
444end NumberTheory
445end IndisputableMonolith