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)
30theorem honestPhaseAdmissible_iff_charge_zero (zfd : ZetaPhaseFamilyData) :
31 HonestPhaseAdmissible zfd ↔ zfd.sensor.charge = 0 := by
proof body
Term-mode proof.
32 constructor
33 · intro hadm
34 exact charge_zero_of_honestPhaseAdmissible zfd hadm
35 · intro hzero
36 exact ⟨(honestPhaseFamily_cost_bounded_iff_charge_zero zfd).mpr hzero⟩
37
38/-- A global admissibility bridge for all honest zeta phase data. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (16)
Lean names referenced from this declaration's body.
-
all
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
-
all
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
bridge
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
all
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
phase
in IndisputableMonolith.Foundation.EightTick
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
all
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use
-
charge_zero_of_honestPhaseAdmissible
in IndisputableMonolith.NumberTheory.HonestPhaseAdmissibility
decl_use
-
HonestPhaseAdmissible
in IndisputableMonolith.NumberTheory.HonestPhaseAdmissibility
decl_use
-
honestPhaseFamily_cost_bounded_iff_charge_zero
in IndisputableMonolith.NumberTheory.HonestPhaseBudgetBridge
decl_use
-
ZetaPhaseFamilyData
in IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
decl_use
-
zeta
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
phase
in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge
decl_use