Prime-independent system seeds

A compatible system should not be treated as an unrelated collection of \(\lambda\)-adic roots. Its members share algebraic Frobenius polynomials, Hodge–Tate data, determinant information, and local Weil–Deligne packets.

Permalink · Source line 760

The system seed is the fibered object

The fiber product notation states a compatibility requirement. It does not prove that every fiber is nonempty.

Permalink · Source line 776

The theorem above is conditional on the chosen spine and the stated local inverse-limit closure. In the fixed-rank integral representation setting, “closed under inverse limits” means that every compatible family of admissible finite representation classes, after coherent matrix framing and reconstruction, satisfies the full selected local realization relations. It is not merely closedness of an unrelated label space. Weight and packet relations retain their supplied arithmetic meaning; they are parameters of the universal theorem. For a general moduli functor, effectivity requires its own reconstruction hypothesis or the corresponding full meaning of admissible inverse-limit closure.

The complete Lean assembly now includes the common polynomials, good-place sets with finite complements, coefficient-specific prescribed determinants, and every selected weight and packet relation. Determinants are recovered from their actual finite-class determinants. A single common field-valued character on the whole Galois group is not assumed. The returned representations are continuous, and their reductions form the actual compatible branches. Their common polynomial identities hold at every declared good place, hence almost everywhere for each coefficient prime.

This checks Claim 8.2 as the universal conditional source theorem. The previous partial status also demanded proofs that particular intended arithmetic packets satisfy its premises; that stronger application target is not a conclusion of the theorem. The Block 23 source-claim count was therefore sixteen checked and four partial. Concrete Hodge–Tate and Weil–Deligne attachments, torsion interpretations, closure instances, and companion nonemptiness remain obligations of arithmetic applications. Inertial-type labels are not upgraded to full Weil–Deligne data.

Permalink · Source line 837

The eighth formalization block works with actual matrix representations of a fixed group, not only with underlying sets. For a complete separated ring \(R\) and ideal \(I\), compatible maps \(\rho_m:G\to\operatorname{GL}_d(R/I^m)\) reconstruct a unique integral representation for that fixed compatible family. Multiplication and inverses are verified after every reduction. If all finite representations are continuous for the discrete quotient topology, the integral representation is continuous for the ideal-adic topology. This does not assert uniqueness among all possible branches of the allowed forest.

The forest has as its level the actual subtype of representations satisfying the declared finite conditions. Those conditions must be preserved by reduction. Finiteness and nonemptiness at every level give an infinite branch and hence an actual continuous representation. Finiteness of the coefficient quotient alone is not a substitute for finiteness of the allowed representation set for an arbitrary source group. Surjectivity of the reductions is not required.

All coefficients of the characteristic polynomial commute with reduction. Consequently, prescribed integral characteristic polynomials at every precision hold exactly in the reconstructed representation. For a common coefficient field \(E\), local integral polynomials lie in \({\mathcal O}_\lambda[X]\) and are compared with \(P_v\in E[X]\) only after mapping both into the local coefficient field. No field embedding \(E\to{\mathcal O}_\lambda\) is assumed. The allowed-place predicate is explicit and may depend on \(\lambda\). Trivial action on a supplied subgroup is likewise detected at every precision; identifying that subgroup with arithmetic inertia is a separate input.

The eleventh block assembles continuous coefficient-field representations, exact common polynomials and the prescribed local predicate from positive finite depths. Depth-zero finiteness and nonemptiness are derived. Claims 8.2 and 11.1 already assume inverse-limit closure of the selected local conditions; an unconditional closure theorem is not a missing hypothesis of their conditional proofs. Their conditional matrix core is checked. The remaining full arithmetic interpretation must identify the admissible finite objects and the actual local invariants with these data. The coherent-framing obligation is resolved by Block 14 below. An arbitrary local predicate is not being renamed Hodge–Tate or Weil–Deligne compatibility.

Permalink · Source line 865

Over an \(I\)-adically complete separated commutative coefficient ring \(R\), for a fixed finite rank, the formalization now takes finite-level objects to be actual matrix representations modulo conjugation by an invertible matrix. Assume the coefficient quotients \(R/I^k\) are finite. Conjugation commutes with coefficient reduction, and each conjugacy class has finitely many frames over a finite coefficient ring. Thus finite allowed class levels give finite full preimages of allowed matrix representations. Downward admissibility and positive-depth nonemptiness yield an exactly compatible matrix branch and an actual integral representation. More strongly, every prescribed compatible class branch has such representatives, using finite nonempty fibers over that branch. No surjectivity of reductions or lifting of prescribed change-of-basis matrices is assumed. This does not assert uniqueness up to integral conjugacy.

For finitely generated \(I\) with finite \(R/I\), finiteness of \(R/I^k\) is derived. One continuous representative per allowed class suffices, because continuity is proved invariant under conjugation. Characteristic polynomials, determinants and trivial action on a supplied subgroup are likewise actual invariants. The unframed common-spine theorem constructs continuous coefficient-field representations with the prescribed whole polynomials and the explicitly supplied inverse-limit-closed local predicate.

An actual \(\mathbb Z_3\) example applies the class-level completion theorem for the cyclic group of order two and polynomial \(X^2-1\), producing a nonidentity generator. Another checked example has compatible classes represented by \(\operatorname{diag}(1,-1)\) modulo \(3\) and \(\operatorname{diag}(-1,1)\) modulo \(9\): these chosen matrices disagree under reduction, and an actual swap of basis repairs them. Arbitrary independent representatives therefore do not replace the framing argument.

