EightTickFiniteResolution
plain-language theorem explainer
EightTickFiniteResolution encodes that measurement outcomes on each recognition neighborhood remain finite. Recognition Science modelers cite it to connect the eight-tick cycle to discrete local states in the geometry bridge. The declaration is a direct structural definition that introduces the finite_local_events field with no derivation.
Claim. Let $L$ be a ledger space satisfying the configuration axioms and let $E$ be an event type. Given a recognition operator inducing neighborhoods on $L$ and a measurement map $m:L→E$, the property asserts that for every ledger state $ℓ$ the image of its recognition neighborhood under $m$ is a finite set.
background
RSConfigSpace treats ledger states as a nonempty type with decidable equality, supplying the configuration space for the universe ledger. RSLocalityFromRHat equips this space with a recognition operator whose neighborhoods satisfy self-inclusion, refinement, and transitivity. RSMeasurement supplies the map from ledger states to observable events together with a nontriviality condition. The module uses these structures to instantiate Recognition Geometry axioms from Recognition Science ledger data, with the eight-tick cycle providing the finite-resolution link.
proof idea
This declaration is a structural definition; it introduces the finite_local_events field directly with no lemmas or tactics applied.
why it matters
The definition supplies the hypothesis for eight_tick_implies_RG4, which shows Recognition Science satisfies the finite-resolution axiom of Recognition Geometry. It is packaged into the master result RS_instantiates_RG. The construction directly encodes the eight-tick octave as the source of local discreteness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.