Observation Refinement Beyond a Fixed Carrier, with Constrained Observation Design

   1 \documentclass[11pt]{article}
   2 \usepackage[margin=1in]{geometry}
   3 \usepackage{amsmath,amssymb,amsthm,mathtools}
   4 \usepackage{booktabs,tabularx,array,longtable}
   5 \usepackage{xcolor}
   6 \usepackage{enumitem}
   7 \usepackage{hyperref}
   8 \usepackage{microtype}
   9 \usepackage{tikz-cd}
  10 \usepackage{fancyhdr}
  11 \usepackage{titlesec}
  12 \usepackage{newtxtext,newtxmath}
  13 
  14 \definecolor{navy}{RGB}{35,55,85}
  15 \definecolor{softblue}{RGB}{235,242,250}
  16 \definecolor{softgray}{RGB}{246,246,246}
  17 \definecolor{softgreen}{RGB}{237,247,240}
  18 \definecolor{softgold}{RGB}{251,246,232}
  19 \definecolor{softred}{RGB}{251,238,238}
  20 \hypersetup{colorlinks=true,linkcolor=navy,citecolor=navy,urlcolor=navy}
  21 \titleformat{\section}{\Large\bfseries\color{navy}}{\thesection}{0.7em}{}
  22 \titleformat{\subsection}{\large\bfseries\color{navy}}{\thesubsection}{0.7em}{}
  23 \pagestyle{fancy}
  24 \setlength{\headheight}{14pt}
  25 \fancyhf{}
  26 \lhead{ProLT Observation Refinement}
  27 \rhead{Classification note v0.2}
  28 \cfoot{\thepage}
  29 \setlength{\parindent}{0pt}
  30 \setlength{\parskip}{0.55em}
  31 
  32 \newtheorem{theorem}{Theorem}[section]
  33 \newtheorem{proposition}[theorem]{Proposition}
  34 \newtheorem{lemma}[theorem]{Lemma}
  35 \newtheorem{corollary}[theorem]{Corollary}
  36 \theoremstyle{definition}
  37 \newtheorem{definition}[theorem]{Definition}
  38 \newtheorem{example}[theorem]{Example}
  39 \newtheorem{remark}[theorem]{Remark}
  40 
  41 \newcommand{\F}{\mathbb F_2}
  42 \newcommand{\Om}{\Omega_P}
  43 \newcommand{\truth}{\varsigma}
  44 \newcommand{\OX}{\mathcal O}
  45 \newcommand{\Cone}{\operatorname{Cone}}
  46 \newcommand{\im}{\operatorname{im}}
  47 \newcommand{\rank}{\operatorname{rank}}
  48 \newcommand{\xor}{\mathbin{\Updownarrow}}
  49 \newcommand{\redhom}{\widetilde H}
  50 \newcommand{\statusS}{\textbf{[S]}}
  51 \newcommand{\statusA}{\textbf{[A]}}
  52 \newcommand{\statusC}{\textbf{[C]}}
  53 \newcommand{\down}{\mathord\downarrow}
  54 \newcommand{\up}{\mathord\uparrow}
  55 
  56 \begin{document}
  57 
  58 \begin{center}
  59 {\LARGE\bfseries\color{navy} Observation Refinement in Propositional Logical Topologies}\par
  60 \vspace{0.3em}
  61 {\large Fiber profiles, adjoint criteria, Quillen fibers, refinement defects, and the limits of complete classification}\par
  62 \vspace{0.65em}
  63 {\normalsize Working research note v0.2 --- 23 September 2026}\par
  64 \vspace{0.3em}
  65 {\small Follow-up to \emph{Homological Foundations for Propositional Logical Topologies}, built on the ProLT core manuscript v0.8.}
  66 \end{center}
  67 
  68 \vspace{0.7em}
  69 \noindent\colorbox{softgold}{\parbox{0.96\textwidth}{
  70 \textbf{Status convention.} \statusS\ denotes standard finite-poset/algebraic-topological mathematics. \statusA\ denotes a direct ProLT specialization or elementary theorem derived from the v0.8 signature framework. \statusC\ denotes a potentially publishable ProLT-specific formulation, invariant, or algorithmic consequence whose novelty should be subjected to a dedicated literature audit before any priority claim.
  71 }}
  72 
  73 \section{Question and answer in one page}
  74 
  75 Let \(\Phi=(\phi_i)_{i\in I}\) be an observation family and let \(\Psi\) extend \(\Phi\) by new observations. The v0.8 ProLT theory gives the realized-signature posets
  76 \[
  77 P_\Phi=o_\Phi(\Om),\qquad P_\Psi=o_\Psi(\Om),
  78 \]
  79 ordered by inclusion, and a canonical forgetful refinement map
  80 \[
  81 r_{\Psi\Phi}:P_\Psi\longrightarrow P_\Phi
  82 \]
  83 obtained by deleting the new coordinates. The corresponding order complexes are
  84 \[
  85 \OX_\Phi=\Delta(P_\Phi),\qquad \OX_\Psi=\Delta(P_\Psi).
  86 \]
  87 The central problem is:
  88 
  89 \begin{center}
  90 \emph{When does adding observations change only the resolution of the presentation, and when does it change the homotopy or homology of the observable-state space?}
  91 \end{center}
  92 
  93 The main results of this note give a hierarchy of answers.
  94 
  95 \begin{enumerate}[label=\textbf{R\arabic*.},leftmargin=2.7em]
  96 \item Every refinement admits an exact \emph{fiber-profile normal form}: over each coarse signature \(p\), record exactly which new-coordinate signatures occur. This completely reconstructs \(P_\Psi\) and the map \(r_{\Psi\Phi}\).
  97 \item The refinement is \emph{topologically redundant} exactly when every coarse state has one new profile and those profiles are monotone. Equivalently, \(r_{\Psi\Phi}\) is an order isomorphism.
  98 \item If the refinement does not split coarse states, then \(\OX_\Psi\) is literally a subcomplex of \(\OX_\Phi\). A coarse chain survives exactly when its new-coordinate profiles increase along the chain. For one new Boolean observation, the deleted chains are precisely those containing a \(1\to0\) descent.
  99 \item There are simple signature-level sufficient criteria for homotopy invariance. If every lower refinement fiber has a greatest element, or every upper refinement fiber has a least element, then \(r_{\Psi\Phi}\) has an order adjoint and is a homotopy equivalence. For one observation \(\psi\), this says: \emph{possibility of \(\psi\)} or \emph{forced truth of \(\psi\)} must be monotone in the coarse information order.
 100 \item More generally, Quillen--McCord/Barmak fiber criteria apply. Contractible principal fibers imply a simple homotopy equivalence; acyclic principal fibers imply homology equivalence.
 101 \item Homology equivalence has an exact finite test: the refinement mapping cone is acyclic. In the non-splitting case it reduces to ordinary relative homology \(H_*(\OX_\Phi,\OX_\Psi)\).
 102 \item There is no unrestricted algorithmic classification of homotopy-neutral refinements: arbitrary finite posets can be realized as refined signature posets above a one-point coarse space, so the problem contains finite-complex contractibility, which is undecidable. Homology neutrality, by contrast, remains decidable by finite boundary-matrix computation.
 103 \end{enumerate}
 104 
 105 \section{Base ProLT data and refinement map}
 106 
 107 Let \(P=\{p_1,\dots,p_n\}\) be a finite propositional variable set and \(\Om=\{0,1\}^P\) its valuation space. For a formula \(L\), write
 108 \[
 109 \truth(L)=\{v\in\Om:v\models L\}.
 110 \]
 111 For an indexed observation family \(\Phi=(\phi_i)_{i\in I}\), define
 112 \[
 113 o_\Phi(v)=\{i\in I:v\models\phi_i\}\subseteq I.
 114 \]
 115 The v0.8 ProLT results identify topological indistinguishability with equality of signatures and the specialization preorder with inclusion:
 116 \[
 117 v\sim_\Phi w\iff o_\Phi(v)=o_\Phi(w),
 118 \qquad
 119 v\preceq_\Phi w\iff o_\Phi(v)\subseteq o_\Phi(w).
 120 \]
 121 Hence the Kolmogorov quotient is the finite poset
 122 \[
 123 P_\Phi=o_\Phi(\Om)\subseteq 2^I
 124 \]
 125 with inclusion order.
 126 
 127 Suppose now that
 128 \[
 129 \Psi=(\Phi,\Theta)
 130 \]
 131 extends \(\Phi\) by a disjointly indexed family \(\Theta=(\theta_a)_{a\in A}\). Then
 132 \[
 133 o_\Psi(v)=\bigl(o_\Phi(v),o_\Theta(v)\bigr)
 134 \in 2^I\times 2^A,
 135 \]
 136 and the coordinate-forgetting map
 137 \[
 138 r=r_{\Psi\Phi}:P_\Psi\to P_\Phi,
 139 \qquad
 140 r(s)=s\cap I,
 141 \]
 142 is surjective and monotone.
 143 
 144 \section{The fiber-profile normal form}
 145 
 146 \begin{definition}[Coarse state and refinement profile]\label{def:profile}
 147 For \(p\in P_\Phi\), let
 148 \[
 149 C_p:=o_\Phi^{-1}(p)
 150 \]
 151 be the coarse observational state represented by \(p\). Define its \emph{new-coordinate fiber profile}
 152 \[
 153 \mathcal B_p:=o_\Theta(C_p)
 154 =\{o_\Theta(v):v\in C_p\}\subseteq 2^A.
 155 \]
 156 Each \(\mathcal B_p\) is nonempty.
 157 \end{definition}
 158 
 159 \begin{theorem}[Fiber-profile normal form]\label{thm:normalform}
 160 \statusA/\statusC\;
 161 Let
 162 \[
 163 Q_{\mathcal B}
 164 :=\{(p,a):p\in P_\Phi,\ a\in\mathcal B_p\}
 165 \subseteq P_\Phi\times2^A
 166 \]
 167 with product order
 168 \[
 169 (p,a)\le(q,b)
 170 \iff p\le q\text{ in }P_\Phi\text{ and }a\subseteq b.
 171 \]
 172 Then
 173 \[
 174 P_\Psi\cong Q_{\mathcal B}
 175 \]
 176 as posets, under separation of old and new coordinates. Under this isomorphism the refinement map is exactly the first-coordinate projection
 177 \[
 178 r(p,a)=p.
 179 \]
 180 Consequently the family \((\mathcal B_p)_{p\in P_\Phi}\) determines the refined signature poset and the refinement projection completely.
 181 \end{theorem}
 182 
 183 \begin{proof}
 184 Every realized \(\Psi\)-signature comes from a valuation \(v\) and splits uniquely as
 185 \[
 186 (o_\Phi(v),o_\Theta(v))=(p,a)
 187 \]
 188 with \(a\in\mathcal B_p\). Conversely, every pair in \(Q_{\mathcal B}\) is realized by the definition of \(\mathcal B_p\). Inclusion of the combined signatures is coordinatewise inclusion because the old and new index sets are disjoint. The projection statement is immediate.
 189 \end{proof}
 190 
 191 \begin{remark}[Point fibers are not Quillen fibers]\label{rem:pointfiber}
 192 The direct point fiber
 193 \[
 194 r^{-1}(p)=\{p\}\times\mathcal B_p
 195 \]
 196 records only how the coarse state \(p\) splits. Quillen-type theorems use instead the preimages of principal ideals or filters,
 197 \[
 198 r^{-1}(\down p),\qquad r^{-1}(\up p),
 199 \]
 200 which also remember how the split pieces compare with states below or above \(p\). This distinction is essential: every point fiber can be contractible while the refinement still changes homotopy type.
 201 \end{remark}
 202 
 203 \section{Exact classification of topological redundancy}
 204 
 205 The v0.8 manuscript calls a new observation topologically redundant when its truth region is already open in the old ProLT. The fiber normal form turns this into an exact signature-level theorem for an arbitrary finite block of added observations.
 206 
 207 \begin{theorem}[Redundancy/order-isomorphism theorem]\label{thm:redundancy}
 208 \statusA/\statusC\;
 209 For a refinement \(\Psi=(\Phi,\Theta)\), the following are equivalent.
 210 \begin{enumerate}[label=(\roman*)]
 211 \item \(\tau_\Psi=\tau_\Phi\) on the fixed valuation carrier \(\Om\).
 212 \item Every new truth region \(\truth(\theta_a)\), \(a\in A\), is already \(\tau_\Phi\)-open.
 213 \item Every fiber profile is a singleton,
 214 \[
 215 \mathcal B_p=\{\alpha(p)\},
 216 \]
 217 and the resulting map
 218 \[
 219 \alpha:P_\Phi\to2^A
 220 \]
 221 is isotone:
 222 \[
 223 p\le q\Longrightarrow\alpha(p)\subseteq\alpha(q).
 224 \]
 225 \item The refinement projection \(r:P_\Psi\to P_\Phi\) is an order isomorphism.
 226 \end{enumerate}
 227 \end{theorem}
 228 
 229 \begin{proof}
 230 The equivalence of (i) and (ii) is the definition of equality of the generated topologies: \(\tau_\Phi\subseteq\tau_\Psi\) automatically, and equality holds exactly when each new subbasic truth region is old-open.
 231 
 232 Assume (i). If two valuations lie in the same old signature class \(C_p\), they are topologically indistinguishable in \(\tau_\Phi\); equality of topologies makes them indistinguishable in \(\tau_\Psi\) as well. Thus the new signature is constant on \(C_p\), giving \(\mathcal B_p=\{\alpha(p)\}\). If \(p\le q\), choose \(v\in C_p\), \(w\in C_q\). The old specialization relation gives \(v\preceq_\Phi w\). Equality of topologies gives \(v\preceq_\Psi w\), hence \(\alpha(p)\subseteq\alpha(q)\). Therefore (iii) holds.
 233 
 234 Assume (iii). For each new coordinate \(a\in A\), the set
 235 \[
 236 U_a:=\{p\in P_\Phi:a\in\alpha(p)\}
 237 \]
 238 is upward closed. By the signature representation of the ProLT topology,
 239 \[
 240 \truth(\theta_a)=o_\Phi^{-1}(U_a)
 241 \]
 242 is \(\tau_\Phi\)-open. Hence (ii).
 243 
 244 Under (iii), Theorem~\ref{thm:normalform} identifies \(P_\Psi\) with the graph \(\{(p,\alpha(p))\}\). Monotonicity of \(\alpha\) says
 245 \[
 246 p\le q\iff(p,\alpha(p))\le(q,\alpha(q)),
 247 \]
 248 so projection is an order isomorphism. Conversely, if projection is an order isomorphism then every fiber has one point and its inverse is necessarily isotone, giving (iii).
 249 \end{proof}
 250 
 251 \begin{remark}
 252 This theorem separates three notions which should not be conflated:
 253 \begin{enumerate}[label=(\alph*)]
 254 \item \emph{no splitting}: each \(\mathcal B_p\) is a singleton;
 255 \item \emph{no order deletion}: the singleton profile map is isotone;
 256 \item \emph{full redundancy}: both hold, equivalently the topology is unchanged.
 257 \end{enumerate}
 258 A refinement can leave every coarse equivalence class intact while still deleting one-way specialization comparisons.
 259 \end{remark}
 260 
 261 \section{Non-splitting refinements and chain deletion}
 262 
 263 \begin{definition}[Non-splitting refinement]
 264 A refinement is \emph{non-splitting} if every \(\mathcal B_p\) is a singleton. Write
 265 \[
 266 \mathcal B_p=\{\alpha(p)\}.
 267 \]
 268 No monotonicity of \(\alpha\) is assumed.
 269 \end{definition}
 270 
 271 \begin{theorem}[Order deletion theorem]\label{thm:orderdelete}
 272 \statusA/\statusC\;
 273 For a non-splitting refinement, identify the fine and coarse vertex sets through the bijection \(r\). Then
 274 \[
 275 p\le_\Psi q
 276 \iff
 277 p\le_\Phi q\ \text{and}\ \alpha(p)\subseteq\alpha(q).
 278 \]
 279 Consequently
 280 \[
 281 \le_\Psi\ \subseteq\ \le_\Phi
 282 \]
 283 and
 284 \[
 285 \OX_\Psi\subseteq\OX_\Phi
 286 \]
 287 as a simplicial subcomplex on the same vertex set. A coarse chain
 288 \[
 289 p_0<p_1<\cdots<p_k
 290 \]
 291 survives the refinement exactly when
 292 \[
 293 \alpha(p_0)\subseteq\alpha(p_1)\subseteq\cdots\subseteq\alpha(p_k).
 294 \]
 295 \end{theorem}
 296 
 297 \begin{proof}
 298 In the fiber-profile normal form the unique fine point over \(p\) is \((p,\alpha(p))\). Product order gives the displayed criterion. Every fine chain is therefore a coarse chain; conversely, a coarse chain is fine exactly when its new profiles are coordinatewise nondecreasing.
 299 \end{proof}
 300 
 301 \begin{corollary}[One-bit descent criterion]\label{cor:descent}
 302 Suppose one new Boolean observation \(\psi\) is constant on each coarse class, and write
 303 \[
 304 b(p)\in\{0,1\}
 305 \]
 306 for its value on \(C_p\). Then a coarse chain \(p_0<\cdots<p_k\) survives exactly when
 307 \[
 308 b(p_0)\le b(p_1)\le\cdots\le b(p_k).
 309 \]
 310 Equivalently, it is deleted exactly when it contains a \(1\to0\) inversion.
 311 \end{corollary}
 312 
 313 \begin{corollary}[Post-\(T_0\) refinement filtration]\label{cor:T0filtration}
 314 \statusA/\statusC\;
 315 If \(X_\Phi\) is already \(T_0\) on the valuation carrier, then \(o_\Phi\) is injective, so every later observation refinement is automatically non-splitting. Thus a sequence
 316 \[
 317 \Phi_0\subseteq\Phi_1\subseteq\cdots\subseteq\Phi_T
 318 \]
 319 with \(X_{\Phi_0}\) \(T_0\) yields, after identifying vertices with valuations,
 320 \[
 321 \OX_{\Phi_T}\subseteq\cdots\subseteq\OX_{\Phi_1}\subseteq\OX_{\Phi_0}.
 322 \]
 323 Hence ordinary persistence can be applied after reversing the refinement index; zigzag persistence is not required while observations are only added.
 324 \end{corollary}
 325 
 326 \begin{proof}
 327 A coarse signature class contains a single valuation when \(o_\Phi\) is injective, so it cannot split further as a set. Theorem~\ref{thm:orderdelete} then applies at every later stage.
 328 \end{proof}
 329 
 330 \section{Relative defect chains in the non-splitting case}
 331 
 332 The preceding inclusion lets the mapping-cone defect from the foundation note be sharpened.
 333 
 334 \begin{theorem}[Refinement defect becomes relative homology]\label{thm:relativecone}
 335 \statusS/\statusA\;
 336 For a non-splitting refinement, under the vertex identification of Theorem~\ref{thm:orderdelete}, the induced simplicial map is the inclusion
 337 \[
 338 \OX_\Psi\hookrightarrow\OX_\Phi.
 339 \]
 340 Therefore the mapping-cone refinement defect satisfies
 341 \[
 342 D_k(\Psi/\Phi;R)
 343 \cong
 344 H_k(\OX_\Phi,\OX_\Psi;R).
 345 \]
 346 \end{theorem}
 347 
 348 \begin{definition}[Refinement-descent chain complex]\label{def:descentcomplex}
 349 For a non-splitting refinement define \(C_k^{\mathrm{desc}}(\Psi/\Phi;R)\) to be the free \(R\)-module generated by the coarse \(k\)-chains that fail the survival condition
 350 \[
 351 \alpha(p_0)\subseteq\cdots\subseteq\alpha(p_k).
 352 \]
 353 Its boundary is the ordinary simplicial boundary followed by deletion of every face that does survive the refinement.
 354 \end{definition}
 355 
 356 \begin{proposition}[Exact descent-chain computation]\label{prop:descentcomplex}
 357 \statusA/\statusC\;
 358 There is a natural chain isomorphism
 359 \[
 360 C_*^{\mathrm{desc}}(\Psi/\Phi;R)
 361 \cong
 362 C_*(\OX_\Phi,\OX_\Psi;R).
 363 \]
 364 Hence
 365 \[
 366 D_k(\Psi/\Phi;R)
 367 \cong
 368 H_k(C_*^{\mathrm{desc}}(\Psi/\Phi;R)).
 369 \]
 370 For one added Boolean observation, the generators are exactly coarse chains containing a \(1\to0\) descent.
 371 \end{proposition}
 372 
 373 \begin{proof}
 374 The simplicial chain group of \(\OX_\Phi\) is free on its simplices, and the subcomplex \(\OX_\Psi\) is spanned by exactly the surviving simplices. The quotient chain group therefore has the nonsurviving simplices as a basis. Its differential is the coarse simplicial differential modulo the surviving submodule, which is precisely the stated rule.
 375 \end{proof}
 376 
 377 \section{Adjoint criteria: an elementary homotopy-neutral class}
 378 
 379 For \(p\in P_\Phi\), define the principal refinement fibers
 380 \[
 381 L_p:=r^{-1}(\down p),
 382 \qquad
 383 U_p:=r^{-1}(\up p).
 384 \]
 385 The following test is much easier than computing arbitrary homotopy types.
 386 
 387 \begin{theorem}[Greatest-lower-fiber / least-upper-fiber criterion]\label{thm:adjoint}
 388 \statusS/\statusA/\statusC\;
 389 Let
 390 \[
 391 \mathsf U(p)
 392 :=\bigcup_{\substack{q\le p\\a\in\mathcal B_q}}a,
 393 \qquad
 394 \mathsf L(p)
 395 :=\bigcap_{\substack{q\ge p\\a\in\mathcal B_q}}a.
 396 \]
 397 Then:
 398 \begin{enumerate}[label=(\roman*)]
 399 \item \(L_p\) has a greatest element if and only if
 400 \[
 401 \mathsf U(p)\in\mathcal B_p.
 402 \]
 403 When this holds, the greatest element is \((p,\mathsf U(p))\).
 404 \item \(U_p\) has a least element if and only if
 405 \[
 406 \mathsf L(p)\in\mathcal B_p.
 407 \]
 408 When this holds, the least element is \((p,\mathsf L(p))\).
 409 \end{enumerate}
 410 If (i) holds for every \(p\), then \(r\) has a right adjoint. If (ii) holds for every \(p\), then \(r\) has a left adjoint. Either global condition implies that
 411 \[
 412 \Delta(r):\OX_\Psi\to\OX_\Phi
 413 \]
 414 is a homotopy equivalence.
 415 \end{theorem}
 416 
 417 \begin{proof}
 418 Suppose \(L_p\) has greatest element \((q,a_*)\). Since \(r\) is surjective, choose some \((p,b)\in r^{-1}(p)\subseteq L_p\). Greatness gives \((p,b)\le(q,a_*)\), so \(p\le q\le p\) and therefore \(q=p\). The second coordinate \(a_*\) contains every new signature occurring over every \(q\le p\), hence contains \(\mathsf U(p)\). Since \(a_*\) itself occurs in the union, equality follows. Conversely, if \(\mathsf U(p)\in\mathcal B_p\), then every \((q,a)\in L_p\) satisfies
 419 \[
 420 q\le p,\qquad a\subseteq\mathsf U(p),
 421 \]
 422 so \((p,\mathsf U(p))\) is greatest. This proves (i). The proof of (ii) is dual.
 423 
 424 If every lower fiber has a greatest element, define
 425 \[
 426 s_R(p):=(p,\mathsf U(p)).
 427 \]
 428 Then
 429 \[
 430 r(x)\le p\iff x\le s_R(p),
 431 \]
 432 so \(r\dashv s_R\). In particular \(r s_R=\mathrm{id}\) and
 433 \[
 434 \mathrm{id}\le s_Rr.
 435 \]
 436 Order-preserving maps that are pointwise comparable induce homotopic maps on order complexes, so \(\Delta(s_R)\) is a homotopy inverse to \(\Delta(r)\). The left-adjoint case is dual.
 437 \end{proof}
 438 
 439 \subsection{A sharp one-observation interpretation}
 440 
 441 Let \(\psi\) be one newly added observation. For each coarse state \(C_p\), define
 442 \[
 443 M_\psi(p)=
 444 \begin{cases}
 445 1,&\text{some }v\in C_p\text{ satisfies }\psi,\\
 446 0,&\text{otherwise},
 447 \end{cases}
 448 \]
 449 and
 450 \[
 451 m_\psi(p)=
 452 \begin{cases}
 453 1,&\text{every }v\in C_p\text{ satisfies }\psi,\\
 454 0,&\text{otherwise}.
 455 \end{cases}
 456 \]
 457 Thus \(M_\psi\) records \emph{possibility} of the new observation inside a coarse state, while \(m_\psi\) records \emph{forced truth}. The possible fiber profiles are
 458 \[
 459 \{0\},\qquad\{1\},\qquad\{0,1\},
 460 \]
 461 with
 462 \[
 463 m_\psi(p)=\min\mathcal B_p,
 464 \qquad
 465 M_\psi(p)=\max\mathcal B_p.
 466 \]
 467 
 468 \begin{corollary}[Possible/forced monotonicity criterion]\label{cor:possibleforced}
 469 \statusA/\statusC\;
 470 For a one-observation refinement:
 471 \begin{enumerate}[label=(\roman*)]
 472 \item \(r\) has a right adjoint if and only if \(M_\psi:P_\Phi\to\{0,1\}\) is isotone.
 473 \item \(r\) has a left adjoint if and only if \(m_\psi:P_\Phi\to\{0,1\}\) is isotone.
 474 \end{enumerate}
 475 Equivalently, either of the following is sufficient for homotopy invariance:
 476 \begin{itemize}
 477 \item the coarse states in which \(\psi\) is \emph{possible} form an upset;
 478 \item the coarse states in which \(\psi\) is \emph{forced} form an upset.
 479 \end{itemize}
 480 Topological redundancy is the stronger special case
 481 \[
 482 m_\psi=M_\psi=b
 483 \]
 484 with \(b\) isotone.
 485 \end{corollary}
 486 
 487 \begin{proof}
 488 For one bit,
 489 \[
 490 \mathsf U(p)=\max_{q\le p}M_\psi(q).
 491 \]
 492 The membership condition \(\mathsf U(p)\in\mathcal B_p\) is equivalent to \(\mathsf U(p)=M_\psi(p)\), which for every \(p\) is exactly isotonicity of \(M_\psi\). Dually,
 493 \[
 494 \mathsf L(p)=\min_{q\ge p}m_\psi(q)
 495 \]
 496 and \(\mathsf L(p)\in\mathcal B_p\) for every \(p\) is exactly isotonicity of \(m_\psi\).
 497 \end{proof}
 498 
 499 \section{Quillen--McCord/Barmak fiber criteria}
 500 
 501 The adjoint criterion forces a cone point in every principal fiber. Quillen's fiber theorem permits much more general contractible fibers.
 502 
 503 \begin{theorem}[Contractible-fiber criterion]\label{thm:quillen}
 504 \statusS/\statusA\;
 505 If for every \(p\in P_\Phi\), the order complex
 506 \[
 507 \Delta\bigl(r^{-1}(\down p)\bigr)
 508 \]
 509 is contractible, then
 510 \[
 511 \Delta(r):\OX_\Psi\longrightarrow\OX_\Phi
 512 \]
 513 is a simple homotopy equivalence, hence a homotopy equivalence. Dually, the same conclusion follows if every
 514 \[
 515 \Delta\bigl(r^{-1}(\up p)\bigr)
 516 \]
 517 is contractible.
 518 \end{theorem}
 519 
 520 \begin{proof}
 521 The lower-fiber statement is the finite-poset McCord--Quillen theorem together with Barmak's strengthening to simple homotopy equivalence. The upper-fiber statement follows by applying the theorem to opposite posets.
 522 \end{proof}
 523 
 524 \begin{theorem}[Acyclic-fiber homology criterion]\label{thm:acyclicfiber}
 525 \statusS/\statusA\;
 526 Fix coefficients \(R\). If
 527 \[
 528 \redhom_i\!\left(\Delta(r^{-1}(\down p));R\right)=0
 529 \]
 530 for every \(p\in P_\Phi\) and every \(i\ge0\), then
 531 \[
 532 r_*:H_i(\OX_\Psi;R)\longrightarrow H_i(\OX_\Phi;R)
 533 \]
 534 is an isomorphism for every \(i\). The dual upper-fiber statement also holds.
 535 \end{theorem}
 536 
 537 \begin{remark}[Sufficient, not necessary]\label{rem:notnecessary}
 538 The principal-fiber conditions are powerful but not necessary. Section~\ref{sec:examples} gives a concrete ProLT refinement for which \(r\) is a homotopy equivalence even though one lower principal fiber and one upper principal fiber are each two disconnected points. Thus neither orientation of the Quillen test succeeds, despite homotopy neutrality.
 539 \end{remark}
 540 
 541 \section{Exact homology classification by the refinement cone}
 542 
 543 The homotopy problem is difficult in full generality, but the homology problem has an exact algebraic answer.
 544 
 545 \begin{definition}[Refinement mapping cone]
 546 Let
 547 \[
 548 r_\#:C_*(\OX_\Psi;R)\longrightarrow C_*(\OX_\Phi;R)
 549 \]
 550 be the induced chain map. Define
 551 \[
 552 \mathsf D_*(\Psi/\Phi;R)=\Cone(r_\#)
 553 \]
 554 and
 555 \[
 556 D_k(\Psi/\Phi;R)=H_k(\mathsf D_*(\Psi/\Phi;R)).
 557 \]
 558 \end{definition}
 559 
 560 \begin{theorem}[Exact homology-equivalence criterion]\label{thm:coneexact}
 561 \statusS/\statusA/\statusC\;
 562 The following are equivalent:
 563 \begin{enumerate}[label=(\roman*)]
 564 \item \(r_*:H_k(\OX_\Psi;R)\to H_k(\OX_\Phi;R)\) is an isomorphism for every \(k\);
 565 \item
 566 \[
 567 D_k(\Psi/\Phi;R)=0
 568 \qquad\text{for every }k.
 569 \]
 570 \end{enumerate}
 571 Thus the refinement cone gives an exact, finite homological classification of whether the refinement is homology-neutral.
 572 \end{theorem}
 573 
 574 \begin{proof}
 575 The standard mapping-cone long exact sequence is
 576 \[
 577 \cdots\to H_k(\OX_\Psi)
 578 \overset{r_*}{\longrightarrow}H_k(\OX_\Phi)
 579 \to D_k(\Psi/\Phi)
 580 \to H_{k-1}(\OX_\Psi)\to\cdots.
 581 \]
 582 Exactness gives the equivalence.
 583 \end{proof}
 584 
 585 \begin{corollary}[Quick obstructions]
 586 If any of the following differs between \(\OX_\Psi\) and \(\OX_\Phi\), the refinement is not homology-neutral:
 587 \begin{enumerate}[label=(\alph*)]
 588 \item a Betti number over the chosen field;
 589 \item the number of connected components;
 590 \item the Euler characteristic.
 591 \end{enumerate}
 592 The converses are false in general.
 593 \end{corollary}
 594 
 595 \subsection{An exact \(H_0\) criterion}
 596 
 597 \begin{proposition}[Connected-component criterion]\label{prop:H0}
 598 \statusA\;
 599 Let \(\pi_0(P)\) denote connected components of the undirected comparability graph of a finite poset \(P\). Since \(r\) is surjective, the induced map
 600 \[
 601 r_*:H_0(\OX_\Psi;R)\to H_0(\OX_\Phi;R)
 602 \]
 603 is always surjective. It is an isomorphism if and only if, for every connected component \(C\subseteq P_\Phi\), the inverse image
 604 \[
 605 r^{-1}(C)
 606 \]
 607 is connected.
 608 \end{proposition}
 609 
 610 \begin{proof}
 611 A connected component of \(P_\Psi\) maps into one component of \(P_\Phi\) because comparability paths map to comparability-or-equality paths. Surjectivity of \(r\) ensures every coarse component receives at least one fine component. On \(H_0\), each fine component generator maps to the generator of its coarse component. The map is injective exactly when no coarse component receives more than one fine component.
 612 \end{proof}
 613 
 614 \section{A strict hierarchy of refinement-neutrality tests}\label{sec:hierarchy}
 615 
 616 It is useful to distinguish five levels.
 617 
 618 \begin{center}
 619 \begin{tabular}{cl}
 620 \toprule
 621 Class & Condition \\
 622 \midrule
 623 \(\mathsf R\) & \(r\) is an order isomorphism (topological redundancy) \\
 624 \(\mathsf A\) & \(r\) has a left or right order adjoint \\
 625 \(\mathsf Q\) & all lower or all upper principal refinement fibers are contractible \\
 626 \(\mathsf H\) & \(\Delta(r)\) is a homotopy equivalence \\
 627 \(\mathsf M\) & \(r_*\) is a homology isomorphism \\
 628 \bottomrule
 629 \end{tabular}
 630 \end{center}
 631 
 632 Standard implications and the preceding theorems give
 633 \[
 634 \boxed{
 635 \mathsf R\subseteq\mathsf A\subseteq\mathsf Q\subseteq\mathsf H\subseteq\mathsf M.
 636 }
 637 \]
 638 The examples below show that the first three inclusions are already strict in very small Boolean ProLTs. The universality result of Section~\ref{sec:universality} shows that \(\mathsf H\subsetneq\mathsf M\) also occurs in unrestricted ProLT refinements by importing any finite acyclic noncontractible complex.
 639 
 640 \section{Worked Boolean examples}\label{sec:examples}
 641 
 642 Throughout, signatures are ordered by inclusion and coefficients for displayed homology groups are \(\F\).
 643 
 644 \subsection{Redundant: adding \(X\wedge Y\) to \((X,Y)\)}
 645 
 646 Let
 647 \[
 648 \Phi=(X,Y),\qquad \psi=X\wedge Y.
 649 \]
 650 The coarse signatures are
 651 \[
 652 D=\varnothing,
 653 \quad A=\{X\},
 654 \quad C=\{Y\},
 655 \quad B=\{X,Y\},
 656 \]
 657 forming the Boolean diamond. The new bit is
 658 \[
 659 b(D)=b(A)=b(C)=0,
 660 \qquad b(B)=1.
 661 \]
 662 It is isotone, so Theorem~\ref{thm:redundancy} applies. The refinement is in \(\mathsf R\): the ProLT topology and canonical order complex are unchanged, although a weighted signature metric may change if the redundant coordinate is assigned positive weight.
 663 
 664 \subsection{Adjoint-neutral but nonredundant: adding \(X\) to no observations}
 665 
 666 Take one propositional variable \(X\), let \(\Phi\) be the empty observation family, and refine by \(\Psi=(X)\). The coarse poset is a point; the fine poset is the two-element chain
 667 \[
 668 0<1.
 669 \]
 670 The projection to a point has both a left adjoint (choose the minimum) and a right adjoint (choose the maximum), so it is a homotopy equivalence. The topology nevertheless changes from indiscrete to Sierpi\'nski. Thus this refinement lies in \(\mathsf A\setminus\mathsf R\).
 671 
 672 \subsection{Quillen-neutral but no adjoint: adding XOR to \((X,Y)\)}
 673 
 674 Let
 675 \[
 676 \Phi=(X,Y),\qquad \psi=X\xor Y.
 677 \]
 678 The new-bit profile on \((D,A,C,B)\) is
 679 \[
 680 (0,1,1,0).
 681 \]
 682 No coarse class splits, but the old comparisons \(A<B\) and \(C<B\) are deleted. The fine poset has \(D\) as a minimum and three elements \(A,C,B\) above it. Hence its order complex is a cone and is contractible.
 683 
 684 The bit is not isotone, so neither the possible nor forced map is isotone; no adjoint criterion applies. However every lower Quillen fiber is contractible: over \(D,A,C\) it is a point or edge, and over \(B\) it is the entire fine poset, again a cone. Therefore the refinement lies in
 685 \[
 686 \mathsf Q\setminus\mathsf A.
 687 \]
 688 
 689 \subsection{Homotopy-neutral while both Quillen orientations fail}\label{ex:alternating}
 690 
 691 Take
 692 \[
 693 \Phi=(X\wedge Y,\ X,\ X\vee Y).
 694 \]
 695 On the four valuations \(00,01,10,11\), the realized signatures form a four-element chain
 696 \[
 697 p_0<p_1<p_2<p_3
 698 \]
 699 with
 700 \[
 701 \begin{array}{c|c}
 702 00&\varnothing\\
 703 01&\{X\vee Y\}\\
 704 10&\{X,X\vee Y\}\\
 705 11&\{X\wedge Y,X,X\vee Y\}.
 706 \end{array}
 707 \]
 708 Add
 709 \[
 710 \psi=\neg Y.
 711 \]
 712 Its profile along the chain is
 713 \[
 714 1,0,1,0.
 715 \]
 716 No coarse class splits. The surviving strict comparisons are
 717 \[
 718 p_0<p_2,
 719 \qquad
 720 p_1<p_2,
 721 \qquad
 722 p_1<p_3.
 723 \]
 724 Thus \(\OX_\Psi\) is a three-edge tree, while \(\OX_\Phi\) is a \(3\)-simplex. Both are nonempty and contractible, so the refinement projection is a homotopy equivalence.
 725 
 726 Nevertheless,
 727 \[
 728 r^{-1}(\down p_1)=\{p_0,p_1\}
 729 \]
 730 is a two-point antichain, and
 731 \[
 732 r^{-1}(\up p_2)=\{p_2,p_3\}
 733 \]
 734 is also a two-point antichain. Hence the lower-fiber Quillen criterion fails and the dual upper-fiber criterion fails. This gives a concrete refinement in
 735 \[
 736 \mathsf H\setminus\mathsf Q.
 737 \]
 738 
 739 \subsection{Homology-active: adding negation to \((X)\)}
 740 
 741 Let
 742 \[
 743 \Phi=(X),\qquad \Psi=(X,\neg X).
 744 \]
 745 The coarse signature poset is a two-element chain, so \(\OX_\Phi\) is an edge. The fine signatures \(\{X\}\) and \(\{\neg X\}\) are incomparable, so \(\OX_\Psi\) is two isolated points. Hence
 746 \[
 747 H_0(\OX_\Phi)\cong\F,
 748 \qquad
 749 H_0(\OX_\Psi)\cong\F^2.
 750 \]
 751 The refinement is not homology-neutral. The mapping cone gives
 752 \[
 753 D_1(\Psi/\Phi;\F)\cong\F,
 754 \qquad D_0(\Psi/\Phi;\F)=0.
 755 \]
 756 This is the smallest example in which adding an observation splits a connected coarse information structure into disconnected fine states.
 757 
 758 \subsection{Splitting can still be homotopy-neutral}
 759 
 760 Let \(\Phi=(X)\) on two variables \(X,Y\), and add \(Y\). Each coarse \(X\)-state splits into the two possible \(Y\)-values, so
 761 \[
 762 \mathcal B_{\varnothing}=\mathcal B_{\{X\}}=\{0,1\}.
 763 \]
 764 The coarse poset is an edge and the fine poset is the Boolean diamond. Both are contractible. In fact both the possible map \(M_Y\equiv1\) and the forced map \(m_Y\equiv0\) are isotone, so the projection has both adjoints. This shows that state splitting by itself does not imply a topological defect.
 765 
 766 \section{Small exhaustive verification}
 767 
 768 To test the logical hierarchy independently of the proofs, the accompanying script exhaustively enumerates every one-bit refinement profile over every nonempty subposet of the Boolean square \(B_2\). A coarse point may have new-bit fiber \(\{0\}\), \(\{1\}\), or \(\{0,1\}\). There are \(255\) such refinement instances in total.
 769 
 770 The verifier checks redundancy, left/right section-adjoint criteria, lower-fiber contractibility by finite beat-point reduction, lower-fiber acyclicity over \(\F\), the Betti numbers of the coarse and fine order complexes, and the mapping-cone Betti numbers. It finds exactly five logical pattern types under those tests:
 771 \[
 772 \begin{array}{c|r}
 773 (\mathsf R,\mathsf A,\mathsf Q_{\downarrow},\mathsf{Acyc}_{\downarrow},\mathsf M)&\text{count}\\\hline
 774 (0,0,0,0,0)&24\\
 775 (0,0,0,0,1)&16\\
 776 (0,0,1,1,1)&20\\
 777 (0,1,1,1,1)&144\\
 778 (1,1,1,1,1)&51
 779 \end{array}
 780 \]
 781 These finite checks are not substitutes for the theorems, but they verify the example calculations and demonstrate that the sufficient conditions are genuinely non-equivalent even at very small size.
 782 
 783 \section{Universality of refinement and the limit of complete homotopy classification}\label{sec:universality}
 784 
 785 The preceding criteria invite the question whether one could push further to a complete effective homotopy classification. In unrestricted dimension the answer is negative.
 786 
 787 \begin{theorem}[Universality of refined signature posets]\label{thm:universality}
 788 \statusA/\statusC\;
 789 Every finite poset \(Q\) is isomorphic to the realized-signature poset of some finite propositional observation family. More strongly, \(Q\) can occur as \(P_\Psi\) in a refinement
 790 \[
 791 \Phi\subseteq\Psi
 792 \]
 793 for which \(P_\Phi\) is a single point.
 794 \end{theorem}
 795 
 796 \begin{proof}
 797 Take enough propositional variables that \(|\Om|\ge|Q|\), and choose a surjection
 798 \[
 799 h:\Om\twoheadrightarrow Q.
 800 \]
 801 Let the coarse observation family \(\Phi\) be empty, so \(P_\Phi\) is one point. Index new observations by the elements \(q\in Q\). For each \(q\), prescribe the truth set
 802 \[
 803 T_q:=\{v\in\Om:q\le h(v)\}.
 804 \]
 805 Every subset of a finite valuation space is definable by a propositional formula, for example by the disjunction of the complete minterms of its members. Choose \(\theta_q\) with \(\truth(\theta_q)=T_q\).
 806 
 807 If \(h(v)=x\), then the new observation signature is
 808 \[
 809 o_\Psi(v)=\{q\in Q:q\le x\}=\down x.
 810 \]
 811 The map \(x\mapsto\down x\) is an order embedding of \(Q\) into \(2^Q\), because
 812 \[
 813 x\le y\iff\down x\subseteq\down y.
 814 \]
 815 Surjectivity of \(h\) realizes every such signature and no others. Hence \(P_\Psi\cong Q\).
 816 \end{proof}
 817 
 818 \begin{corollary}[Every finite simplicial homotopy type occurs]\label{cor:alltypes}
 819 For every finite simplicial complex \(K\), choose its face poset \(Q=\mathcal X(K)\). Then
 820 \[
 821 \Delta(Q)=\operatorname{sd}(K),
 822 \]
 823 the barycentric subdivision of \(K\). Therefore a refinement above a one-point coarse ProLT can realize the homotopy type of any finite simplicial complex.
 824 \end{corollary}
 825 
 826 \begin{theorem}[Undecidability of unrestricted homotopy-neutral refinement]\label{thm:undecidable}
 827 \statusS/\statusA/\statusC\;
 828 There is no algorithm that, for arbitrary finite ProLT observation refinements in unrestricted dimension, always decides whether
 829 \[
 830 \Delta(r_{\Psi\Phi})
 831 \]
 832 is a homotopy equivalence.
 833 \end{theorem}
 834 
 835 \begin{proof}
 836 Given a finite simplicial complex \(K\), apply Corollary~\ref{cor:alltypes} to construct a refinement whose coarse signature poset is a point and whose fine order complex has the homotopy type of \(K\). The refinement projection to the point is a homotopy equivalence exactly when \(K\) is contractible. Algorithmic recognition of contractibility for arbitrary finite simplicial complexes is undecidable. Thus a universal decision algorithm for homotopy-neutral ProLT refinements would decide an undecidable problem.
 837 \end{proof}
 838 
 839 \begin{corollary}[Homology remains effectively computable]\label{cor:decidablehomology}
 840 For any fixed computable coefficient field, homology-neutrality of a given finite refinement is decidable: construct the finite mapping-cone boundary matrices and compute their ranks. Thus the homotopy and homology classification problems diverge sharply in unrestricted generality.
 841 \end{corollary}
 842 
 843 \begin{remark}[Strictness of \(\mathsf H\subsetneq\mathsf M\)]
 844 The universality theorem also imports standard acyclic noncontractible finite complexes. For example, a finite triangulation of a punctured Poincar\'e homology sphere is acyclic but has nontrivial fundamental group. Refining a point to its face poset gives a homology equivalence to the point which is not a homotopy equivalence.
 845 \end{remark}
 846 
 847 \section{A practical classification algorithm}
 848 
 849 The theory suggests the following release-quality workflow for a concrete observation refinement.
 850 
 851 \begin{enumerate}[label=\textbf{Step \arabic*.},leftmargin=4em]
 852 \item \textbf{Build the coarse poset.} Compute the realized old signatures \(P_\Phi\) and their inclusion order.
 853 \item \textbf{Build fiber profiles.} For each \(p\in P_\Phi\), compute
 854 \[
 855 \mathcal B_p=o_\Theta(C_p).
 856 \]
 857 No fine-poset construction is conceptually necessary beyond these profiles.
 858 \item \textbf{Check exact redundancy.} If every \(\mathcal B_p\) is singleton and the profile map is isotone, the refinement is an order isomorphism and the classification stops.
 859 \item \textbf{Check adjoints.} Compute \(\mathsf U(p)\) and \(\mathsf L(p)\). If all \(\mathsf U(p)\in\mathcal B_p\), or all \(\mathsf L(p)\in\mathcal B_p\), the refinement is homotopy-neutral.
 860 \item \textbf{Check principal fibers.} Apply beat-point/collapse tests or another contractibility certificate to \(r^{-1}(\down p)\) and \(r^{-1}(\up p)\). Uniform contractibility certifies simple homotopy equivalence. Uniform acyclicity certifies homology equivalence.
 861 \item \textbf{Compute the exact homology defect.} Build \(\Cone(r_\#)\). Nonzero \(D_k\) proves that the refinement changes homology. Vanishing of all \(D_k\) proves homology equivalence.
 862 \item \textbf{For non-splitting refinements, use descent chains.} Replace the general mapping cone by the relative/descent chain complex of Proposition~\ref{prop:descentcomplex}.
 863 \item \textbf{Do not treat an inconclusive homotopy test as failure.} The Quillen and adjoint criteria are sufficient, not necessary. In unrestricted dimension no complete decision algorithm exists. For a research theorem, restrict to a structurally controlled subclass.
 864 \end{enumerate}
 865 
 866 \section{Promising theorem targets after this classification}
 867 
 868 The classification above narrows the next research questions substantially.
 869 
 870 \begin{enumerate}[label=\textbf{T\arabic*.},leftmargin=2.8em]
 871 \item \textbf{Logical criteria for contractible Quillen fibers.} Find syntactic or semantic conditions on newly added formulas that force every \(r^{-1}(\down p)\) to have a cone point, beat-point reduction, or nerve decomposition.
 872 \item \textbf{Minimal homology-changing observations.} Given \(\Phi\), characterize or optimize observations \(\psi\) for which \(D_k((\Phi,\psi)/\Phi)\neq0\), possibly with a cost on formulas or observations.
 873 \item \textbf{Post-\(T_0\) persistence.} Study the reverse filtration of Corollary~\ref{cor:T0filtration}. Determine whether logical properties of the added observations constrain barcode births/deaths in the relative descent complexes.
 874 \item \textbf{Refinement/update interaction.} Combine the contravariant-looking refinement deletion \(\OX_\Psi\subseteq\OX_\Phi\) after \(T_0\) with premise restriction subcomplexes. This should yield a two-parameter family indexed by observational resolution and admissible-state restriction.
 875 \item \textbf{Cross-layer comparison.} Relate refinement defects in canonical order-complex homology to changes in the presentation-sensitive Dowker compatibility complex and to changes in metric/Rips persistence. A nontrivial comparison theorem would be substantially stronger than defining the layers independently.
 876 \item \textbf{Restricted decidable classes.} Because unrestricted homotopy neutrality is undecidable, identify meaningful ProLT classes where the problem becomes decidable or efficiently certifiable: bounded poset height, bounded number of observations, distributive-lattice images, monotone formula fragments, or bounded treewidth of the comparability/Hasse graph.
 877 \end{enumerate}
 878 
 879 \section{Preliminary novelty positioning}
 880 
 881 The finite-poset fiber theorems, adjunction-homotopy principle, mapping cones, and undecidability of arbitrary finite-complex contractibility are standard mathematics. They should not be claimed as new. The current contribution candidates are instead the \emph{ProLT-specific synthesis and sharpenings}: the refinement fiber-profile normal form; the exact redundancy theorem in signature terms; the possible/forced monotonicity criterion; the descent-chain description after \(T_0\); the refinement-defect hierarchy; and the universality reduction formulated for propositional observation refinement.
 882 
 883 A preliminary literature check found adjacent but distinct areas. Formal concept analysis and information-system theory study binary object--attribute data and attribute reduction. Separately, Gaucher used the phrase ``refinement of observation'' in directed homotopy theory for flows and finite bounded posets, with preservation results for branching/merging homology and underlying homotopy type. That is not the same object as the ProLT signature-projection refinement studied here, but the terminology overlap should be acknowledged in any publication. A dedicated adversarial novelty audit remains necessary before promoting any \statusC\ item to a novelty claim.
 884 
 885 \section{Conclusion}
 886 
 887 Observation refinement in a ProLT is not a single phenomenon. It may:
 888 \begin{itemize}
 889 \item add a coordinate without changing the topology at all;
 890 \item split observational states while preserving homotopy type;
 891 \item leave all states unsplit but delete specialization comparisons;
 892 \item change homotopy while preserving homology;
 893 \item or change homology itself.
 894 \end{itemize}
 895 
 896 The fiber-profile normal form makes these possibilities explicit. It reduces every refinement to a structured surjective poset map
 897 \[
 898 Q_{\mathcal B}\longrightarrow P_\Phi.
 899 \]
 900 Topological redundancy is exactly order isomorphism. Adjoint and Quillen-fiber tests give progressively broader homotopy-neutral classes. Mapping-cone homology gives an exact finite test for homology neutrality. Once the old ProLT is \(T_0\), refinement becomes especially transparent: it can no longer split vertices, so it acts only by deleting chains from the canonical order complex, and the defect is ordinary relative homology generated by the deleted descent chains.
 901 
 902 The universality theorem also tells us where to stop looking for an all-purpose homotopy decision rule: unrestricted refinement already contains the full contractibility problem for finite complexes. The productive research direction is therefore not a mythical universal criterion, but a theory of \emph{logically natural subclasses} in which the fiber geometry can be controlled and related back to observations, premises, and eventually time-evolving logical state spaces.
 903 
 904 \appendix
 905 \section{Computational verification summary}
 906 
 907 The accompanying verifier constructs order complexes and normalized simplicial chain maps explicitly over \(\F\). It verifies:
 908 \begin{enumerate}[label=(\roman*)]
 909 \item the redundant \(X\wedge Y\) example has identical coarse/fine Betti vector \((1,0,0)\) and zero cone homology;
 910 \item the XOR refinement has coarse Betti \((1,0,0)\), fine Betti \((1,0)\), and zero cone homology;
 911 \item the negation split has coarse Betti \((1,0)\), fine Betti \((2)\), and cone Betti \((0,1)\);
 912 \item the splitting-but-neutral \(Y\) refinement of \((X)\) has zero cone homology;
 913 \item the four-chain alternating profile \((1,0,1,0)\) yields contractible coarse and fine complexes while failing both lower and upper Quillen-fiber tests;
 914 \item all \(255\) one-bit profiles over nonempty subposets of \(B_2\) agree with the logical hierarchy reported in Section~\ref{sec:hierarchy}.
 915 \end{enumerate}
 916 
 917 \begin{thebibliography}{99}
 918 \bibitem{Theory2026}
 919 B. Theory,
 920 \emph{Propositional Logical Topology: Observation, Distinguishability, and Inference},
 921 core manuscript v0.8, September 2026, unpublished.
 922 
 923 \bibitem{TheoryHomology2026}
 924 B. Theory,
 925 \emph{Homological Foundations for Propositional Logical Topologies},
 926 working research note v0.1, September 2026, unpublished.
 927 
 928 \bibitem{McCord1966}
 929 M. C. McCord,
 930 ``Singular homology groups and homotopy groups of finite topological spaces,''
 931 \emph{Duke Mathematical Journal} 33 (1966), 465--474.
 932 
 933 \bibitem{Quillen1978}
 934 D. Quillen,
 935 ``Homotopy properties of the poset of nontrivial \(p\)-subgroups of a group,''
 936 \emph{Advances in Mathematics} 28 (1978), 101--128.
 937 
 938 \bibitem{Barmak2011}
 939 J. A. Barmak,
 940 ``On Quillen's Theorem A for posets,''
 941 \emph{Journal of Combinatorial Theory, Series A} 118 (2011), 2445--2453.
 942 
 943 \bibitem{BarmakBook2011}
 944 J. A. Barmak,
 945 \emph{Algebraic Topology of Finite Topological Spaces and Applications},
 946 Lecture Notes in Mathematics 2032, Springer, 2011.
 947 
 948 \bibitem{Tancer2016}
 949 M. Tancer,
 950 ``Recognition of collapsible complexes is NP-complete,''
 951 \emph{Discrete \& Computational Geometry} 55 (2016), 21--38.
 952 The appendix discusses undecidability of contractibility for finite simplicial complexes.
 953 
 954 \bibitem{Gaucher2006}
 955 P. Gaucher,
 956 ``T-homotopy and refinement of observation. III. Invariance of the branching and merging homologies,''
 957 \emph{New York Journal of Mathematics} 12 (2006), 319--348.
 958 
 959 \bibitem{Gaucher2005}
 960 P. Gaucher,
 961 ``T-homotopy and refinement of observation. IV. Invariance of the underlying homotopy type,''
 962 arXiv:math/0505331 (2005).
 963 
 964 \end{thebibliography}
 965 
 966 \end{document}