A conditional system-completion criterion

The preceding results can be assembled without promoting their missing hypotheses to theorems.

Permalink · Source line 1727

The actual order-two representation with generator

satisfies \(A^2=I\) and \(\det(XI-A)=X^2-1\). It has no lift modulo \(8\) with the same characteristic polynomial. Indeed, every lift has entries congruent to \(1,2,2,3\) modulo \(4\). Trace zero then forces its determinant to be \(3\) modulo \(8\), whereas \(X^2-1\) requires determinant \(-1=7\) modulo \(8\). Both the occupied node and the absence of any next-level matrix or representation with the prescribed polynomial are Lean-checked. Other branches of the same unrestricted involution forest survive, so this example does not contradict finite-branch compactness.

Permalink · Source line 1763

Over a domain, for a nonzero \(\pi\in I\), the representations of the additive integer group given by

are all nontrivial and converge pointwise in the ideal-adic topology to the trivial representation. The convergence and the failure of limit preservation for nontriviality are formally checked. Thus not every property of approximating integral representations can be asserted for a limit. This example is not claimed to disprove stability for any particular intended Galois local condition.

Permalink · Source line 1777

The eleventh block established the corresponding conditional matrix criterion. Block 24 now uses the complete common-spine conclusion of Claim 8.2: the returned coefficient-field representations are continuous, have the prescribed common polynomials and coefficient-specific determinants, and satisfy every selected local realization relation under the stated inverse-limit closure hypothesis. All finite reductions belong to the admissible classes.

For each supplied required packet \(p\), let \(A_p\) be its finite-dimensional carrier over a characteristic-zero field \(E_p\), and let \(e_p\) be the actual joint spectral projector for its finite list of split commuting conditions. No order on \(E_p\) is assumed. The source notation \({\operatorname{Tr}}(e_p)>0\) means that the unique natural number \(n_p\) with \({\operatorname{Tr}}(e_p)=(n_p:E_p)\) is positive. The checked projector formula identifies \(n_p\) with the dimension of the actual joint eigenspace.

An admissible realization here includes continuous coefficient-field members and membership of every finite reduction in its designated admissible class. Under the completion hypotheses and these supplied carrier hypotheses, Lean proves

The packet index may be infinite. Each \(x_p\) belongs to its own supplied carrier; no common vector across distinct carriers or embedding of the reconstructed system into those carriers is asserted. Neither an unknown carrier nor positive trace is constructed without the corresponding hypotheses.

This completes Claim 11.2 at its conditional source scope, on the same counting basis used for Claim 8.2 in Block 23. The full arithmetic application premises remain separate. In particular, the criterion does not prove universal occupancy, Hodge–Tate or Weil–Deligne attachment, or the Frobenius recovery clause of Claim 11.1. The latter still depends on the partial Claims 9.1 and 9.2.

Permalink · Source line 1789

For each omitted index \(N\in\mathbb N\), consider one-dimensional rational carriers with the identity operator, requiring eigenvalue \(0\) at \(N\) and eigenvalue \(1\) at every other index. The actual spectral projector has trace \(0\) at \(N\) and trace \(1\) elsewhere. Lean proves that any predetermined finite sample of packet indices can miss an empty required packet: choose \(N\) outside that sample. The family depends on the omitted index. This does not assert that one fixed family passes every finite prefix while failing global occupancy.

Permalink · Source line 1830