IndisputableMonolith.Foundation.MultiAxisRobustness
Module on multi-axis robustness of forced spatial dimension D=3 in Recognition Science. It states the codimension formula for a recognized object of dimension p, proves that axes C, I, and A are robust, and shows the P-axis selects D (with p=1 giving D=3). Downstream the unified forcing chain imports it when closing T8. The argument is a short suite of codimension identities plus per-axis robustness lemmas over DimensionForcing.
claimFor a recognized object of dimension $p$, a codimension formula holds and the substrate dimension equals the forced value. Axes $C$, $I$, and $A$ are robust; the $P$-axis selects spatial dimension $D$, and $p=1$ forces $D=3$.
background
Recognition Science forces spatial dimension from the cost foundation rather than assuming it. The upstream DimensionForcing module proves $D=3$ by several independent routes (linking/topological and related arguments). This module sits one layer above that work: it packages how dimension and codimension interact for a recognized object of dimension $p$, and how that selection survives along named axes.
Sibling content centers on a codimension formula, equality of substrate dimension with the forced value, and three robustness predicates (axes $C$, $I$, $A$). A separate $P$-axis story selects $D$ and specializes to $p=1\Rightarrow D=3$. Notation is RS-native: $D$ is spatial dimension in the T8 slot of the forcing chain; $p$ is the dimension label of the recognized object entering the codimension identity.
The local setting is foundation-level inevitability, not phenomenology. Imports are Mathlib plus DimensionForcing; no cost-functional algebra is re-derived here.
proof idea
Not a single theorem: a small foundation module. Codimension and substrate-dimension statements are proved or recorded first (formula holds; substrate dimension equals the forced $D$). Robustness is then discharged axis by axis: separate lemmas for $C$, $I$, and $A$. The $P$-axis block shows that $P$ selects $D$, that moving along $P$ moves $D$, and that the $p=1$ case yields $D=3$. Proofs lean on DimensionForcing rather than reopening the four dimension-forcing arguments.
why it matters in Recognition Science
T8 in the primer is the claim that $D=3$ spatial dimensions are forced. This module supplies the multi-axis robustness layer that lets the unified forcing chain treat that conclusion as stable under the named axes, not a one-off identity. Downstream, UnifiedForcingChain imports the module while proving that T0–T8 are inevitabilities from the Recognition Composition Law and cost foundation; its stronger claim is that the whole chain, not only $\varphi$ pinning, is forced. Parent use is therefore chain closure at the dimension step, not a mass or coupling computation. Landmarks touched: T8 ($D=3$) and the forcing-chain architecture that consumes DimensionForcing.
scope and limits
- Does not re-prove $D=3$ from the linking or other DimensionForcing arguments.
- Does not derive the Recognition Composition Law, $J$-uniqueness, or $\varphi$ fixed-point (T5–T6).
- Does not address couplings, masses, or the $\alpha$ band.
- Does not claim robustness for axes outside the named $C$, $I$, $A$, and $P$ suite.
- Does not fix physical units or empirical error bars on $D$.
used by (1)
depends on (1)
declarations in this module (14)
-
def
CodimensionDimension -
def
CodimensionFormulaHolds -
def
SubstrateDimensionEquals -
def
AxisCRobust -
def
AxisIRobust -
def
AxisARobust -
theorem
axis_P_selects_D -
theorem
p_one_gives_D3 -
theorem
axis_P_moves_D -
theorem
axis_C_robust -
theorem
axis_I_robust -
theorem
axis_A_robust -
theorem
multi_axis_robustness -
theorem
p_one_route_agrees_with_dimension_forced