M
plain-language theorem explainer
The definition supplies a concrete recognition structure on the unit type with equality as the recognition relation. Cost algebra derivations cite this to anchor defect distance bounds and J-cost estimates. It is constructed by direct record extension from the unit type and the structural equality predicate.
Claim. Let $M$ be the recognition structure whose underlying type is the unit type and whose recognition relation is equality.
background
RecognitionStructure is the record type consisting of a type $U$ together with a binary relation $R$ on $U$. The local setting in this module is T1, the meta-principle that nothing can recognize itself. The upstream minimal stub from Chain supplies a standalone compilation interface, while recog defines the relation by structural equality on the unit type.
proof idea
One-line wrapper that applies the record constructor to the unit type and the equality predicate recog.
why it matters
M supplies the base instance used by defectDist_nonneg, defectDist_quasi_triangle_local, and the quasi-triangle constant identity in CostAlgebra. It realizes the T1 step of the forcing chain and supports the zero-parameter hypothesis in MassToLight. The structure enables J-cost bounds to be derived from the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.