theorem proved term proof

`midpointMap_fixed_point`

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

formal statement (Lean)

  43theorem midpointMap_fixed_point : midpointMap 1 = 1 := by

Term-mode proof.

  44  unfold midpointMap; norm_num
  45
  46/-- J decreases under the midpoint map for any x > 0, x ≠ 1. -/

From the project-wide theorem graph. These declarations reference this one in their body.

rHatEmergenceCert in IndisputableMonolith.Foundation.RHatFromJCostGradient decl_use

Lean names referenced from this declaration's body.

midpointMap in IndisputableMonolith.Foundation.RHatFromJCostGradient decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use