pith. machine review for the scientific record. sign in
theorem proved term proof

rh_from_composition_closure

show as:
view Lean formalization →

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)

  98theorem rh_from_composition_closure (cch : CompositionClosureHypothesis) :
  99    ∀ ρ : ℂ, ¬OnCriticalLine ρ → False := by

proof body

Term-mode proof.

 100  intro ρ hρ
 101  obtain ⟨n, hn⟩ := composition_violates_budget ρ hρ cch.bound
 102  have hle := cch.reflected ρ hρ n
 103  linarith
 104
 105/-! ## §3. The Forcing Chain (summary) -/
 106
 107/-- **Certificate**: the full forcing chain from RCL to RH.
 108
 109    This packages the entire argument:
 110    - T5: RCL uniquely forces J
 111    - Bridge: ξ-symmetry = J-symmetry
 112    - Composition: RCL self-composition amplifies defect
 113    - Divergence: iterated defect is unbounded
 114    - Budget: carrier budget is finite
 115    - Conclusion: off-critical zeros are impossible -/

used by (1)

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

depends on (18)

Lean names referenced from this declaration's body.