nontrivial_recognition_forces_lattice
plain-language theorem explainer
Nontrivial recognition on a carrier K forces existence of a primitive interface I such that the quotient recognition lattice is nonempty. Workers on the observer layer cite this when moving from distinction events to lattice structure. The proof obtains the interface via the upstream forcing result and exhibits one cell using cellOf.
Claim. If a type $K$ admits nontrivial recognition, then there exists a primitive interface $I$ on $K$ such that the recognition lattice generated by $I$ is nonempty.
background
The RecognitionLattice for an interface I is the quotient of the carrier K by the interfaceSetoid, i.e., the set of kernel equivalence classes. A PrimitiveInterface consists of a positive natural number n and an observation map from K to Fin n. NontrivialRecognition K asserts the existence of a pair of configurations distinguished by equalityDistinction.
proof idea
The term proof introduces the hypothesis and destructures the result of nontrivial_recognition_forces_interface to obtain an interface I and a point x. It then constructs the nonempty proof by supplying the cell cellOf I x as the witness.
why it matters
This theorem provides the from_nontrivial field in the recognitionLatticeCert definition, completing the assembly of lattice properties including kernel equivalence and the logicNat interpretation. It realizes the claim that a non-trivial recognition event forces a recognition lattice, as stated in the module documentation. In the broader framework it marks the transition from raw distinction to the quotient structure that precedes spatial geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.