same_sector_forces_odd
plain-language theorem explainer
If the ambient dimension equals 2p+1 for some defect dimension p ≥ 1, then D is an odd integer at least 3. Anyone citing the allowed same-sector linking set A_A = {3,5,7,…} needs this arithmetic half of the characterization. The proof is pure omega arithmetic: lower bound from p ≥ 1, and parity by contradiction on a factor of 2.
Claim. For natural numbers $D$ and $p$ with $p \ge 1$ and $D = 2p+1$, one has $D \ge 3$ and $D$ is odd (i.e., $2 \nmid D$).
background
In the Recognition Science forcing chain, spatial dimension is pinned by linking nontriviality (T8). Same-sector linking of two $p$-spheres in $\mathbb{R}^D$ is topologically possible only when the dimension formula $D = 2p+1$ holds, so the ambient space is odd-dimensional. The module formalizes the paper's U5/U10 package: Alexander duality selects $D=3$ for loop-loop linking ($p=1$), while same-sector arithmetic alone permits every odd $D \ge 3$.
Here $p$ is the defect (sphere) dimension and $D$ the ambient spatial dimension. The hypothesis $p \ge 1$ excludes the degenerate $p=0$ case. Downstream, the allowed set $A_A$ is defined as those $D$ for which some $p \ge 1$ realizes same-sector linking; this lemma is the forward direction of that characterization.
proof idea
Term-mode proof by constructor on the conjunction.
- Left conjunct $D \ge 3$: substitute $D = 2p+1$ and apply
omegawith $p \ge 1$. - Right conjunct $\neg 2 \mid D$: assume $D = 2k$ for some $k$, rewrite via $D = 2p+1$, and let
omegaderive the contradiction (even equals odd).
No external lemmas; pure linear arithmetic on naturals.
why it matters
Feeds directly into allowed_set_A_characterization, whose doc-comment states: forward direction is "if same-sector linking exists for some $p \ge 1$, then $D$ is odd $\ge 3$", discharged by this theorem. That characterization is the Lean form of the paper's Proposition 3.5 claim $A_A = {3,5,7,\ldots}$.
In the framework this is the arithmetic half of the T8 dimension story: same-sector linking forces odd $D \ge 3$, while the loop-loop specialization $p=1$ (Alexander duality on the circle) forces the unique physical value $D=3$. Without this lemma the converse witnesses (witness_p, witness_D3, …) would have no matching forward filter. It closes the parity gap the paper left as an informal argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.