lemma proved term proof

`J_at_one`

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

formal statement (Lean)

  92lemma J_at_one : J 1 = 0 := by unfold J; norm_num

proof body

Term-mode proof.

  93
  94/-- J(x) = 0 iff x = 1 (for positive x). -/

used by (21)

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

canonicalCostAlgebra in IndisputableMonolith.Algebra.CostAlgebra decl_use
canonicalRecognitionCostSystem_cost_one in IndisputableMonolith.Algebra.CostAlgebra decl_use
cost_algebra_certificate in IndisputableMonolith.Algebra.CostAlgebra decl_use
defectDist_no_global_quasi_triangle in IndisputableMonolith.Algebra.CostAlgebra decl_use
defectDist_self in IndisputableMonolith.Algebra.CostAlgebra decl_use
H_at_one in IndisputableMonolith.Algebra.CostAlgebra decl_use
J_at_one in IndisputableMonolith.Algebra.CostAlgebra decl_use
J_at_one in IndisputableMonolith.Masses.BaselineDerivation decl_use
nontriviality_from_cost in IndisputableMonolith.Masses.BaselineDerivation decl_use
collapse_automatic in IndisputableMonolith.Modal.Actualization decl_use
every_config_actualizes in IndisputableMonolith.Modal.Actualization decl_use
H_adjoint_non_minimal in IndisputableMonolith.Modal.Actualization decl_use
possibility_actualization_adjoint_minimal in IndisputableMonolith.Modal.Actualization decl_use
possibility_actualization_adjoint_monotonic in IndisputableMonolith.Modal.Actualization decl_use
actualize_decreases_cost in IndisputableMonolith.Modal.Possibility decl_use
identity_always_possible in IndisputableMonolith.Modal.Possibility decl_use
identity_prefers_stasis in IndisputableMonolith.Modal.Possibility decl_use
identity_unique_attractor in IndisputableMonolith.Modal.Possibility decl_use
J_stasis_at_one in IndisputableMonolith.Modal.Possibility decl_use
J_zero_iff_one in IndisputableMonolith.Modal.Possibility decl_use
J_at_one in IndisputableMonolith.QFT.HiggsMechanism decl_use

depends on (4)

Lean names referenced from this declaration's body.

J_at_one in IndisputableMonolith.Algebra.CostAlgebra decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
J_at_one in IndisputableMonolith.Masses.BaselineDerivation decl_use
J_at_one in IndisputableMonolith.QFT.HiggsMechanism decl_use