cproj_eq_two_from_J_normalization — Recognition explainer

formal statement (Lean)

 280theorem cproj_eq_two_from_J_normalization
 281  (_hJ : deriv (deriv (fun t : ℝ => IndisputableMonolith.Cost.Jcost (Real.exp t))) 0 = 1) :
 282  coneConstants.Cproj = 2 := by

proof body

Term-mode proof.

 283  simp [cone_Cproj_eq_two]
 284
 285end RS
 286
 287/-! ## Bridge Lemmas: CPM Constants from RS Invariants
 288
 289These lemmas explicitly connect CPM constants to Recognition Science
 290invariants, providing the formal bridge between the abstract CPM
 291framework and the RS derivations. -/
 292
 293namespace Bridge
 294
 295/-- C_proj = 2 follows from the J-cost second derivative normalization.
 296
 297The Hermitian rank-one bound ‖Pψ‖² ≤ C_proj · ‖ψ‖² has optimal constant
 298C_proj = 2 when the projection is normalized so that J''(1) = 1 in
 299log-coordinates. This is the content of `RS.Jcost_log_second_deriv_normalized`. -/

depends on (31)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
coneConstants in IndisputableMonolith.CPM.LawOfExistence decl_use
cone_Cproj_eq_two in IndisputableMonolith.CPM.LawOfExistence decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
Jcost_log_second_deriv_normalized in IndisputableMonolith.CPM.LawOfExistence decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
rank in IndisputableMonolith.Foundation.PreTemporalForcingOrder decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
C_proj in IndisputableMonolith.Gravity.CoerciveProjection decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
normalized in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
Bridge in IndisputableMonolith.RecogSpec.Core decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use

… and 1 more