def definition def or abbrev

`J`

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

formal statement (Lean)

 156noncomputable def J (x : ℝ) : ℝ := Cost.Jcost x

proof body

Definition body.

 157
 158/-- Exact decomposition of the J-cost composition identity.
 159
 160This is the concrete RCL form specialized to `J`:
 161`J(ab) + J(a/b) = 2JaJb + 2Ja + 2Jb`. -/

depends on (14)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma 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
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use