legalTraditionsCert
plain-language theorem explainer
This definition constructs the certificate for five legal traditions by populating the structure field with the cardinality theorem. Sociologists or Recognition Science modelers extending the framework to jurisprudence would cite it when mapping configuration dimension five to the major legal families. The construction is a direct one-line structure instantiation that references the decide-proven count.
Claim. A certificate structure asserts that the type of legal traditions has cardinality five. The definition supplies an instance of this structure by direct assignment of the theorem establishing the cardinality.
background
The module states that five canonical legal traditions correspond to configuration dimension five: civil law (Roman-Germanic), common law, Islamic (sharia), customary, and socialist/post-socialist. These are claimed to cover more than 95 percent of the world's jurisdictions. The upstream cardinality theorem proves the count equals five by decision procedure, and the structure packages this equality as a formal certificate.
proof idea
The definition is a one-line wrapper. It constructs the certificate structure by assigning its field the value of the cardinality theorem proved by decide.
why it matters
This definition completes the certificate for legal traditions in the sociology module, supplying the formal link from configuration dimension five to jurisprudence. It extends the forcing chain dimension count (T8) into social structures without introducing new axioms. No downstream uses appear, so it functions as a terminal fact in this branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.