pith. machine review for the scientific record. sign in
theorem proved term proof

eight_tick_implies_RG4

show as:
view Lean formalization →

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)

 149theorem eight_tick_implies_RG4 {L E : Type*} [RSConfigSpace L]
 150    (rs : RSLocalityFromRHat L) (m : RSMeasurement L E)
 151    (h8 : EightTickFiniteResolution L E rs m) :
 152    HasFiniteResolution (toLocalConfigSpace rs) (toRecognizer m) := by

proof body

Term-mode proof.

 153  intro ℓ
 154  use rs.RHat ℓ
 155  constructor
 156  · exact ⟨1, rfl, trivial⟩
 157  · exact h8.finite_local_events ℓ
 158
 159/-! ## Master Bridge Statement -/
 160
 161/-- **Master theorem (RG4)**: RS's 8-tick finite-resolution hypothesis yields Recognition Geometry's
 162finite-resolution axiom (RG4) for the induced locality and recognizer. -/

used by (3)

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

depends on (15)

Lean names referenced from this declaration's body.