theorem proved term proof

`simplicial_loop_tick_lower_bound`

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

formal statement (Lean)

 128theorem simplicial_loop_tick_lower_bound
 129    (L : SimplicialLedger.SimplicialLedger)
 130    (cycle : List SimplicialLedger.Simplex3)
 131    (hloop : SimplicialLedger.is_recognition_loop cycle) :
 132    eight_tick ≤ cycle.length := by

proof body

Term-mode proof.

 133  simpa [eight_tick] using SimplicialLedger.eight_tick_uniqueness L cycle hloop
 134
 135/-- 8 = 2^3, so eight-tick forces D = 3. -/

depends on (13)

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
eight_tick in IndisputableMonolith.Foundation.DimensionForcing decl_use
forces in IndisputableMonolith.Foundation.MagnitudeOfMismatch decl_use
eight_tick_uniqueness in IndisputableMonolith.Foundation.SimplicialLedger decl_use
is_recognition_loop in IndisputableMonolith.Foundation.SimplicialLedger decl_use
Simplex3 in IndisputableMonolith.Foundation.SimplicialLedger decl_use
SimplicialLedger in IndisputableMonolith.Foundation.SimplicialLedger decl_use
eight_tick in IndisputableMonolith.Gap45.PhysicalMotivation decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
eight_tick in IndisputableMonolith.RRF.Foundation.Constants decl_use
eight_tick in IndisputableMonolith.Thermodynamics.RecognitionThermodynamics decl_use