theorem proved term proof

`integrationGap_factors`

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

formal statement (Lean)

  59theorem integrationGap_factors : integrationGap D = 9 * 5 := by native_decide

proof body

Term-mode proof.

  60
  61/-! ## Coprimality forces odd dimension -/
  62
  63/-- For odd `D = 2k+1`, `D²(D+2)` is odd (a product of odd numbers),
  64    hence coprime with any power of `2`. -/

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
power in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
integrationGap in IndisputableMonolith.Foundation.IntegrationGap decl_use
forces in IndisputableMonolith.Foundation.MagnitudeOfMismatch decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use