def definition def or abbrev

`canonical_phi_lattice`

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

formal statement (Lean)

  52noncomputable def canonical_phi_lattice : PhiLatticeRegularity where
  53  edge_length := phi ^ 2 * 1.47

proof body

Definition body.

  54  edge_positive := by positivity
  55  edge_uniform := fun _ _ => trivial
  56  edge_from_phi := rfl
  57
  58/-! ## Convergence Regime Classification -/
  59

used by (2)

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

nonlinear_regge_cert_exists in IndisputableMonolith.Gravity.NonlinearReggeProof decl_use
phi_lattice_satisfies_cms in IndisputableMonolith.Gravity.NonlinearReggeProof decl_use

depends on (1)

Lean names referenced from this declaration's body.

PhiLatticeRegularity in IndisputableMonolith.Gravity.NonlinearReggeProof decl_use