SatisfiesRG5
plain-language theorem explainer
SatisfiesRG5 encodes the RG5 local regularity axiom for a recognizer r on local config space L by requiring that r is regular at every configuration. This forces resolution cells to remain connected within neighborhoods rather than fragmenting. Researchers deriving smooth geometry from discrete recognition would cite the axiom when showing that local blobs support continuous structure. The definition is a direct packaging of the IsRegular predicate into a single Prop structure.
Claim. Let $L$ be a local configuration space and $r$ a recognizer. The pair $(L,r)$ satisfies RG5 when $r$ is locally regular everywhere, i.e., for every configuration $c$ the resolution cell around $c$ remains recognition-connected inside a neighborhood of $c$.
background
The module develops recognition connectivity: two configurations are connected when a path between them stays inside one resolution cell. IsRecognitionConnected declares a set connected when all its points are equivalent under the recognizer. IsLocallyRegular requires that the preimage of any observed label stays connected when intersected with a neighborhood; the neighborhood itself is the set of all cells sharing the same observed label. SatisfiesRG5 packages the universal statement that every recognizer meets this local condition. Upstream, the neighborhood construction comes from RecognitionLatticeFromRecognizer, where the cell of a configuration lies in the neighborhood of its observed label.
proof idea
The declaration is a structure definition whose single field is the predicate IsRegular L r. IsRegular expands directly to the universal quantification over all configurations c of IsLocallyRegular L r c. No tactics or lemmas are applied; the structure simply names the RG5 axiom.
why it matters
SatisfiesRG5 supplies the RG5 axiom that connectivity_status invokes to conclude resolution cells are locally blob-like. In the Recognition framework this local coherence is required for smooth geometric structure to emerge from discrete recognition steps. It closes the gap between the recognition lattice and the continuous manifolds needed for classical physics, while leaving open how global topology follows from repeated local regularity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.