D_physical_compatible
plain-language theorem explainer
The theorem asserts that the physical spatial dimension satisfies the full RS compatibility structure. Researchers deriving D from the Recognition Science forcing chain would cite it to confirm that the observed dimension meets ledger conservation, eight-tick, and gap-synchronization requirements. The proof is a direct term application of the D = 3 compatibility theorem.
Claim. The physical spatial dimension satisfies the RS-compatible dimension conditions: it supports non-trivial linking for ledger conservation, obeys the eight-tick synchronization, and is compatible with gap-45 period divisibility.
background
The Dimension Forcing module proves that spatial dimension D = 3 is forced by the RS framework through topological linking and synchronization arguments. The RSCompatibleDimension structure is a Prop requiring three fields: SupportsNontrivialLinking D, EightTickFromDimension D = eight_tick, and 2^D divides sync_period. D_physical is the definition that sets the physical dimension to the constant 3. This result rests on the upstream D3_compatible theorem, which constructs the structure explicitly via D3_has_linking, reflexivity on the eight-tick equality, and a divisibility witness obtained by rewriting sync_period_eq_360.
proof idea
The proof is a one-line term wrapper that directly applies the D3_compatible theorem, using the definitional equality D_physical = 3.
why it matters
This declaration anchors the physical dimension inside the RS framework by verifying it satisfies the forcing conditions that select D = 3. It completes the compatibility interface for the physical case in the module that derives D from the eight-tick octave and gap-45 synchronization. The result supports the T8 step of the unified forcing chain and the ledger conservation arguments in the module documentation, though it has no immediate downstream uses listed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.