Proof audit and repair ledger
Reader card. This is the authoritative dependency and status ledger. Conceptual chapters may summarize a technical engine, but claims of proof, conditionality, or remaining obstruction should be checked here and at the cited theorem location.
This chapter records the status of every nontrivial implication after the external proof critique. A checked item means that the relevant construction and bridge lemma are now written in this book. An open item is not used as an unconditional theorem.
Dependency table
| Step | Input | Output | Status and location |
|---|---|---|---|
| Positive representative | \(f\in C(\Sigma,\mathbb Z)_{T_h}\) | Full diagonal \(P(g)\) with \([P(g)]-[1_N]=x_f\) | Proved in Chapter 1 |
| Individual transport | \(G\)-invariance of \([f]\) | Common-size finite PE bisection-normalizer \(W_i\) | Proved in (1.1)--(1.5), including disjoint source/range supports and diagonal normalization |
| Corner holonomy | \(W_i,W_j\) | Barlak's compressed Bott unitary is \(\Omega_{ij}^\ast\) | Proved by the explicit unitary (A.5) and compression (A.7) |
| PV/transgression comparison | Transfer functions \(h_i\) | \(\partial_h[\Omega_{ij}]=\pm[\kappa_{ij}]\) in the correct coinvariant target | Proved in (A.8)--(A.18): the equivariant Toeplitz triangle is passed through the exact Baum--Connes skeletal functor, (A.9)--(A.11) give the filtered cofiber and \(3\times3\) diagrams, and the admissible lift is constructed in the filtered-cofiber staircase lemma. |
| Removal of the quotient | Minimal \(T_h\) | Barlak target equals actual \(K_1(B_h)\cong\mathbb Z\) | Proved after (A.4) |
| Integer curl vanishing | Minimal \(T_h\), common invariant measure | \(\kappa_{ij}=0\) and hence \([\Omega_{ij}]=0\) for every pair | Proved in Chapter 5 using the comparison theorem from Technical Engine A |
| Coloured corner | Full diagonal \(P\) | Exact transformation groupoid \(Y\rtimes_\psi\mathbb Z\) | Proved in (3.1)--(3.3) |
| Normalizer and orientation | Semilinear symbol \(S_i\) | \(S_i\in N(\Gamma)\) and successor orientation is preserved | Proved by the syndetic coloured-orbit and bounded original-height end argument (3.4)--(3.5), without identifying the two cocycles |
| \(K_1\)-index bridge | Finite PE normalizer | Corner \(K_1\)-vanishing is equivalent to zero GPS index | Proved by the typed PV boundary and corner isomorphism (3.8)--(3.13) |
| Permutation strictification | Pairwise actual \(K_1\)-vanishing and finite-PE bisection normalizers | Simultaneously commuting symbols \(c_i\) | Proved using GPS Proposition 5.11 and Corollary 5.12; arbitrary finite Fourier transports are not covered |
| Fixed-corner phase | Commuting symbols | \(\nu\in Z^2(G,U(D_{\mathrm{lc}}))\) and diagonal strictification iff \([\nu]=0\) | Proved in (4.2)--(4.4) |
| Block-supported phase | \(\Theta_{ih}=0\) | Exact equality of coefficient-one bisections | Proved in Section 4.6 |
| Full-field primary curvature | Arbitrary height--transverse entries | Same vanishing \(K_1\)-class as the block-supported curvature | Proved by the comparison theorem and the homotopy (A.20)--(A.22); this does not remove the diagonal phase |
| General finite-stable phase | Cross-block magnetic entries | Strictification when a fixed-corner class vanishes at an allowed finite stage | Sufficient existential hypothesis in Section 4.5 |
| Choice-independent stable phase | Changes of corner, stabilization, transfer, and representative | A class depending only on \(x_f\) | Not constructed; not claimed |
| Balanced descent | Strict equivariant actual module \(F\) | \(D\)-\(A\) correspondence \(X_F=F\otimes_BA\) | Proved in (B.2)--(B.5); the Weyl multiplier, adjoints, conjugate-space right action, and coefficient order are explicit in (B.7)--(B.8b) |
| Mixed projectivity | Rieffel projection \(e\), finite \(F\) | Range of \(\lambda_F^{(m)}(e)\) is finite projective | Proved in Section B.4 |
| Trace | Canonical Fourier trace | \(\tau(\mathcal E_{T,F})=\tau(E_T)\tau(F)\) | Proved on the finite projection in (B.10)--(B.13) |
Corrections forced by the audit
Fixed corner versus stable invariant
The class \([\nu]\) is well defined after fixing the corner, commuting symbols, coefficient action, and lift convention. The book does not construct comparison maps between the cohomology groups attached to different corners. It therefore does not use the former notation \(\mathfrak m_{\Theta,\mathrm{st}}(x_f)\) as though it were an invariant of \(x_f\).
Actual modules versus virtual classes
For an actual coefficient module \(F\) and an actual Rieffel module \(E_T\), Technical Engine B produces an actual finite projective mixed module. For signed \(f\), arbitrary torus \(K_0\)-classes, or isolated Pfaffian terms obtained by subtraction, the output is a graded difference of finite projective modules. No positivity statement is inferred from a possibly negative trace.
Principal solenoidal tori
Benameur--Mathai's principal-solenoidal theorem proves their magnetic gap-labelling conjecture, which is the upper containment
\[ \tau_\mu(K_0(A_{\Sigma,\Theta})) \subseteq\mathcal G_\Theta(\mu). \]
It does not prove equality of these groups in nonzero magnetic field. The higher-dimensional chapter now states only this containment.
Completion checklist
- The stabilization preserves the prescribed graded class.
- The clopen-flow block sizes and orthogonal complements are explicit.
- The Barlak unitary is compressed to \(\Omega_{ij}^\ast\).
- The enhanced equivariant PV triangle is carried through Barlak's exact skeletal functor; the resulting filtered cofiber and \(3\times3\) diagrams construct the exact-couple morphism and the admissible transfer-function lift without forming an ordinary \(C^*\)-algebra cone of \(1-\alpha_h\).
- The Baum--Connes/PV target and minimality removal of coinvariants are proved.
- The coloured corner, normalizer membership, end-preservation orientation argument, and typed \(K_1\)-index comparison are proved.
- For finite-PE bisection normalizers with vanishing corner \(K_1\)-defects, one GPS retraction corrects all symbol generators simultaneously.
- The phase-scaling path preserves the corner and identifies full-field primary \(K_1\)-curvature with the block-supported class; it is not used to trivialize the diagonal phase.
- Block support kills the diagonal phase by exact bisection equality.
- The three-dimensional all-plane statement assumes a minimal selected height in every cyclic splitting.
- The descent correspondence, compact identity, and product trace formula are proved.
- Actual and virtual outputs are distinguished throughout the theorem.
- The principal-solenoid attribution is corrected.
- Construct comparison maps making the finite-stable phase a genuine invariant of \(x_f\).
- Find dynamical conditions forcing the cross-block phase to vanish.
- Extend the coefficient absorption argument beyond height rank one.
The remaining unchecked items concern extensions beyond the proved block-supported height-one theorem.