theorem proved term proof

`xiMap_eq_exp_zeroDeviation`

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

formal statement (Lean)

  75theorem xiMap_eq_exp_zeroDeviation (ρ : ℂ) :
  76    xiMap ρ.re = Real.exp (zeroDeviation ρ) := by

proof body

Term-mode proof.

  77  simp [xiMap, zeroDeviation]
  78
  79/-! ## §3. J-cost in strip coordinates -/
  80
  81/-- J-cost on defect coordinates gives the cosh form of the zero defect:
  82    J(e^{2η}) = cosh(2η) − 1  where η = σ − 1/2. -/

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
xiMap in IndisputableMonolith.NumberTheory.XiJBridge decl_use
zeroDeviation in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use