D Conditional occupied-system completion: final checked scope
On this page · Visual guide: One root is not the whole problem · Visual guide: A condition must survive the limit · Visual guide: Finite splitting data are not a density theorem · Visual guide: Read the evidence at its actual scope · Permalink · Source line 2
The current endpoint is PaperX.ConditionalOccupiedSystemCompletion.conditional_occupied_system_completion. 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.
D.1 Two conclusions with separate inputs
On this page · Permalink · Source line 8
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 exists_transported_system_of_inverseLimitClosed 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 TransportedAlong, and has the declared complete target profile.
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.
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
These are actual equivariant presentations. They are not inferred from an unexplained equality of numerical traces. The selected family \(\bigoplus_i\rho_{i,\lambda}^{\oplus m_i}\) has a split equivariant inclusion in the carrier. The finite trace sample uniquely determines the multiplicity vector in the declared constituent packet.
The package 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.
D.2 Why the assembly closes
On this page · Permalink · Source line 26
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.
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.
D.3 Occupancy and inherited support
On this page · Permalink · Source line 31
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.
D.4 Evidence tied to this exact source
On this page · Permalink · Source line 34
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 propext, Classical.choice, and 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.
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.
D.5 A later attempt with a different scope
On this page · Permalink · Source line 39
The retained stronger residual-system attempt reports 19/20 and FAIL_CLAIM111_NOT_PROMOTED, with terminal error 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.