Bad
plain-language theorem explainer
Defines the bisection invariant for nested parameter intervals on an embedded arc in S^D: [u,v] sits inside [0,1] and the pushforward of a fixed reference 1-cycle into the complement of a([u,v]) is not a boundary. Cited by anyone running the nested-interval argument for arc-complement H_1-acyclicity (Hatcher 2B.1). Pure definitional packaging of four conjuncts; no proof content.
Claim. For real parameters $u,v$, the predicate $\mathrm{Bad}(u,v)$ holds when $0 \le u \le v \le 1$ and the pushforward of the reference singular $1$-cycle into the complement of the arc image $a([u,v]) \subset S^D$ is not a singular boundary.
background
The ambient space is the unit $D$-sphere $\mathrm{Sph},D$ in Euclidean space of dimension $D+1$, with $D=3$ the RS-forced spatial dimension (T8/T9). An arc $a$ is a continuous map from the unit interval into that sphere. For a subinterval $[u,v]\subseteq[0,1]$, $\mathrm{seg},a,u,v$ is the image $a([u,v])$, and $\mathrm{zSeg},a,z,u,v$ is the image of a fixed reference $1$-cycle $z$ under the chain map induced by inclusion of the full arc-complement into the smaller complement of that segment.
Boundaries are taken in the singular chain complex via $\mathrm{bnd}$, the degree-$(n+1)\to n$ differential on the coproduct presentation of chain groups. The module develops a formal singular-homology proof that every embedded arc in $S^D$ has $H_1$-acyclic complement, following Hatcher's arc case of theorem 2B.1.
proof idea
Definitional: four conjuncts conjoined. The first three force $[u,v]\subseteq[0,1]$ with correct order. The fourth is the non-boundary assertion $\neg\exists w,,\mathrm{zSeg},a,z,u,v=\mathrm{bnd}(\mathrm{complement\ of\ seg},a,u,v),1,w$. No tactics or lemmas; pure Prop packaging for the bisection loop.
why it matters
This is the invariant carried by the nested-interval sequence in the proof of arc-complement acyclicity. Downstream, bad_step shows every bad interval has a bad half of half the length; badSeq builds the nested sequence from an initial bad pair $(0,1)$; badSeq_le records the nested bounds. Those feed arcComplementsAcyclic, the formal Hatcher 2B.1 arc case: every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement in every dimension $D$.
In the RS forcing chain this underwrites linking-vanishing in high dimension and the $D=3$ spatial-dimension step (T8), since nontrivial linking needs a non-acyclic complement that only exists in low dimension. Verification-side uses (badPrediction, rs_derives_observables_strong) are name collisions on "bad", not consumers of this Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.