theorem proved term proof

`c_value_cone`

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

formal statement (Lean)

 359theorem c_value_cone : cmin RS.coneConstants = 1/2 := by

proof body

Term-mode proof.

 360  simp only [cmin, RS.cone_Knet_eq_one, RS.cone_Cproj_eq_two, RS.cone_Ceng_eq_one]
 361  norm_num
 362
 363end Bridge
 364
 365/-! ## Formal Constants Record
 366
 367A structured record of all CPM constants with their derivations,
 368suitable for auditing and JSON export. -/
 369
 370/-- Complete record of CPM constants with provenance. -/

depends on (21)

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
cmin in IndisputableMonolith.CPM.LawOfExistence decl_use
cone_Ceng_eq_one in IndisputableMonolith.CPM.LawOfExistence decl_use
coneConstants in IndisputableMonolith.CPM.LawOfExistence decl_use
cone_Cproj_eq_two in IndisputableMonolith.CPM.LawOfExistence decl_use
cone_Knet_eq_one in IndisputableMonolith.CPM.LawOfExistence decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
all in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
Bridge in IndisputableMonolith.RecogSpec.Core decl_use