Paper X: Universal Residual Seeds and Conditional Occupied-System Completion

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \clearpage
2 \section{Conditional occupied-system completion: final checked scope}
3 \label{sec:conditional-final}
4 The current endpoint is
5 \nolinkurl{PaperX.ConditionalOccupiedSystemCompletion.conditional_occupied_system_completion}.
6 The retained release records 20/20 internal claims checked at their amended and conditional source scopes. This is an assembly theorem with explicit inputs, not unrestricted companion existence or carrier existence.
7 
8 \subsection{Two conclusions with separate inputs}
9 The first conclusion starts with actual completed source members at every coefficient place, admissibility at every positive depth, reduction-natural horizontal transport, and an inverse-limit-closed target profile. The predecessor theorem
10 \nolinkurl{exists_transported_system_of_inverseLimitClosed}
11 constructs a coefficient-indexed target family. Each target member satisfies every declared finite-depth admissibility condition, is related to the source by the exact all-depth relation \nolinkurl{TransportedAlong}, and has the declared complete target profile.
12 
13 The second conclusion starts with a supplied finite compatible family of pairwise nonisomorphic irreducible constituents, a supplied carrier and its explicit constituent-copy decomposition, and a supplied initial subrepresentation with its constituent-copy presentation. Claim 9.1's arithmetic occurrence result supplies a finite set of distinct good primes outside any prescribed finite forbidden set. Its actual Frobenius trace matrix has nonzero determinant. Claim 9.2 then uses this separator to recover the selected multiplicity vector and its summand inside the carrier.
14 
15 Write $\rho_i$ for the supplied constituents, $c_i$ for the carrier multiplicities and $m_i$ for the selected multiplicities, with $m_i\leq c_i$. At a distinguished coefficient place $\lambda$, the input presentations have the form
16 \[
17  V_{\mathrm{car},\lambda}\simeq\bigoplus_i\rho_{i,\lambda}^{\oplus c_i},
18  \qquad U_{0,\lambda}\simeq\bigoplus_i\rho_{i,\lambda}^{\oplus m_i}.
19 \]
20 These are actual equivariant presentations. They are not inferred from an unexplained equality of numerical traces. The selected family
21 $\bigoplus_i\rho_{i,\lambda}^{\oplus m_i}$
22 has a split equivariant inclusion in the carrier. The finite trace sample uniquely determines the multiplicity vector in the declared constituent packet.
23 
24 The package \nolinkurl{CarrierRecoveryAt} also supplies continuity of the selected copies, the common Frobenius characteristic-polynomial product, finite-copy Weil--Deligne and smooth-inertia data, local characteristic and Euler polynomial products, monodromy-kernel dimension and inertia-fixed trace formulas, and genuine semilinear period comparisons with weight-multiplicity sums. The constituent local packets and comparisons are semantic inputs. The conclusion proves their stated finite-copy closure.
25 
26 \subsection{Why the assembly closes}
27 The final proof is a conjunction. The first branch applies the checked inverse-limit-closed horizontal completion theorem to the completed source family. The second branch constructs the finite arithmetic separator and applies the checked compatible-carrier closure theorem. Claim 9.1 constructs its separator independently of the carrier recovery. Claim 9.2 accepts the separator and the compatible-carrier packet. The final source composes these results; it does not use its conclusion to establish either premise.
28 
29 The two branches do not identify the recovered carrier's supplied local Weil or period structures with restrictions of the transported target family. They remain logically distinct outputs. A simultaneous all-place carrier statement is obtained by applying the pointwise result at every place when the corresponding carrier presentations are supplied.
30 
31 \subsection{Occupancy and inherited support}
32 Zero multiplicities are permitted by the formal endpoint. A nonzero occupied conclusion additionally requires the manuscript's declared nonzero-multiplicity premise and nonzero constituents. The module-support/Fitting-ideal alternative is logically separate: its checked support formalization is inherited and is not re-proved by this final module. No unrestricted companion existence, automorphy, carrier existence, or universal $p$-adic Hodge comparison follows from this conditional assembly.
33 
34 \subsection{Evidence tied to this exact source}
35 The saved gate records two warnings-as-errors builds from separate copies of the frozen dependency cache, byte-identical corresponding proof objects, and an axiom audit allowing only \nolinkurl{propext}, \nolinkurl{Classical.choice}, and \nolinkurl{Quot.sound}. False and placeholder controls, a missing profile-closure control, and a missing separator/nonisomorphism-premise control were rejected. An injected custom axiom compiled and was detected by the policy audit. The pinned dependency cache and predecessor releases are trusted inputs of that recorded gate.
36 
37 The October 5 collection audit records a fresh compilation of 30 Paper X project modules, including this endpoint and the arithmetic occurrence closure, using its selected pinned analytic foundation. The present publication migration checks source identity and rebuilds the documents. It performs no new Lean kernel execution.
38 
39 \subsection{A later attempt with a different scope}
40 The retained stronger residual-system attempt reports 19/20 and
41 \nolinkurl{FAIL_CLAIM111_NOT_PROMOTED}, with terminal error
42 \nolinkurl{NO_PINNED_LEAN}. No endpoint was promoted by that attempt. It is not a compiler rejection or retraction of the earlier checked conditional theorem. Its criterion begins with finite nonempty companion levels, while the checked conditional endpoint assumes actual completed members. These are different source obligations.

Back to source controls

Back to Paper X: Universal Residual Seeds and Conditional Occupied-System Completion