Foundation Multi Axis Robustness P One Route Agrees With Dimension Forced

The agreement theorem

The theorem p_one_route_agrees_with_dimension_forced is a formal statement in the machine-checked library of the Recognition Science framework. It says, in plain terms, that the route to three-dimensional space through the dimension of a recognized object agrees exactly with the route that forces the dimension directly from the cost function. The agreement is not approximate and not a heuristic: it is a proved equality between the two routes' outputs.

The route in question starts with a recognized object of dimension p. The framework's definition gives the substrate dimension as 2p + 1. For p = 1, that formula yields 3. The theorem states that this value, 3, is the unique dimension that is compatible with the framework's earlier dimension-forcing result. The word "unique" matters: the theorem proves there is exactly one such dimension, not merely that one exists. The proof is a direct computation, and the compatibility with the forced dimension is itself a proved fact, not an assumption.

What the theorem does not claim is just as important as what it proves. It does not claim that the other axes of robustness mentioned in the framework's paper, such as the coefficient ring, the tracked invariant, or acyclicity, are proved. Those remain named stability obligations, not theorems. The framework's own documentation is explicit: their former stubs were removed rather than kept as empty claims. The theorem also does not claim that p = 1 is derived from first principles here; it takes p = 1 as the case that gives D = 3 and proves the agreement for that case.

The consequence is a tighter foundation. A reader can now see that the two independent-looking routes to three dimensions in the framework do not contradict each other. They land on the same number, and the proof is checked. This does not make the physical claim that space is three-dimensional; it makes the formal claim that within the framework's definitions, the codimension route and the forcing route agree.

/-- The `p = 1` codimension case is `D = 3`. -/
theorem p_one_gives_D3 :
    CodimensionDimension 1 = 3 := by
  rfl

/-- Compatibility with the existing dimension forcing result: once `p = 1`,
the codimension route agrees with the existing forced dimension. -/
theorem p_one_route_agrees_with_dimension_forced :
    ∃! D : DimensionForcing.Dimension,
      D = CodimensionDimension 1 ∧ DimensionForcing.RSCompatibleDimension D := by
  refine ⟨3, ?_, ?_⟩
  · constructor
    · rfl
    · exact DimensionForcing.D3_compatible
  · intro D hD
    exact hD.1.trans (by rfl)

/-- Bundled multi-axis robustness theorem (Axis P content).

Only Axis P can move the dimension away from `3`. Axes C, I, and A remain
named stability obligations of the paper; they are not claimed as theorems
here until a non-trivial substrate model exists. -/
theorem multi_axis_robustness :
    (∀ p : ℕ, 1 ≤ p → p ≠ 1 → CodimensionDimension p ≠ 3) ∧
      CodimensionDimension 1 = 3 :=
  ⟨axis_P_moves_D, p_one_gives_D3⟩

What this page does not claim

The theorem does not prove that p = 1 is the only possible value from physical principles; it proves agreement for that case. The theorem does not claim the other robustness axes are stable; those remain open obligations. The theorem does not assert that three-dimensional space is physically real; it asserts a formal agreement within the framework.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/MultiAxisRobustness.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: