count_in_spectrum
plain-language theorem explainer
Cross-domain structural theorems total 27, placing the count inside the 25-45 spectrum. Analysts of meta-universality patterns reference this bound when certifying the layer's completeness. The proof unfolds the constant definition and lets the decision procedure confirm the inequalities.
Claim. $25 ≤ N ≤ 45$, where $N$ is the number of joint structural theorems in the wave-64 cross-domain layer.
background
The module lists 27 cross-domain theorems (C1–C27) that encode universality patterns such as 5×5×5 state spaces, phi-ladder ratios, gap-45 ceilings, and cube cardinalities. The definition crossDomainModuleCount fixes this total at 27. The present theorem supplies the spectrum check required by the meta-claim for the layer.
proof idea
Unfold the definition of crossDomainModuleCount to obtain the literal 27. Split the conjunction via refine and discharge both inequalities with the decide tactic.
why it matters
The result populates the count_in_spectrum_range field of metaTheoremCountCert. It closes the meta-counting step for the cross-domain layer, which aggregates the listed universality results including J-equilibrium and phi-ladder instances. No new axioms are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.