theorem proved term proof

`gapMinusOne_factor`

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

formal statement (Lean)

  98theorem gapMinusOne_factor : gapMinusOne D = 4 * 11 := by native_decide

proof body

Term-mode proof.

  99
 100/-! ## φ-power identity (matter-balance bridge) -/
 101
 102noncomputable section
 103
 104/-- The active edge count per fundamental tick. -/

depends on (7)

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
power in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
gapMinusOne in IndisputableMonolith.Foundation.IntegrationGap decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use