patterns_match_D
plain-language theorem explainer
The cross-domain layer of Recognition Science covers exactly five universality patterns. Researchers auditing the meta-count of structural theorems cite this equality to confirm pattern coverage in the C28 meta-claim. The proof is a one-line reflexivity that matches the constant definition of patternsCovered.
Claim. The number of universality patterns covered by the cross-domain theorems equals five.
background
The module supplies the meta-count for the cross-domain layer, which contains 27 theorems labeled C1 through C27 plus this declaration as C28. The definition patternsCovered identifies five patterns: D=5, 2³=8, J=0, φ-ladder, gap45. The local setting is a structural meta-claim that quantifies joint structural theorems with zero sorry or axiom, as stated in the module doc-comment.
proof idea
The proof is a term-mode reflexivity that directly matches the constant definition of patternsCovered.
why it matters
This equality supplies the patterns_covered field inside metaTheoremCountCert. It supports the lower bound on the number of cross-domain theorems and aligns with framework landmarks including the eight-tick octave (2³) and the φ-ladder. It closes one piece of the meta-count scaffolding for the cross-domain layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.