theorem proved term proof

`knet_from_cone_projection`

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

formal statement (Lean)

 312theorem knet_from_cone_projection :
 313    RS.coneConstants.Knet = 1 := rfl

proof body

Term-mode proof.

 314
 315/-- K_net for ε-net covering in dimension d.
 316
 317Given covering radius ε and dimension d, the net constant is
 318K_net = (1/(1-2ε))^d. For ε = 1/8 and d = 3:
 319K_net = (1/(1-1/4))^3 = (4/3)^3 = 64/27. -/

depends on (12)

Lean names referenced from this declaration's body.

radius in IndisputableMonolith.Complexity.CellularAutomata decl_use
coneConstants in IndisputableMonolith.CPM.LawOfExistence decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
K_net in IndisputableMonolith.Gravity.CoerciveProjection decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use
net in IndisputableMonolith.RRF.Core.Strain decl_use
net in IndisputableMonolith.RRF.Foundation.Ledger decl_use