pith. sign in
module module low

IndisputableMonolith.Sociology.LegalTraditionsFromConfigDim

show as:
view Lean formalization →

The Sociology.LegalTraditionsFromConfigDim module formalizes legal traditions derived from configuration dimensions in the Recognition Science framework. It depends solely on the Constants module that sets the fundamental time quantum τ₀ = 1 tick. The module supplies definitions for legal traditions, their counts, and certificates. Researchers extending RS into sociology would cite these objects. This is a definition module with no proofs.

claimThe module introduces the type of legal traditions $L$, a counting function $c : L → ℕ$, and certification predicates $C$ all derived from configuration dimension $d$.

background

The module sits in the Sociology domain and imports Mathlib together with IndisputableMonolith.Constants. The upstream Constants module supplies the single fact that the fundamental RS time quantum is τ₀ = 1 tick. No further definitions or theorems are supplied by the module itself beyond the sibling objects LegalTradition, legalTradition_count, LegalTraditionsCert and legalTraditionsCert.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module extends the Recognition Science framework into sociology by supplying the listed definitions. It feeds no parent theorems; the used_by count is zero. It rests on the time-quantum definition from the imported Constants module.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)