pith. sign in
theorem

dimension_forced

proved
show as:

Why this theorem is linked from Gauge Theory Correlators from Non-Critical String Theory contradicts

Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.

The operators that couple to massive string states at level n acquire anomalous dimensions that grow as 2 (n g_YM sqrt(2 N))^{1/2} for large 't Hooft coupling. This is a new prediction about the strong coupling behavior of large N SYM theory.

CONTRADICTS: the theorem conflicts with this paper passage, or marks a claim that would need revision before publication.

module
IndisputableMonolith.Foundation.DimensionForcing
domain
Foundation
line
383 · github
papers citing
131 papers (below)

plain-language theorem explainer

The dimension forcing theorem asserts existence and uniqueness of a natural number D satisfying the RS compatibility conditions derived from ledger conservation via non-trivial linking and Alexander duality. Researchers deriving physical laws from the Recognition Science monolith would cite this to fix D without free parameters. The proof is a term-mode construction that exhibits D=3 via the compatibility theorem and invokes the uniqueness lemma for any other candidate.

Claim. There exists a unique natural number $D$ such that $D$ supports non-trivial linking for ledger conservation, satisfies $2^D = 8$, and has $2^D$ dividing the synchronization period.

background

Dimension is the type of natural numbers representing spatial dimension. RSCompatibleDimension D is the structure requiring three properties: SupportsNontrivialLinking D (from Alexander duality ensuring stable topological conservation), EightTickFromDimension D equals the eight-tick constant, and $2^D$ divides sync_period (for gap-45 synchronization). The module sets the local context that only D=3 meets these conditions, as D=1 or 2 lacks linking room while D>=4 unlinks everything by codimension. This rests on upstream D3_compatible (which verifies the three properties for D=3) and dimension_unique (which shows no other D works).

proof idea

The proof is a term-mode construction. It uses 3 as the witness for existence, applies the constructor to split the unique existence into the compatibility part and the uniqueness part, invokes the exact theorem D3_compatible to discharge the compatibility of 3, and applies dimension_unique to show that any other RSCompatibleDimension D must equal 3.

why it matters

This theorem places D=3 as the unique dimension compatible with the Recognition Science ledger, feeding directly into why_D_equals_3 which combines the result with spinor structure and eight-tick arguments. It realizes the T7 eight-tick octave and T8 forcing of D=3 from the unified forcing chain, converting the 8-tick and gap-45 synchronization into derived consequences rather than premises. The result closes the topological forcing step from Alexander duality (Hatcher 3.44) and supplies the dimension input to physical derivation certificates in Gap45.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.