No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
100structure LockPhasePrediction (Event : Type*) where
101 /-- Metric for structural change. -/
102 structuralChange : Event → ℝ
103 /-- LOCK phases have higher structural change. -/
104 lock_higher : ∀ (trace : TickedTrace Event) (i j : Fin trace.events.length),
105 (trace.phase i).isLock → (trace.phase j).isBalance →
106 structuralChange (trace.events[i]) ≥ structuralChange (trace.events[j])
107
108/-! ## Falsification Interface -/
109
110/-- A falsification witness: a trace where 8-tick doesn't work. -/
depends on (13)
Lean names referenced from this declaration's body.
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
phase
in IndisputableMonolith.Foundation.EightTick
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
phase
in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge
decl_use
-
falsification
in IndisputableMonolith.Physics.EarthBrainResonance
decl_use
-
Metric
in IndisputableMonolith.Relativity.ILG.Action
decl_use
-
isBalance
in IndisputableMonolith.RRF.Hypotheses.EightTick
decl_use
-
isLock
in IndisputableMonolith.RRF.Hypotheses.EightTick
decl_use
-
TickedTrace
in IndisputableMonolith.RRF.Hypotheses.EightTick
decl_use