theorem proved term proof

`jcost_xiMap_nonneg`

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

formal statement (Lean)

  92theorem jcost_xiMap_nonneg (σ : ℝ) : 0 ≤ Jcost (xiMap σ) :=

proof body

Term-mode proof.

  93  Jcost_nonneg (xiMap_pos σ)
  94
  95/-- J-cost on defect coordinates is symmetric under functional reflection.
  96    This IS the bridge:  ξ(s)=ξ(1−s)  ↔  J(x)=J(1/x). -/

depends on (15)

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
Jcost_nonneg in IndisputableMonolith.Cost decl_use
Jcost_nonneg in IndisputableMonolith.Cost.JcostCore decl_use
defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
Jcost_nonneg in IndisputableMonolith.Gravity.CoherenceCollapse decl_use
Jcost_nonneg in IndisputableMonolith.Gravity.EnergyProcessingBridge decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Jcost_nonneg in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
xiMap in IndisputableMonolith.NumberTheory.XiJBridge decl_use
xiMap_pos in IndisputableMonolith.NumberTheory.XiJBridge decl_use