theorem proved term proof

`gap_range`

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

formal statement (Lean)

  76theorem gap_range : 43 ≤ timescale_gap_log10 ∧ timescale_gap_log10 < 45 := by

proof body

Term-mode proof.

  77  unfold timescale_gap_log10
  78  constructor <;> norm_num
  79
  80/-! ## Decoherence Time Formula -/
  81
  82/-- The number of environmental modes coupled to the system. -/

depends on (8)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
modes in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
Time in IndisputableMonolith.Constants.RSNativeUnits decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
timescale_gap_log10 in IndisputableMonolith.QFT.Decoherence decl_use