theorem proved term proof

`j_dalembert`

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

formal statement (Lean)

 125theorem j_dalembert {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 126    Cost.Jcost (x * y) + Cost.Jcost (x / y) =
 127    2 * Cost.Jcost x + 2 * Cost.Jcost y + 2 * Cost.Jcost x * Cost.Jcost y :=

proof body

Term-mode proof.

 128  Cost.dalembert_identity hx hy
 129
 130/-- J-cost submultiplicativity: the cost of a composite transaction
 131    is bounded by the costs of its factors. -/

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
dalembert_identity in IndisputableMonolith.Cost decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization 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
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