theorem proved term proof

`coshRemainder_zero`

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

formal statement (Lean)

 168theorem coshRemainder_zero : coshRemainder 0 = 0 := by

proof body

Term-mode proof.

 169  unfold coshRemainder
 170  simp
 171
 172/-! ## §4. Decomposition: exact = linearized + quartic remainder -/
 173
 174/-- The quartic remainder of the full action (the "non-linear
 175    correction" to the weak-field Laplacian). It vanishes on the
 176    flat vacuum and is `O(|ε|⁴)` for small `ε`. -/

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
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
coshRemainder in IndisputableMonolith.Foundation.SimplicialLedger.NonlinearBridge decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
vacuum in IndisputableMonolith.Unification.YangMillsMassGap decl_use