finite_resolution_no_chart_hypothesis
plain-language theorem explainer
Finite resolution blocks recognition charts on infinite neighborhoods whose images under the recognizer are finite. Researchers deriving local manifold structure from recognition axioms cite this when establishing cardinality obstructions to continuous coordinates. The definition directly encodes the pigeonhole mismatch as a reusable hypothesis for the obstruction result.
Claim. If a neighborhood $U$ of a configuration is infinite yet the recognizer maps it to only finitely many distinguishable events, then no local coordinate chart of any finite dimension exists with domain exactly $U$.
background
A recognition chart is a local coordinate map from a neighborhood $U$ to $ℝ^n$ that sends indistinguishable configurations to identical points and satisfies the neighborhood condition in the local structure. The module develops when recognition geometries admit local Euclidean-like coordinates, with the key tension that finite resolution prevents injections from infinite sets into finite images. This hypothesis rests on the recognizer and neighborhood definitions imported from the Recognition module.
proof idea
The declaration is a definition that directly packages the geometric axiom as a named hypothesis, with no internal proof or tactics.
why it matters
It supplies the premise for the theorem finite_resolution_no_chart that concludes non-existence of charts under these conditions. The definition implements the obstruction result from the Recognition Geometry paper. It enforces that local dimensions in the framework arise only from finite resolution cells, aligning with the derivation of three spatial dimensions from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.