theorem proved term proof

`sync_strictly_increasing_odd`

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

formal statement (Lean)

 146theorem sync_strictly_increasing_odd :
 147    syncPeriod 3 < syncPeriod 5 ∧
 148    syncPeriod 5 < syncPeriod 7 ∧
 149    syncPeriod 7 < syncPeriod 9 ∧
 150    syncPeriod 9 < syncPeriod 11 := by

proof body

Term-mode proof.

 151  exact ⟨by native_decide, by native_decide, by native_decide, by native_decide⟩
 152
 153/-! ## Complete Certificate -/
 154
 155/-- The full constraint (S) certificate packaging the dimensional selection of 45. -/

used by (1)

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

constraintS in IndisputableMonolith.Gap45.SyncMinimization decl_use

depends on (9)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
syncPeriod 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
syncPeriod in IndisputableMonolith.Gap45.SyncMinimization decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
syncPeriod in IndisputableMonolith.Papers.DraftV1 decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use