The framing obligation is finished. Identifying the manuscript's arithmetic admissible objects, actual local invariants and finite-level packet reductions with this interface remains separate. An uninterpreted local predicate is not a construction of Hodge–Tate or Weil–Deligne compatibility. The source's local closure hypothesis remains explicit. Block 23 completes the universal conditional implication; these particular arithmetic applications remain unproved.

Permalink · Source line 905

Let \(R\) be an \(I\)-adically complete separated commutative ring with finite coefficient quotients and an injective map into a field \(K\). Fix a finite matrix rank. For finitely many local group maps \(\phi_s:H_s\to G\) and integral template representations \(\tau_s\), fix detecting depths \(d_s\). At precision \(m\) retain matrices \(P_{s,m}\) as part of the admissible object and require

For \(m\ge d_s\) require their determinants to remain nonzero after reduction to \(R/I^{d_s}\). Earlier levels omit that test. Finite occupied augmented levels give a compatible branch of both representations and comparisons. The integral limits satisfy the actual equations and have nonzero determinants, so the comparisons are units over \(K\). A converse supplies all finite nodes from any integral realization with these detectors. Finite-level invertibility and compatible prior choices of comparisons are not assumed.

The unframed positive-depth version also retains continuity and whole common polynomials. Its actual local isomorphisms are derived from the certificates; there is no uninterpreted local-stability predicate for this particular problem. The fixed depths and augmented-level occupancy remain explicit inputs.

The formalization specializes to the actual maps \(G_{\mathbb Q_p}\to G_{\mathbb Q}\) induced by the field embeddings and choices of algebraic closures. A nontrivial continuous quadratic character of \(G_{\mathbb Q}\), constructed from its action on \(i^2=-1\), gives the integral \(2\)-adic actions

at a nonidentity quadratic element. The determinant \(2\) is detected modulo \(4\). The representations are conjugate over \(\mathbb Q_2\) but not integrally conjugate. A separate \(\mathbb Z_3\) example invokes simultaneous completion and reconstructs a comparison which is an integral nonunit and a field unit.

The bound is substantive: for the unipotent actions \(\rho_a(g)=\begin{pmatrix}1&ag\\0&1\end{pmatrix}\), every integral intertwiner with \(\rho_1\) has determinant \(aP_{22}^2\). Taking \(a=\pi^n\) for a nonzero \(\pi\in I\) rules out every fixed detecting depth, even though all the field-valued approximants are isomorphic and their integral limit is trivial. This does not refute Claim 8.2, which already assumes inverse-limit closure of its chosen local conditions.

Exact prescribed local Galois action is stronger than an inertial-type label. The common arithmetic packet interpretation, its coefficient comparisons and the actual Hodge–Tate/Weil–Deligne attachment remain separate. The new theorem does not supply a uniform bound for all intended arithmetic packets. Those arithmetic applications remain unfinished; the universal conditional implication is checked in Block 23.

Permalink · Source line 945

For a finite group \(\Gamma\) whose order is a unit in a commutative local coefficient ring \(R\), any prescribed equivariant residual isomorphism lifts to an integral isomorphism. Lift its matrix to \(A\) and define

Reindexing proves equivariance, and reduction recovers the prescribed matrix. Its determinant is a unit. Complete local coefficients with finite quotients, occupied compatible finite conditions and this residual type therefore give actual integral completion with detector depth one. A fixed continuous map \(G\to\Gamma\) permits pullback to infinite source groups. The finite-level representations must factor through the same map, and the residual type is imposed on their \(\Gamma\)-actions. No uniform determinant bound or augmented certificate occupancy is assumed in this sector.

For a second sector let \(R\) be a DVR with uniformizer \(\pi\), fraction field \(K\) and matrix rank \(n\). If a fixed template \(\tau\) has full \(K\)-linear action span, finite generation and denominator clearing give a fixed \(c\) such that

Normalize a field comparison to an integral \(P\) with a unit entry. The displayed span constructs an integral \(B\) with \(BP=\pi^cI\), so

One \(c\) works for all integral representations in the fixed field-isomorphism class. Jacobson density derives full span from actual irreducibility and a scalar commutant. The formalization states these hypotheses directly and does not assume the DVR fraction field is algebraically closed.

If at every precision there is an integral representation of this rational type satisfying the finite conditions, the derived bound supplies the simultaneous certificates of Block 15 and preserves the type after completion. The integral approximants are not required to be coherent, but their existence is a substantive premise. Arbitrary torsion nodes are not asserted to lift.

Over \(\mathbb Z_3\), the actual average corrects \(A=\left(\begin{smallmatrix}1&1\\0&1\end{smallmatrix}\right)\) to \(P=\left(\begin{smallmatrix}1&-1/2\\0&1\end{smallmatrix}\right)\) for the involutions \(\rho(g)=\left(\begin{smallmatrix}1&1\\0&-1\end{smallmatrix}\right)\) and \(\tau(g)=\operatorname{diag}(1,-1)\). It preserves the residual comparison and has determinant one. Pullback through the quadratic character of the actual \(G_{\mathbb Q}\) gives continuous arithmetic examples. In contrast, the identity and \(\operatorname{diag}(1,\mathrm{sign})\) over \(\mathbb Z/4\) agree modulo two but are not integrally conjugate. Their group order is not a unit. These restricted results do not supply general arithmetic packet attachment, all finite-level existence statements, or cross-coefficient compatibility.

Permalink · Source line 998