pith. sign in
module module high

IndisputableMonolith.Physics.DimensionalAnalysisFromConfigDim

show as:
view Lean formalization →

This module maps Recognition Science configuration dimensions onto the seven SI base quantities, separating five primary from two derived. Metrologists and physicists building dimensional bridges from RS-native units would cite the definitions. It is a definition module that introduces the quantity enumeration, partition, and certification object with no proofs inside.

claimThe module defines the enumeration of seven SI base quantities partitioned into a primary subset of five and a derived subset of two, together with a certification object for the resulting dimensional analysis.

background

Recognition Science works in RS-native units where the fundamental time quantum is τ₀ = 1 tick. The module supplies the dimensional layer that converts configuration dimensions into the standard SI set. It introduces BaseQuantity as the enumeration type, baseQuantity_count as its cardinality, si_partition as the split into primary and derived, and DimensionalAnalysisCert as the certifying structure.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the base quantities and si_partition that feed DimensionalAnalysisCert and the sibling certification objects inside the same file. It supplies the concrete link from the RS time quantum to SI metrology required by the physics domain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)