IndisputableMonolith.Physics.DimensionalAnalysisFromConfigDim
Module that packages SI dimensional analysis inside Recognition Science: seven base quantities split as five primary and two derived. It exposes the BaseQuantity type, the count, the SI partition, and a DimensionalAnalysisCert certificate. Physicists checking unit consistency of RS-native constants (c, ħ, G) against SI would cite it. The module is largely definitional scaffolding plus a thin certificate wrapper.
claimThe module fixes seven SI base quantities, partitioned as five primary and two derived, and supplies a certificate that dimensional analysis is consistent with the RS configuration dimension. Main objects: the type of base quantities, the count $7$, the SI partition, and the dimensional-analysis certificate.
background
Recognition Science works in RS-native units where $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$. Bridging those units to laboratory SI requires a clean account of the seven SI base quantities (length, mass, time, electric current, temperature, amount of substance, luminous intensity).
This module sits in the Physics domain and imports only Mathlib and the RS Constants module (whose fundamental time quantum is $\tau_0=1$ tick). It introduces BaseQuantity, the count of base quantities, an explicit SI partition into five primary and two derived quantities, and a DimensionalAnalysisCert that records the consistency claim.
The local setting is therefore pure dimensional bookkeeping: no dynamics, only the combinatorial skeleton needed before mass ladders or coupling constants are expressed in SI.
proof idea
This is primarily a definition module. BaseQuantity, baseQuantity_count, and si_partition are data declarations encoding the seven SI bases and the 5+2 split. DimensionalAnalysisCert and dimensionalAnalysisCert form a thin certificate layer that packages the partition as a named Prop/instance pair. No deep tactic proofs appear; the argument is definitional plus a one-line certificate construction.
why it matters in Recognition Science
Dimensional consistency is a prerequisite for any claim that RS-native constants match measured SI values (the $\alpha^{-1}$ band, the mass yardstick, $G=\varphi^5/\pi$). The module supplies the SI side of that bridge: seven bases, five primary plus two derived. Downstream physics certificates that convert $\varphi$-ladder masses or eight-tick periods into SI units can import this partition rather than re-encoding SI by hand. No parent theorems currently list it in used_by, so it is infrastructure awaiting those conversion lemmas.
scope and limits
- Does not derive the numerical values of c, ħ, or G in SI.
- Does not prove uniqueness of the 5+2 partition from first principles.
- Does not treat natural-unit conversions beyond the certificate interface.
- Does not encode derived SI units (newton, joule, etc.) explicitly.
- Does not connect to the forcing chain T0–T8 or the mass ladder.