theorem proved term proof

`C_proj_value`

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

formal statement (Lean)

  60theorem C_proj_value : C_proj = 2 := rfl

proof body

Term-mode proof.

  61
  62/-- The defect bound: Defect(Phi) <= M * K_net * C_proj * sup T_W[Phi].
  63    The constant M * K_net * C_proj controls the stability of the energy minimizer. -/

depends on (14)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Phi in IndisputableMonolith.Cost.AczelProof decl_use
Phi in IndisputableMonolith.Cost.AczelTheorem decl_use
Defect in IndisputableMonolith.CPM.LNALBridge decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
C_proj in IndisputableMonolith.Gravity.CoerciveProjection decl_use
K_net in IndisputableMonolith.Gravity.CoerciveProjection decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use