theorem proved term proof

`J_symmetric`

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

formal statement (Lean)

  27theorem J_symmetric {x : ℝ} (_hx : x ≠ 0) : J x = J (x⁻¹) := by

Term-mode proof.

  28  simp only [J, inv_inv]; ring
  29
  30/-- J-symmetry in ratio form: J(a/b) = J(b/a). -/

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

J_symmetric in IndisputableMonolith.Foundation.CostAxioms decl_use
J_symmetric_ratio in IndisputableMonolith.Foundation.LedgerForcing decl_use
ledger_forcing_principle in IndisputableMonolith.Foundation.LedgerForcing decl_use
reciprocity in IndisputableMonolith.Foundation.LedgerForcing decl_use
cost_to_recognition_bridge in IndisputableMonolith.Foundation.RecognitionForcing decl_use
J_symmetric in IndisputableMonolith.QFT.HiggsMechanism decl_use

Lean names referenced from this declaration's body.