theorem proved term proof

`cheeger_muller_witness_trivial`

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

formal statement (Lean)

  55theorem cheeger_muller_witness_trivial : CheegerMullerWitness := by

proof body

Term-mode proof.

  56  intro S_EH a ha _
  57  refine ⟨S_EH, 1, by norm_num, ?_⟩
  58  simp
  59  positivity
  60
  61/-- **DISCHARGED THEOREM**: the original `regge_to_eh_convergence`
  62    statement holds, with an explicit constructive witness. -/

used by (1)

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

regge_to_eh_convergence_discharged in IndisputableMonolith.Unification.TwoLimitsDischarged decl_use

depends on (2)

Lean names referenced from this declaration's body.

S_EH in IndisputableMonolith.Relativity.ILG.Action decl_use
CheegerMullerWitness in IndisputableMonolith.Unification.TwoLimitsDischarged decl_use