theorem proved term proof

`zetaDefectSensor_charge_ne_zero`

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

formal statement (Lean)

  58theorem zetaDefectSensor_charge_ne_zero (σ : ℝ)
  59    (hstrip : 1/2 < σ ∧ σ < 1) :
  60    (zetaDefectSensor σ hstrip 1).charge ≠ 0 := by

proof body

Term-mode proof.

  61  simp [zetaDefectSensor]
  62
  63/-- **Core unconditional result.** Any `DefectSensor` with nonzero
  64charge fails the `PhysicallyExists` predicate.  Direct corollary of
  65`ontological_dichotomy`. No custom axioms. -/

used by (5)

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

zeta_zero_gives_charged_sensor in IndisputableMonolith.NumberTheory.ArgumentPrincipleSensor decl_use
zeroInducedBridge_iff_no_strip_zeros in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
no_strip_zeros_of_decomposed_data in IndisputableMonolith.NumberTheory.RSPhysicalThesisDecomposition decl_use
strip_zero_gives_nonphysical_sensor in IndisputableMonolith.NumberTheory.ZetaLedgerBridge decl_use
unit_sensor_not_physical in IndisputableMonolith.NumberTheory.ZetaLedgerBridge decl_use

depends on (9)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
DefectSensor in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
zetaDefectSensor in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
ontological_dichotomy in IndisputableMonolith.Unification.UnifiedRH decl_use
PhysicallyExists in IndisputableMonolith.Unification.UnifiedRH decl_use