average_per_pattern
plain-language theorem explainer
The theorem records that the cross-domain module count multiplied by ten equals 270, which encodes the average of 5.4 modules per pattern across the five patterns referenced in the module comment. Meta-theorists auditing the enumeration of joint structural theorems in the Recognition Science cross-domain layer would cite this identity to verify arithmetic closure of the count. The proof is a direct decision procedure on the constant definition of the module count.
Claim. Let $n$ denote the number of cross-domain modules in the wave-64 layer. Then $n$ times 10 equals 270.
background
The module supplies C28, the meta-count for the cross-domain layer of Recognition Science. It enumerates 27 theorems (C1 through C27) spanning cognitive state spaces, phi-ladder universality, J-equilibrium, cube-face counts, and related structural identities, with total 27 and zero sorry or axiom. The sole upstream result is the definition crossDomainModuleCount : ℕ := 27, which supplies the concrete integer used in the equality.
proof idea
One-line wrapper that applies the decide tactic to the numerical equality obtained from the definition of the module count.
why it matters
The declaration closes the arithmetic verification step inside the meta-count of 27 cross-domain theorems. It supports the module's claim of a quantifiable lower bound on joint structural theorems without introducing new hypotheses. No downstream results are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.