pith. machine review for the scientific record. sign in
theorem proved term proof high

not_1_4_signature

show as:
view Lean formalization →

Recognition Science forces the spatial dimension to equal 3. Researchers deriving Lorentzian spacetime from J-cost minimization cite this result to exclude a purely spatial 4D geometry. The proof reduces the negation directly to the definition of D_physical via simplification.

claimIn the Recognition Science framework the spatial dimension satisfies $D_s = 3$, hence $D_s$ is not equal to 4.

background

The module derives the full 4D Lorentzian structure from the J-cost functional and the T0-T8 forcing chain. Spatial directions carry positive metric sign because J''(1) = 1, while the 8-tick recognition operator supplies the single temporal direction with opposite sign. The upstream result D_physical from DimensionForcing fixes the spatial count at 3 and states that this value is RS-compatible.

proof idea

The proof is a one-line term wrapper that applies simp to the definitions of spatial_dim and D_physical, reducing the claim to the fact that D_physical equals 3.

why it matters in Recognition Science

Labeled SE-010, the theorem asserts that the (1,3) signature is the unique RS-compatible choice. It supplies the spatial half of the central module theorem that the metric diag(-1,+1,+1,+1), light cones, and proper time are forced by J-cost with zero free parameters. The result implements the T8 step of the chain and closes the spatial count before the full spacetime emergence is assembled.

scope and limits

formal statement (Lean)

 325theorem not_1_4_signature : ¬(spatial_dim = 4) := by simp [spatial_dim, D_physical]

proof body

Term-mode proof.

 326
 327/-- **SE-010: The signature (1, 3) is the UNIQUE RS-compatible signature.** -/

depends on (7)

Lean names referenced from this declaration's body.