structure definition def or abbrev

`HonestPhaseChargeZeroBridge`

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

formal statement (Lean)

 205structure HonestPhaseChargeZeroBridge where
 206  charge_zero_of_honest_phase :
 207    ∀ zfd : ZetaPhaseFamilyData, zfd.sensor.charge = 0
 208
 209/-- A direct honest-phase charge-zero bridge discharges the `ZeroFreeCriterion`
 210charge-zero field. -/

used by (6)

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

charge_zero_of_honest_phase_of_chargeZeroBridge in IndisputableMonolith.NumberTheory.AnalyticTrace decl_use
direct_rh_from_honestPhaseChargeZeroBridge in IndisputableMonolith.NumberTheory.AnalyticTrace decl_use
zeroFreeCriterion_of_honestPhaseChargeZeroBridge in IndisputableMonolith.NumberTheory.AnalyticTrace decl_use
admissibilityBridge_of_chargeZeroBridge in IndisputableMonolith.NumberTheory.HonestPhaseAdmissibility decl_use
chargeZeroBridge_of_admissibilityBridge in IndisputableMonolith.NumberTheory.HonestPhaseAdmissibility decl_use
honestPhaseAdmissibilityBridge_iff_chargeZeroBridge in IndisputableMonolith.NumberTheory.HonestPhaseAdmissibility decl_use

depends on (8)

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
phase in IndisputableMonolith.Foundation.EightTick decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
ZeroFreeCriterion in IndisputableMonolith.NumberTheory.AnalyticTrace decl_use
ZetaPhaseFamilyData in IndisputableMonolith.NumberTheory.MeromorphicCircleOrder decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use