lemma proved term proof

`modal_distance_symm`

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

formal statement (Lean)

  68lemma modal_distance_symm (c1 c2 : Config) :
  69    modal_distance c1 c2 = modal_distance c2 c1 := by

proof body

Term-mode proof.

  70  unfold modal_distance
  71  exact J_transition_symm c1.pos c2.pos
  72
  73/-! ## Possibility Space Topology -/
  74
  75/-- **POSSIBILITY BALL**: The set of configs within modal distance r of c.
  76
  77    B_r(c) = {y : modal_distance(c, y) ≤ r} -/

depends on (11)

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
Config in IndisputableMonolith.Gravity.ILG decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
modal_distance in IndisputableMonolith.Modal.ModalGeometry decl_use
Config in IndisputableMonolith.Modal.Possibility decl_use
J_transition_symm in IndisputableMonolith.Modal.Possibility decl_use
Possibility in IndisputableMonolith.Modal.Possibility decl_use
c1 in IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension decl_use