IndisputableMonolith.Mathematics.LogicSystemsFromConfigDim
This module defines logic systems and related counts and certificates derived from configuration dimension in the Recognition Science setting. Researchers formalizing the logical foundations of dimensional physics would reference these objects. The module is strictly definitional with no proofs or theorems.
claimLet $d$ denote configuration dimension. A logic system is a structure over $d$, with a count function returning the number of systems for each $d$, and a certification proposition asserting their validity, all relative to the base time quantum.
background
The module imports Mathlib and IndisputableMonolith.Constants. The latter supplies the fundamental RS time quantum with doc-comment stating it is the RS-native time quantum where τ₀ = 1 tick. The module introduces the type for a logic system, a counting function over dimensions, and a certification proposition. These objects model how logic systems arise from configuration dimension.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the core definitions for logic systems derived from configuration dimension. It connects to the constants module and is positioned to support higher-level results on the logical structure of physics in the IndisputableMonolith library, though no downstream uses are listed in the current graph.
scope and limits
- Does not contain any theorem statements or proof bodies.
- Does not import modules beyond Mathlib and Constants.
- Does not define or reference the forcing chain or J-function.
- Does not provide numerical values or explicit formulas for the count function.