connectivity_status
plain-language theorem explainer
The connectivity_status definition produces a status string affirming that recognition-connected sets include the empty collection, singletons, resolution cells and their subsets, while local regularity (RG5) holds at points and constants remain regular. Module auditors in Recognition Geometry cite it to confirm completion of the connectivity layer before advancing to global structure. The implementation is a direct string concatenation of fixed property messages with no computation or lemma application.
Claim. The connectivity status string reports that recognition-connected sets are defined, the empty set and singletons are connected, resolution cells are connected, subsets inherit connectivity, local regularity holds at points (RG5), global regularity holds, the RG5 axiom is satisfied, local regularity implies cell connectivity, and constants are regular. This completes the connectivity and local regularity (RG5) layer.
background
In Recognition Geometry a set is recognition-connected when all its points are equivalent under the recognition relation, so they lie inside one resolution cell. Local regularity (RG5) requires that preimages under the recognition map stay connected inside neighborhoods, preventing fragmentation such as Cantor sets. The module therefore treats resolution cells as coherent atoms that support smooth geometric emergence from discrete recognition steps.
proof idea
The definition constructs the status string by direct concatenation of eleven fixed messages, one for each listed property (empty-set connectivity, singleton connectivity, resolution-cell connectivity, subset inheritance, local regularity at a point, global regularity, RG5 satisfaction, cell connectivity from RG5, and constant regularity) followed by a completion line. No tactics, lemmas, or upstream calls are executed inside the body.
why it matters
This definition supplies a human-readable checkpoint that the RG5 axiom structure is in place, confirming resolution cells remain coherent rather than fragmenting. The module documentation states that such coherence lets resolution cells function as the atoms of recognition geometry and allows smooth physics to emerge. It closes the connectivity section of the Recognition framework even though the dependency graph shows no downstream uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.