Mathematics · proofs · software

Follow a written claim

Read side by side

All 12 core papers are here. Find a statement, open its source passage, and follow the available proof, Lean guide, and evidence.

Paper I retains its 108 correspondence records, including 69 labeled covered by that source. Papers II through XII index explicit statement blocks in their current manuscripts. These are reading locations, not new proof reviews or Lean coverage assessments.

Choose a core paper

Try “seed rank”, “automorphy” or a source label. Filters are saved in this page’s address so you can share the result.

1159 records across 12 papers

Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates

108 correspondence records.

The original record keeps its status and scope. A mapped module does not imply that every statement in this paper has been formalized.

Typed operator grammar

Definition · Source status: definition_represented

Link to this record · PSC-I-D-TYPED-GRAMMAR

Finite vertex set, arbitrary arrow set, source/target maps, independent vector spaces and typed arrow maps; relations are finite linear combinations of paths with fixed endpoints. The more general free-algebra relation format is specialized both to homogeneous typed path relations and to all representatives of an actual TwoSidedIdeal.

Written statement · No separate proof block indexed

Read formatted statement

5 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Collapsed one-space realization

Definition · Source status: definition_represented

Link to this record · PSC-I-D-COLLAPSED-REALIZATION

Total space is the finite product, canonically the finite direct sum. Vertex operators are single-after-projection maps and arrows are single-after-arrow-after-projection. Induction on the genuinely source/target-indexed TypedPath proves the actual block-composition action, including the zero-length vertex path.

Written statement · No separate proof block indexed

Read formatted statement

7 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Typed realization and module equivalence

Theorem · Source status: covered

Link to this record · PSC-I-T-TYPED-MODULE-EQUIVALENCE

The grammar algebra is constructed by FreeAlgebra and RingQuot, with complete orthogonal vertex idempotents and exact source/target arrow corners. Collapse is full, faithful and essentially surjective, using actual vertex ranges and their analysis/synthesis equivalence. Action objects are then proved equivalent to ordinary ModuleCat for all unital left modules; the coefficient action is recovered through algebraMap. A separate quotient comparison uses the actual TwoSidedIdeal ring congruence and proves both inverse identities. No category equivalence, split decomposition, path action or module structure is supplied as an assumption.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

6 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Realized operator algebra

Definition · Source status: definition_represented

Link to this record · PSC-I-D-REALIZED-ALGEBRA

The realized algebra is literally the range of the constructed algebra homomorphism into Module.End. It is not a supplied equivalent algebra or an abstract surrogate.

Written statement · No separate proof block indexed

Read formatted statement

5 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Action factorization and hull invariance

Proposition · Source status: covered

Link to this record · PSC-I-P-ACTION-FACTORIZATION

The two actual spans are compared by span induction and range-surjectivity. The cardinal seed ranks are equal via the identity semilinear bijection into the actual image algebra. Arbitrary seed sets and zero modules are included; there is no finite-generation assumption.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

8 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Linear seed system

Definition · Source status: documentary

Link to this record · PSC-I-D-SEED-SYSTEM

Algebraic and continuous packet cases are represented by concrete operator algebras, packet objects and arbitrary seed sets, which include every finite distinguished family after passage to its range. The record is a regime/data definition, not an assertion that one bundled structure covers the optional packet-free and topological regimes. Optional fields are represented in separate structures.

Written statement · No separate proof block indexed

Read formatted statement

15 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Generated hull

Definition · Source status: definition_represented

Link to this record · PSC-I-D-GENERATED-HULL

The scalar span of algebra-orbit vectors is proved equal as a set to the module span. The general topological operator hull is an actual Submodule and its topologicalClosure is used in the topological development.

Written statement · No separate proof block indexed

Read formatted statement

9 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Algebra generation and module generation are distinct

Proposition · Source status: covered

Link to this record · PSC-I-P-ALGEBRA-MODULE-GENERATION

The regular action is multiplication on A. The singleton unit is proved generating by surjectivity of scalar evaluation; the nontrivial regular module then has seedRank exactly one. No assertion about algebra presentations is used as a premise.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

2 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Seed evaluation map

Definition · Source status: definition_represented

Link to this record · PSC-I-D-SEED-EVALUATION

multiSeedMap is the actual Finsupp linear combination map; finite families give the stated finite free module.

Written statement · No separate proof block indexed

Read formatted statement

4 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Finite free presentation

Theorem · Source status: covered

Link to this record · PSC-I-T-FREE-PRESENTATION

Actual range/span equality, quotient equivalence and generation/surjectivity equivalence are present.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

4 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Minimal free-cover characterization

Corollary · Source status: covered

Link to this record · PSC-I-C-MINIMAL-FREE-COVER

seedFinrank_isLeast_free_surjection proves the finite minimum, not an executable basis algorithm.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

4 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

One-seed presentation

Corollary · Source status: covered

Link to this record · PSC-I-C-ONE-SEED-PRESENTATION

oneSeedMap has the stated annihilator kernel and its quotient is the literal cyclic range.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

6 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Two-sided annihilator criterion

Proposition · Source status: covered

Link to this record · PSC-I-P-ANNIHILATOR-TWO-SIDED

vectorAnnihilator is the actual kernel of a↦a•s. Right multiplication closure is equivalent to annihilating Submodule.span A {s}; Ideal.IsTwoSided supplies the standard two-sided-ideal interface. Under singleton generation, the actual ideal equals Module.annihilator A M. Noncommutative order is a*b and (a*b)•s=a•(b•s).

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

4 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Completion of a dense free presentation

Theorem · Source status: covered

Link to this record · PSC-I-T-COMPLETED-PRESENTATION

The actual finite free evaluation A^(Fin r)→X is used, its actual kernel is quotiented, and UniformSpace.comap pulls back the target uniformity to that quotient. Dense range is derived from dense module span. AbstractCompletion.compareEquiv supplies a uniform equivalence, linearity over A is proved by completion density, and uniqueness follows from equality on the dense image. Constant action uniform continuity is inherited through the actual quotient embedding; scalar action on Completion is the usual extension. The local-convexity pullback lemma uses ordered scalars (in particular ℝ, including underlying real spaces for complex spaces); the stronger uniform-module completion proof does not require local convexity.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

21 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Seed rank

Definition · Source status: definition_represented

Link to this record · PSC-I-D-SEED-RANK

The operator hull is the scalar span of actual action values; for an acting algebra this is AS. The cardinal infimum ranges over all densely generating subsets, and existence of a minimum is proved from identity membership and cardinal well ordering. Empty generators and infinite cardinals are included. The direct moduleSeedRank definition uses Dense of the literal acting-ring module span, and a proved equality identifies it with the integer-linear operator-family definition even for a nonfaithful action.

Written statement · No separate proof block indexed

Read formatted statement

10 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Cyclic characterization

Proposition · Source status: covered

Link to this record · PSC-I-P-CYCLIC-CHARACTERIZATION

The nontriviality hypothesis agrees with the current publication.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

1 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Monotonicity under enlargement of the acting algebra

Proposition · Source status: covered

Link to this record · PSC-I-P-ACTING-ALGEBRA-MONOTONICITY

For unital operator algebras, actual family inclusion implies operator-hull inclusion. Closure monotonicity transports a minimum generating subset. This exactly supplies the topological clause, combined with the previously mapped algebraic semilinear rank theorem.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

4 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Quotient monotonicity

Theorem · Source status: covered

Link to this record · PSC-I-T-QUOTIENT-MONOTONICITY

The new theorem starts with the printed arbitrary unital ring homomorphism, additive map, scalar compatibility, continuity, and surjectivity. Span induction maps the actual source module span into the target module span; continuous surjectivity transports density. An attained minimum generating set maps to an image of no larger cardinality. No ring-homomorphism surjectivity or faithfulness is assumed. The direct module-span rank is proved equal to the earlier operator-family rank using integer-linear acting operators. This supplies the exact topological clause alongside the separately accepted algebraic theorem.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

7 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Isomorphism invariance

Corollary · Source status: covered

Link to this record · PSC-I-C-ISOMORPHISM-INVARIANCE

A continuous semilinear module equivalence with continuous inverse preserves the direct module-span cardinal rank, by applying the exact semilinear surjection inequality in both directions. The same-ring case uses identity ring maps. The earlier bidirectional operator-family theorem covers intertwining operator-algebra isomorphisms, and the new rank equality bridges these definitions. This supplies the exact topological clause alongside separately accepted algebraic invariance.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

8 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Short exact sequence bounds

Theorem · Source status: covered

Link to this record · PSC-I-T-EXACT-SEQUENCE-BOUNDS

Actual linear f,g with injectivity, range f=ker g and surjectivity; canonical seedRank=top.spanRank. Minimum generators of N are lifted and combined with images of minimum generators of L. The proof derives generation of M and the cardinal upper bound; the lower bound is surjective monotonicity. No splitting, finite generation or desired bound is assumed.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

3 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Shared direct-sum bounds

Proposition · Source status: covered

Link to this record · PSC-I-P-SHARED-DIRECT-SUM

The actual diagonal A-action on M×N realizes the binary direct sum. Projection surjectivity gives both lower bounds; inclusion of generating sets in the two factors yields cardinal addition for the upper bound.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

3 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Independent direct-sum formula

Theorem · Source status: covered

Link to this record · PSC-I-T-INDEPENDENT-DIRECT-SUM

Actual product-algebra action and the maximum formula are proved.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

1 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Tensor-product bound

Proposition · Source status: covered

Link to this record · PSC-I-P-TENSOR-BOUND

The genuine tensor-product action and cardinal product upper bound are proved.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

2 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Tensor rank is not generally multiplicative

Boundary · Source status: scope_boundary

Link to this record · PSC-I-B-TENSOR-NONEQUALITY

No universal tensor equality is exported. This boundary is not counted as a positive theorem.

Written statement · No separate proof block indexed

Read formatted statement

2 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Scalar-extension monotonicity

Proposition · Source status: covered

Link to this record · PSC-I-P-SCALAR-EXTENSION-MONOTONICITY

The source constructs the natural (K⊗k A)-action on K⊗k M using commuting tensor-factor actions and proves (c⊗a)•(d⊗m)=(c*d)⊗(a•m). Tensor and span induction prove the literal image (1⊗-) of any generating set generates. Minimum-cardinality generation plus cardinality of an image gives the rank inequality.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

5 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Scalar quotient witness

Proposition · Source status: covered

Link to this record · PSC-I-P-SCALAR-QUOTIENT-WITNESS

The character, surjective semilinear map and finite scalar dimension match the printed hypotheses.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

1 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Nakayama lemma

Classical input · Source status: classical_input_integrated

Link to this record · PSC-I-CI-NAKAYAMA

The noncommutative input is integrated at the printed finitely generated left-module scope. For any left ideal I contained in Ring.jacobson R, the actual submodule equality N ⊔ I • top = top implies N = top. No commutativity, Noetherian, semisimplicity, finite length, or two-sidedness of I is required for this lifting theorem. The proof derives the radical lifting result from maximal submodules and the ring-radical action inclusion, rather than assuming the desired conclusion.

Written statement · No separate proof block indexed

Read formatted statement

3 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Generator number is detected modulo the Jacobson radical

Theorem · Source status: covered

Link to this record · PSC-I-T-MODULE-TOP

The complete generating-set/family equivalence and canonical cardinal seedRank equality are proved for arbitrary unital rings and finitely generated left modules using the literal M / (Jac(R) • top), its actual scalar action over R / Jac(R), and an exact quotient-map kernel. Any lifts of a generating quotient family generate upstairs, and both minimum-cardinality inequalities are established. The natural seedFinrank equality is proved as well. No semisimplicity hypothesis is needed. The descriptive semisimple-top sentence is covered by the pinned general IsSemisimpleRing.isSemisimpleModule instance applied to this actual quotient module. This is not an algorithm for computing the radical or finding generators.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

19 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Local algebra formula

Corollary · Source status: covered

Link to this record · PSC-I-C-LOCAL-ALGEBRA-FORMULA

The local formula is proved for noncommutative local rings and finitely generated left modules. From IsLocalRing R the source proves uniqueness of the maximal left ideal, identifies the actual Jacobson radical as maximal, constructs DivisionRing (R / Jac(R)) internally, and proves the canonical seedRank equals the left vector-space Module.rank of the actual radical quotient. The natural finite-rank equality is also proved. No commutative residue-field surrogate or caller-supplied division-ring certificate is used.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

6 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Wedderburn--Artin decomposition

Classical input · Source status: classical_input_integrated

Link to this record · PSC-I-CI-WEDDERBURN-ARTIN

The actual arbitrary-division-ring Wedderburn-Artin existence theorem is now integrated at its semisimple-ring scope. The finite-algebra radical quotient is proved semisimple and its actual decomposition is constructed. These depend on proved pinned Mathlib results, not a custom existence axiom. Compatible finite module decompositions are separately constructed in ProductPresentation and SemisimpleExistence.

Written statement · No separate proof block indexed

Read formatted statement

3 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Regular-module multiplicities

Lemma · Source status: covered

Link to this record · PSC-I-L-REGULAR-MODULE-MULTIPLICITIES

The actual left regular module is explicitly equivalent to its natural columns, then to the displayed finite direct sum of natural-module copies over arbitrary division rings. Coordinate ring homomorphisms define the inflated actions, other factors act by zero, and positive-dimensional natural factors are proved simple. No transpose-as-ring-map or commutative-scalar shortcut is used. Finite products for the inner repeated copies are the canonical finite direct-sum model.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

10 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Semisimple seed-rank formula over arbitrary division rings

Theorem · Source status: covered

Link to this record · PSC-I-T-SEMISIMPLE-SEED-RANK

Actual product matrix ring with left multiplication and natural column modules acted on through the matching factor. Semilinear eM along eR enforces compatibility. DivisionRows proves left generation iff row spanning and m<=r*d; standard rows prove sufficiency. Product assembly, column rearrangement and seed-rank invariance prove the formula. RadicalTop is literally M/(Jac(R) smul top); existence constructs decompositions.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

22 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Algebraically closed multiplicity formula

Corollary · Source status: covered

Link to this record · PSC-I-C-ALGEBRAICALLY-CLOSED-FORMULA

Correct public map uses decomposition of A/J, not A. The supplied algebra equivalence forgets to a ring equivalence, and the module decomposition stays compatible. Specializing the exact radical-top theorem to all D_i=k gives the current statement.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

7 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Full matrix algebra

Corollary · Source status: covered

Link to this record · PSC-I-C-FULL-MATRIX

For every division ring and positive matrix size, the natural module has canonical seed rank one and every nonzero vector generates. The proof uses entries w_i / v_j with the inverse on the correct right side. The positive-size convention of the surrounding natural-simple-module discussion is essential: size zero has seed rank zero. This guard remains explicit in Lean and is tested, not silently discarded.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

4 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Multiplicity obstruction

Corollary · Source status: covered

Link to this record · PSC-I-C-MULTIPLICITY-OBSTRUCTION

For arbitrary division rings and positive block size, the actual shared matrix action on m natural-module copies has canonical rank ceil(m/d). The rectangular-matrix, natural-column-product and finite-direct-sum formulations are connected by actual module equivalences. Zero multiplicity is included. This is not the independent-factor action, whose bound is a maximum across distinct factors.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

6 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Primary decomposition for polynomial modules

Classical input · Source status: classical_input_integrated

Link to this record · PSC-I-CI-PID-PRIMARY-DECOMPOSITION

For an existing polynomial module, multiplication by X constructs its evaluation operator and an actual polynomial-linear equivalence; finite coefficient dimension gives torsion. PID decomposition constructs positive elementary divisors, while actual intrinsic primary submodules are proved equal to ideal primary components. PolynomialMonic proves a bijection between monic irreducibles and nonzero prime ideals via p↦(p), deriving injectivity from monicity and surjectivity from a normalized PID prime generator. It reindexes the internal sum and finite nonzero support to precisely the manuscript index set. intrinsic_primary_finite_power_sum is a literal finite DirectSum of k[X]/(p^e), with positive e, for each specified irreducible p.

Written statement · No separate proof block indexed

Read formatted statement

11 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Single-operator seed rank

Theorem · Source status: covered

Link to this record · PSC-I-T-SINGLE-OPERATOR

The full printed statement is now mapped. The actual power-annihilation submodule is proved equal to the ideal primary component. Its inclusion into V/pV has exact kernel pX_p and is onto from the internally discharged Artinian hypothesis. The induced quotient equivalence is residue-field linear. Every intrinsic multiplicity is identified with every actual presentation fibre. The grouped factors are proved to be the literal X_p, and any positive primary decomposition of X_p has the same intrinsic count. The presentation-free maximum over all monic irreducibles is proved bounded and attained, and equals both natural-valued and cardinal-valued seed rank. No caller-supplied decomposition or seed-count conclusion is needed by the public maximum theorem. These are noncomputable mathematical constructions. The printed proof uses a different route through local-module/Nakayama machinery; that separately listed machinery is not thereby marked complete.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

23 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Invariant-factor count

Corollary · Source status: covered

Link to this record · PSC-I-C-INVARIANT-FACTOR-COUNT

Complete at the displayed conditional scope: an actual polynomial-module equivalence to the finite product of nonconstant factors and their divisibility chain imply least seed number, natural seed rank and cardinal seed rank equal the factor count. The theorem also handles the empty product. Finite products and finite direct sums represent the same finite decomposition. Existence of an ordered invariant-factor presentation is not asserted by this declaration, and is not an additional hypothesis-free claim of the printed conditional corollary.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

5 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Geometric-multiplicity formula

Corollary · Source status: covered

Link to this record · PSC-I-C-ALGEBRAICALLY-CLOSED-SINGLE-OPERATOR

Complete at the finite-dimensional algebraically closed scope inherited from the single-operator theorem. The actual intrinsic multiplicity for X-C(a) is identified with the dimension of the actual eigenspace, without diagonalizability. The canonical natural and cardinal seed ranks equal the maximum over the actual spectrum. Off-spectrum dimensions are zero, the empty-spectrum/zero-space maximum is defined as zero, and the spectral maximum is attained on nonzero spaces. No executable spectral algorithm is claimed.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

14 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Cyclic-matrix criterion

Corollary · Source status: covered

Link to this record · PSC-I-C-CYCLIC-MATRIX

Block 06 closes the exact six-way criterion for a nonzero finite-dimensional operator over an arbitrary field. The final List.TFAE includes actual cyclicity, canonical seed rank one, cyclicity of every nonzero intrinsic primary component, an actual monic positive-degree one-invariant-factor presentation, minpoly=charpoly, and one-dimensional eigenspaces at every spectral value of the literal tensor extension to AlgebraicClosure k. Minimal-polynomial preservation and cyclicity preservation/descent are proved, not supplied as hypotheses. The one-factor presentation has a constructed basis in which the original operator is the standard companion matrix; its factor is proved to be the minimal polynomial. A separate theorem proves that any actual nonconstant invariant-factor chain has exactly one factor iff the operator is cyclic. This is a mathematical existence and equivalence theorem, not an executable normal-form algorithm or a full sorted invariant-factor construction for arbitrary noncyclic operators. The nonzero-space guard is retained in the six-way statement. Legacy conditional wrappers are preserved unchanged for compatibility, but the new public criterion needs no decomposition, multiplicity, polynomial-preservation, spectral, or seed-number certificates.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

32 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Finite packet system

Definition · Source status: definition_represented

Link to this record · PSC-I-D-PACKET-SYSTEM

LinearProjectorFamily encodes the actual finite completeness, idempotence and annihilation laws.

Written statement · No separate proof block indexed

Read formatted statement

3 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Packet support and packet-pure vectors

Definition · Source status: definition_represented

Link to this record · PSC-I-D-PACKET-SUPPORT

packetSupport is exactly {i | P_i x≠0}. PacketPure is Set.Subsingleton of that support, equivalent for finite support to cardinality at most one. packetPure_iff_zero_or_range identifies purity with zero or membership in one actual packet range; a pure family is pointwise this predicate.

Written statement · No separate proof block indexed

Read formatted statement

7 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Finite packet aggregation

Lemma · Source status: covered

Link to this record · PSC-I-L-PACKET-AGGREGATION

Q_j is the actual filtered sum of P_i. Computing P_a Q_j proves the laws. Actual range analysis/synthesis over the literal fibre subtype are inverse, and the finite product/direct-sum equivalence gives the printed conclusion.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

4 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Packet analysis and synthesis

Definition · Source status: definition_represented

Link to this record · PSC-I-D-ANALYSIS-SYNTHESIS

Analysis and synthesis use genuine projector ranges, not unconstrained packet slots.

Written statement · No separate proof block indexed

Read formatted statement

3 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Exact packet-coordinate isomorphism

Theorem · Source status: covered

Link to this record · PSC-I-T-EXACT-PACKET-COORDINATES

Both inverse identities and the linear equivalence are proved.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

3 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Packetwise equality

Corollary · Source status: covered

Link to this record · PSC-I-C-PACKETWISE-EQUALITY

Exact equality iff every projected coordinate agrees.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

1 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Universal mapping property of finite packet coordinates

Corollary · Source status: covered

Link to this record · PSC-I-C-PACKET-UNIVERSAL-PROPERTY

Outgoing extension is the finite sum of f_i after actual rangeRestrict projections. Incoming assembly is actual rangeSynthesis after LinearMap.pi. Packet laws give restrictions/projections and completeness gives uniqueness. These universal properties induce the displayed Hom equivalences.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

11 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Tensor-product packet systems

Theorem · Source status: covered

Link to this record · PSC-I-T-TENSOR-PACKET-SYSTEM

Actual TensorProduct.map projectors satisfy all laws by tensor induction. Tensor products of range inclusions have the tensor products of projections as left inverses; range_map identifies the actual packet range. This proves the canonical embedded interpretation of the printed range equality. Exact coordinates then give the literal DirectSum.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

4 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Dual packet systems

Proposition · Source status: covered

Link to this record · PSC-I-P-DUAL-PACKET-SYSTEM

Actual dualMap means precomposition. Composition reverses indices and orthogonality uses the reversed inequality correctly. Restriction and precomposition with the actual packet projection are inverse, giving the stated packet duals and literal finite DirectSum.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

3 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Finite Banach packet isomorphism

Theorem · Source status: covered

Link to this record · PSC-I-T-BANACH-PACKET-ISOMORPHISM

The actual finite projectors are continuous and explicitly bounded as IsBoundedLinearMap over an arbitrary NormedField, including a trivial valuation. Individual bounds produce one finite uniform bound; analysis has that bound and synthesis has the finite-cardinality bound. Any coordinate norm equivalent to the canonical maximum norm is represented by a linear identification and its literal two-sided norm inequalities. Composition gives bounded actual analysis and synthesis, both inverse identities, and closed packet ranges. No conclusion-shaped hypotheses occur.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

6 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Packet-coordinate condition number

Definition · Source status: definition_represented

Link to this record · PSC-I-D-PACKET-CONDITION-NUMBER

The definition is the product of the ordinary operator norms of the actual bounded analysis and synthesis. The generic bounded additive homomorphism norm is defined as the infimum of nonnegative valid operator bounds; linearity is retained by ofBoundedLinear. Equivalent-norm coordinates have explicit actual-map equalities.

Written statement · No separate proof block indexed

Read formatted statement

7 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Conditioned coordinate transport

Proposition · Source status: covered

Link to this record · PSC-I-P-CONDITIONED-COORDINATES

For nonzero X the identity has norm one. The actual inverse relation S∘A=id and operator norm submultiplicativity give κ≥1. The coordinate operator is literally A∘T∘S, and S∘[T]∘A=T gives the reverse estimate. The final wrapper constructs both bounded actual coordinate maps for every equivalent finite-product norm and proves both inequalities for every bounded linear T over any NormedField.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

7 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Completion preserves a finite packet split

Corollary · Source status: covered

Link to this record · PSC-I-C-COMPLETION-PACKET-SPLIT

Over an arbitrary NormedField, the actual dense-submodule restrictions determine the ambient continuous projector identities by equality on a dense set. Each ambient range equals closure of the corresponding dense-submodule image, and two continuous ambient projector extensions agreeing on the dense submodule coincide. This is stronger than the bounded-input manuscript statement; boundedness of the given ambient projectors is available from the printed premise and is not needed for the density/uniqueness argument.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

5 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Unconditional packet sum space

Definition · Source status: definition_represented

Link to this record · PSC-I-D-UNCONDITIONAL-PACKET-SPACE

The carrier is exactly sequences x_n in the specified closed subspaces for which Summable x holds; mathlib Summable is the finite-subset net (unconditional summation). The norm is exactly sSup of norms of finite sums with coefficients in the closed scalar unit ball. Type synonyms avoid inherited product topology. Finiteness is derived, not assumed. RCLike covers real and complex scalars as stated.

Written statement · No separate proof block indexed

Read formatted statement

5 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Completeness of the unconditional packet sum

Lemma · Source status: covered

Link to this record · PSC-I-L-UNCONDITIONAL-COMPLETENESS

Uniform boundedness on the complete continuous dual is justified by finite-dimensional real absolute summability of each scalar image; the isometric bidual inclusion yields finite multiplier bounds. The signed norm controls each coordinate; coordinate limits stay in closed subspaces. Each fixed finite multiplier estimate passes to the limit, uniformly in the finite set and coefficients. Unweighted tails prove Summable for the limit, and the same uniform estimate gives convergence in the signed norm. Metric completeness is then obtained without a projector hypothesis.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

6 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Countable unconditional packet isomorphism

Theorem · Source status: covered

Link to this record · PSC-I-T-COUNTABLE-UNCONDITIONAL-PACKETS

ofSupBound constructs K as the literal supremum of finite multiplier operator norms from BddAbove. The carriers use Summable sequences in actual projector ranges. Continuous projectors commute with the sum, so annihilation proves both inverse identities. The literal signed norm yields analysis bound K and synthesis bound 1. A proved linear isometry identifies the projector-specific carrier and norm with the general ClosedPackets.Space. Completeness follows either from the general theorem or from the constructed uniform equivalence with Banach X.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

12 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Transfer block

Definition · Source status: definition_represented

Link to this record · PSC-I-D-TRANSFER-BLOCK

Ambient compositions and their genuinely range-restricted packet Hom maps are both encoded.

Written statement · No separate proof block indexed

Read formatted statement

6 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Exact operator reconstruction

Theorem · Source status: covered

Link to this record · PSC-I-T-OPERATOR-RECONSTRUCTION

The existing result is more general: source and target can have different finite packet systems.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

2 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Packet matrix multiplication

Theorem · Source status: covered

Link to this record · PSC-I-T-BLOCK-MULTIPLICATION

The output-first block product is proved for three possibly different modules.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

3 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Packet powers and paths

Corollary · Source status: covered

Link to this record · PSC-I-C-BLOCK-POWERS

The power theorem expands transferBlock(P,P,T^m) using packetPathSum. The independent operatorWord/packetWordSum induction expands every finite list of possibly different operators, with composition order matching rightmost-acts-first temporal order. Each summation is over actual intermediate packet labels.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

2 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Adjoint reversal

Corollary · Source status: covered

Link to this record · PSC-I-C-ADJOINT-REVERSAL

The result is proved for bounded self-adjoint outer maps, more generally than orthogonal packet projectors.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

1 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Tensor-product transfer blocks

Corollary · Source status: covered

Link to this record · PSC-I-C-TENSOR-TRANSFER-BLOCKS

Actual transfer blocks factor by tensor-map composition in exactly the (target,source) order printed. Both sides are actual endomorphisms of X tensor Y; no factorization witness is an input.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

1 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Blockwise intertwining equations

Theorem · Source status: covered

Link to this record · PSC-I-T-BLOCK-INTERTWINING

U is any linear map, not an intertwiner structure. Forward direction inserts middle projector sums; reverse direction reconstructs UT and SU from all equal blocks. Distinct source/target index sets are retained.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

11 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Full block-algebra representation

Theorem · Source status: covered

Link to this record · PSC-I-T-BLOCK-ALGEBRA

Full dependent packet Hom families and their multiplication are identified with the actual endomorphism algebra.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

4 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Propagation of packet support

Corollary · Source status: covered

Link to this record · PSC-I-C-PACKET-SUPPORT-PROPAGATION

The source expands each target coordinate as the finite sum of the actual transfer-block contributions and filters to active sources. This yields the support inclusion; nonzero active sums give equality. The single-active theorem uses activeSources={a} plus nonzero transfer contribution, which is equivalent to at-most-one active source plus kernel avoidance on a target that is active.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

7 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Dimension count

Corollary · Source status: covered

Link to this record · PSC-I-C-DIMENSION-COUNT

The actual End space is linearly equivalent to the heterogeneous packet Hom product. Its finite dimension equals the sum of products of actual packet-range dimensions, and finite distributivity gives the displayed square. Both printed equalities occur in one conjunction.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

2 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Block-diagonal projection and packet commutant

Proposition · Source status: covered

Link to this record · PSC-I-P-BLOCK-DIAGONAL-COMMUTANT

diagonalProjection is the actual K-linear map T↦Σ_i P_i T P_i. The proofs derive idempotence, equivalence of commutation with every projector and off-diagonal block vanishing, equivalence to fixed points of this projection, and equality of its actual linear range to the equality-supported subalgebra.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

5 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Support relation and support space

Definition · Source status: definition_represented

Link to this record · PSC-I-D-SUPPORT-RELATION

OperatorSupported is initially defined via actual restricted packet maps; operatorSupported_iff_ambient proves its exact equivalence to ambient transfer-block vanishing. supportSubmodule is the corresponding actual linear subspace of End(X). Relation dictionary: formal rel(a,b) means manuscript (b,a)∈R, with a source and b target.

Written statement · No separate proof block indexed

Read formatted statement

5 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Support-pattern algebra criterion

Theorem · Source status: covered

Link to this record · PSC-I-T-SUPPORT-PATTERN-ALGEBRA

The two difficult converses use arbitrary maps between the actual nonzero packet ranges. Identity support is equivalent to reflexivity; multiplication closure is equivalent to transitivity. support_mul_closed_iff transfers the block statement to actual ambient operators, and support_pattern_algebra_criterion characterizes existence of a Subalgebra whose carrier is precisely that support space.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

4 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

$*$-closed bounded support patterns

Corollary · Source status: covered

Link to this record · PSC-I-C-SUPPORT-PATTERN-STAR

Supported uses literal continuous transfer blocks and is proved equivalent to the underlying algebraic support predicate. Converse symmetry and transitivity use actual bounded rank-one operators between nonzero ranges. Identity support forces reflexivity. Sufficiency constructs an actual StarSubalgebra. RCLike covers the real and complex Hilbert settings; no finite-dimensional restriction or blanket bounded-block assumption is used.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

3 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Preorder support algebra decomposition

Theorem · Source status: covered

Link to this record · PSC-I-T-PREORDER-ALGEBRA-DECOMPOSITION

The support algebra is constructed from the actual preorder. strictSupportIdeal is an actual TwoSidedIdeal of it, with membership proved equivalent to vanishing within every mutual-order class. Nonzero product blocks force strict paths; finite strict-path height is bounded and attained on nonempty indices. strictSupportIdeal_pow_eq_bot uses Mathlib standard ideal powers, with the span-of-words surrogate bridged by strictIdeal_power_mem. Antisymmetrization supplies the actual quotient partial order; class_maximalStrictSteps proves its height equals the exponent parameter. Grouped class projectors are actual sums of original projectors. The diagonal-class homomorphism is surjective with kernel equal to the strict ideal, and preorderQuotientDirectSumEquiv is the actual quotient by that ideal to the product of End of the literal direct sums of class packet ranges.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

11 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Transfer graph of an algebra-generating family

Definition · Source status: definition_represented

Link to this record · PSC-I-D-TRANSFER-GRAPH

packetGeneratedAlgebra is Algebra.adjoin K (range P.proj ∪ ops), exactly the declared algebra in the manuscript. TransferEdge is witnessed by an actual member of ops with nonzero ambient transfer block. ReachableFrom uses ReflTransGen and hence includes length zero.

Written statement · No separate proof block indexed

Read formatted statement

7 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Reachability support of the generated algebra

Theorem · Source status: covered

Link to this record · PSC-I-T-ALGEBRA-REACHABILITY-SUPPORT

Each projector and declared generator lies in the actual support algebra of ReflTransGen(TransferEdge). Algebra.adjoin_le therefore proves containment of the entire generated algebra. generatedAlgebra_block_zero is the literal ambient P_b A P_a=0 consequence outside reachability.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

6 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Reachability obstruction for generated hulls

Proposition · Source status: covered

Link to this record · PSC-I-P-REACHABILITY-OBSTRUCTION

The actual reachable-support subspace is preserved by every element of the generated algebra. Span of actual algebra orbits yields the hull inclusion for arbitrary seed sets. The source SCC is the actual mutual-reachability quotient, with source status equivalent to no incoming condensation edge. generatedAlgebra_source_obstruction separately assembles the printed final clause: seeds outside that source cannot generate any nonzero vector supported in it. It obtains a nonzero coordinate by packet completeness and applies no_reach_into_source and the unreachable-coordinate obstruction.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

9 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Packet-pure seed rank

Definition · Source status: definition_represented

Link to this record · PSC-I-D-DIRECTED-SEED-RANK

The cardinal infimum is over all actual pure generating subsets, its indexing type is nonempty, and its infimum is attained by well-ordering. Corner compression is e*T on range(e), hence literally e*T*e there. Closure and the identity restriction are proved. A local family retains outside indices as zero maps; local_proj_zero_iff identifies these precisely for nonzero original packets, and zero deletion preserves purity and rank. The corrected zero-or-range wording matches empty-index conventions.

Written statement · No separate proof block indexed

Read formatted statement

11 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Basic packet-pure rank bounds

Proposition · Source status: covered

Link to this record · PSC-I-P-PACKET-PURE-RANK-BOUNDS

The left inequality is direct inclusion of admissible generating sets. The upper inequality chooses attained minimal generating sets under each genuine corner algebra, embeds them into X, and proves their union generates by projector completeness and corner_action_ambient. The union cardinal is bounded by the cardinal sum. This works for arbitrary infinite dimensions and arbitrary cardinal ranks, including zero packets.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

2 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Edge-surjective packet system

Definition · Source status: definition_represented

Link to this record · PSC-I-D-EDGE-SURJECTIVE

The edge is TransferEdge P ops, not a supplied surrogate graph. The witness T belongs to Algebra.adjoin of the projectors and declared operators; restrictBlocks is the literal map from the source range to the target range.

Written statement · No separate proof block indexed

Read formatted statement

1 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Source-component formula for packet-pure seed rank

Theorem · Source status: covered

Link to this record · PSC-I-T-SOURCE-COMPONENT-SEED-RANK

SCC is the quotient by mutual reflexive-transitive reachability. Source is proved equivalent to absence of incoming condensation edges. Finite minimality proves every vertex is reached from a source. Generated-algebra support proves source projection compression. The lower bound removes zero seeds, proves those actually lying in each source generate its corner module, and injects the dependent union of these nonzero seed sets into the original generating set. The upper bound chooses attained local minima; actual surjective blocks propagate range containment along actual paths. No source coverage, compression identity, generating conclusion, or graph certificate is assumed in the final theorem. The theorem in fact does not require nonzero original packets, so it includes the printed hypotheses.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

1 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Packet-propagating system

Definition · Source status: definition_represented

Link to this record · PSC-I-D-PACKET-PROPAGATING

Cyclicity is the existing module Cyclic predicate for the genuine packetCornerAlgebra acting on its actual range. There are no extra local-rank-one certificates supplied.

Written statement · No separate proof block indexed

Read formatted statement

2 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Unweighted source-component count

Corollary · Source status: covered

Link to this record · PSC-I-C-SOURCE-COMPONENT-COUNT

The upper bound chooses a cyclic vector at one actual representative vertex of each source SCC and propagates full packet ranges to every vertex. The lower bound proves every generating set has a nonzero source projection, then uses purity and orthogonality to inject Sources into the chosen pure generating set. Nonzero packet range hypotheses are explicit. The finite cardinal-number form is proved; no finite generation or dimension assumption is introduced.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

2 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Mixed-support seeds can merge source requirements

Boundary · Source status: scope_boundary

Link to this record · PSC-I-B-PACKET-PURE-BOUNDARY

The unrestricted mixed-seed example is consistent with the proved product-algebra formula. The packet-pure rank calculation is not separately formalized.

Written statement · No separate proof block indexed

Read formatted statement

1 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Coordinate transport

Theorem · Source status: covered

Link to this record · PSC-I-T-COORDINATE-TRANSPORT

conjugate constructs the actual family U P_i U⁻¹ and proves all projector identities. conjugate_transferBlock proves the exact displayed equality. packetRangeEquiv restricts U to each actual packet range and yields cardinal dimension equality with explicit universe lifts. support_pattern_invariant proves preservation for every relation. TransferEdge and ReachableFrom are unchanged when the actual generator set is transported by conjugation.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

13 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Packet-compatible operator morphism

Definition · Source status: definition_represented

Link to this record · PSC-I-D-PACKET-MORPHISM

The source and target have actual concrete unital operator subalgebras and nonzero complete orthogonal packet projectors. The linear map, unital algebra map and entirely arbitrary index map are separately retained. Fiber projectors are literal finite sums; no injectivity or surjectivity condition is imposed on the index map.

Written statement · No separate proof block indexed

Read formatted statement

10 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Morphism of seeded systems

Definition · Source status: definition_represented

Link to this record · PSC-I-D-SEED-MORPHISM

The algebraic condition uses the actual target algebra span, with arbitrary seed sets. The continuous variant separately retains Hausdorff topological vector-space structure, actual continuity of every algebra operator and packet projector, and actual continuity of the carrier morphism. Its seed condition is membership in the literal topologicalClosure of AlgebraGeneratedHull. The paper specifies an algebra of continuous operators, not a separate topology on that algebra, and the code states this convention explicitly.

Written statement · No separate proof block indexed

Read formatted statement

6 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Naturality of generated hulls and transfer blocks

Theorem · Source status: covered

Link to this record · PSC-I-T-NATURALITY

Hull naturality is actual Submodule.map equality with the span of image-algebra orbits; target-algebra inclusion is derived. The block formula is the exact double sum over possibly many-to-one fibers, at the level of actual linear maps. Surjective generation is derived from the map of top, then the seeded condition implies generation by the target seeds.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

11 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Category of seeded packet systems

Proposition · Source status: covered

Link to this record · PSC-I-P-SEED-SYSTEM-CATEGORY

Composition explicitly aggregates composite fibers by a finite-sum rearrangement and composes operator intertwiners. Algebraic seed closure is proved using span transport. The continuous variant proves invariance of the actual closed algebraic hull from individual operator continuity, maps the source algebraic hull into the target closed hull, then derives map_closedHull from carrier continuity and closure minimality. Seeded composition applies this proved closure transport; identity seed membership and all category laws are proved. The actual algebraic and topological Category instances therefore cover the full stated category claim.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

11 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Packet exact sequence for an invariant subspace

Theorem · Source status: covered

Link to this record · PSC-I-T-PACKET-EXACT-SEQUENCE

K is an actual invariant submodule. Restriction/quotient projectors are constructed; restricted range equals K intersect X_i. Actual packet inclusion is injective, its range equals the actual quotient-map kernel, and quotient map is onto. First/second quotient isomorphisms use denominator comaps in the correct ambient type. Pointwise coordinate maps intertwine with original inclusion/quotient and form a short exact sequence; exact direct-sum coordinates give the full decomposition.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

12 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Packet descent through an invariant quotient

Theorem · Source status: covered

Link to this record · PSC-I-T-QUOTIENT-PACKET-DESCENT

Actual mapQ uses invariance of K. Quotient representative calculations prove the laws and commuting identity. Zero removal preserves completeness. Quotient surjectivity proves uniqueness of every descended operator, so canonicity is established.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

6 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Restriction and quotient of transfer blocks

Corollary · Source status: covered

Link to this record · PSC-I-C-QUOTIENT-PACKET-DESCENT

Invariance under P_i,T,P_j proves preservation of K and membership in the target packet. Tbar is actual K.mapQ K T hT, and representative calculation proves the quotient-block identity. Lean orientation is the symmetric equality of the printed formula.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

11 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Topological packet exact sequence

Corollary · Source status: covered

Link to this record · PSC-I-C-TOPOLOGICAL-PACKET-EXACT-SEQUENCE

The generic theorem works over any NormedField, including a trivial valuation, with explicit boundedness of the original projectors. Restriction and quotient CLMs are the actual algebraic packet maps. Near-minimal quotient representatives transfer every original bound to the quotient; the norm bound uses the usual infimum-of-bounds norm of the bounded additive projector. Actual packet inclusion and quotient maps are bounded with constant one and retain injectivity, exactness, and surjectivity. Closed K and closed bounded-idempotent ranges make all three terms complete.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

7 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Dense realization theorem

Theorem · Source status: covered

Link to this record · PSC-I-T-DENSE-REALIZATION

For the actual continuous linear intertwiner in the packet-morphism convention, the image of the source algebraic operator hull is contained in the target hull, and continuous surjectivity transports density. The actual finite grouped projector is the sum over the σ-fibre, including empty fibres. Surjectivity and the given intertwining identity prove exact equality of image and target range. No norm or metrizability assumptions occur.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

6 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Quotient topology and completed realization

Theorem · Source status: covered

Link to this record · PSC-I-T-QUOTIENT-TOPOLOGY-COMPLETION

The actual first-isomorphism linear equivalence is continuous both ways using IsQuotientMap, not continuity plus surjectivity alone. The restriction to D uses its actual kernel, definitionally comap(D inclusion,ker Φ); density is exactly Φ(D). The same explicit transported-uniformity quotient completion gives the canonical target equivalence and agrees with Φ on represented classes. No original-domain quotient topology is silently substituted for the printed transported topology.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

15 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Realization functor and preservation profile

Definition · Source status: documentary

Link to this record · PSC-I-D-REALIZATION-FUNCTOR

The profile is represented by actual additive/linear functor and PreservesLimit/PreservesColimit instances, with typed syntax for equational operations. Universal constructions also use explicit structured categories, an induced functor, an underlying comparison isomorphism, and actual initial/terminal preservation. No Boolean profile field is accepted in place of preservation evidence.

Written statement · No separate proof block indexed

Read formatted statement

3 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Equational realization principle

Theorem · Source status: covered

Link to this record · PSC-I-T-REALIZATION-EXPORT

Structural induction on well-typed morphism expressions proves transport of identities, zero, addition, negation, scalar multiplication and composition. The additive-only statement uses the canonical integer enrichment, and no extra scalar-linearity assumption is inserted. Actual limit/colimit diagrams are transported under the matching preservation instance. The conditional universal-construction clause is explicit: a declared profile supplies the structured categories of the universal problem, an induced functor, compatibility with the underlying realization functor, and actual initial/terminal preservation. CategoryUniversal derives the mapped initial/terminal property, equality of the uniquely induced arrows, and the underlying commuting comparison squares. Tensor and completion preservation are legitimate conditional inputs, not falsely inferred from additivity.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

11 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Realization export principle

Proposition · Source status: covered

Link to this record · PSC-I-P-REALIZATION-EXPORT

This is the methodological specialization of record 103 to already established Paper I identities. The formal equations are transported from a proved source equality, not assumed as the desired target equality. The universal-property step uses the explicit structured-category profile of CategoryUniversal. No new analytic/topological/positivity/finiteness/integrality assumption is generated.

Written statement · Written proof

Read formatted statement · Read formatted proof

Read statement and proof side by side

10 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Reserved example slots

Definition · Source status: documentary

Link to this record · PSC-I-ALG-EXAMPLE-SLOTS

Example slots are editorial. Existing examples and algorithm specifications remain outside the 69 proved-record denominator.

Written statement · No separate proof block indexed

Read formatted statement

18 recorded Lean declarations

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets

65 written statement records.

Statement types are taken from the manuscript. Conjectures, definitions, classical inputs, and certificates remain distinct. Lean mappings for individual claims are not assigned by this index.

Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory

139 written statement records.

Statement types are taken from the manuscript. Conjectures, definitions, classical inputs, and certificates remain distinct. Lean mappings for individual claims are not assigned by this index.

Paper IV: Cyclic Analytic Functions, Reciprocal Families, and Spectral Zero Data

85 written statement records.

Statement types are taken from the manuscript. Conjectures, definitions, classical inputs, and certificates remain distinct. Lean mappings for individual claims are not assigned by this index.

Paper V: Polyphase Signal Calculus

103 written statement records.

Statement types are taken from the manuscript. Conjectures, definitions, classical inputs, and certificates remain distinct. Lean mappings for individual claims are not assigned by this index.

Paper VI: Transfer Semigroups: Stochastic, Bayesian, Fractional, and PDE Realizations

164 written statement records.

Statement types are taken from the manuscript. Conjectures, definitions, classical inputs, and certificates remain distinct. Lean mappings for individual claims are not assigned by this index.

Optimal selection for the certified primary block bound

Corollary · Written statement

Link to this record · paper-vi-extended-record-090

Source labels: extended:record:090, extended:cor:optimal_primary_selection

Written statement · Following proof block

Read formatted statement · Read formatted proof

Read statement and proof side by side

Lean mapping for this statement has not been transcribed here.

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Paper VII: Quantum Seed Calculus

140 written statement records.

Statement types are taken from the manuscript. Conjectures, definitions, classical inputs, and certificates remain distinct. Lean mappings for individual claims are not assigned by this index.

Physical compression is not a closure test

Proposition · Written statement

Link to this record · paper-vii-strong-proposition-011

Source labels: strong:proposition:011, strong:prop:physical_compression_trivial

Written statement · Following proof block

Read formatted statement · Read formatted proof

Read statement and proof side by side

Lean mapping for this statement has not been transcribed here.

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Paper VIII: Packet Operator Algorithms, Exact Compilation, and GPU Realization

80 written statement records.

Statement types are taken from the manuscript. Conjectures, definitions, classical inputs, and certificates remain distinct. Lean mappings for individual claims are not assigned by this index.

Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation

79 written statement records.

Statement types are taken from the manuscript. Conjectures, definitions, classical inputs, and certificates remain distinct. Lean mappings for individual claims are not assigned by this index.

All-address differences on the divisor branch

Theorem · Written statement

Link to this record · paper-ix-thm-arith-divisor-base

Source labels: thm:arith-divisor-base, eq:arith-divisor-integral, eq:arith-divisor-bound, eq:arith-divisor-normalized

Written statement · Following proof block

Read formatted statement · Read formatted proof

Read statement and proof side by side

Lean mapping for this statement has not been transcribed here.

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

All-row prime-power transfer

Theorem · Written statement

Link to this record · paper-ix-thm-all-prime-power-transfer

Source labels: thm:all-prime-power-transfer, eq:prime-power-signed-bound, eq:prime-power-original-twist

Written statement · Following proof block

Read formatted statement · Read formatted proof

Read statement and proof side by side

Lean mapping for this statement has not been transcribed here.

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

A first-difference criterion

Lemma · Written statement

Link to this record · paper-ix-lem-newton-exact-isometry-criterion

Source labels: lem:newton-exact-isometry-criterion, eq:newton-isometry-criterion, eq:newton-isometry-conclusion

Written statement · Following proof block

Read formatted statement · Read formatted proof

Read statement and proof side by side

Lean mapping for this statement has not been transcribed here.

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Exact four-address first differences

Theorem · Written statement

Link to this record · paper-ix-thm-rank-four-exact-periods

Source labels: thm:rank-four-exact-periods, eq:rank-four-normalized-isometry, eq:rank-four-original-isometry, eq:rank-four-least-period-final

Written statement · Following proof block

Read formatted statement · Read formatted proof

Read statement and proof side by side

Lean mapping for this statement has not been transcribed here.

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Taylor coefficient bounds and radii

Theorem · Written statement

Link to this record · paper-ix-thm-four-taylor-radii

Source labels: thm:four-taylor-radii, eq:zero-one-exact-taylor-radius, eq:two-exact-taylor-radius

Written statement · Following proof block

Read formatted statement · Read formatted proof

Read statement and proof side by side

Lean mapping for this statement has not been transcribed here.

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Analytic local root graph

Theorem · Written statement

Link to this record · paper-ix-thm-analytic-local-graph

Source labels: thm:analytic-local-graph, eq:analytic-psi, eq:analytic-root-graph, eq:implicit-derivative

Written statement · Following proof block

Read formatted statement · Read formatted proof

Read statement and proof side by side

Lean mapping for this statement has not been transcribed here.

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

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

37 written statement records.

Statement types are taken from the manuscript. Conjectures, definitions, classical inputs, and certificates remain distinct. Lean mappings for individual claims are not assigned by this index.

Paper XI: Packets, Arithmetic Realization, and Conditional Comparison

90 written statement records.

Statement types are taken from the manuscript. Conjectures, definitions, classical inputs, and certificates remain distinct. Lean mappings for individual claims are not assigned by this index.

Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion

69 written statement records.

Statement types are taken from the manuscript. Conjectures, definitions, classical inputs, and certificates remain distinct. Lean mappings for individual claims are not assigned by this index.

Full support gives pointwise automorphy on the realized locus

Corollary · Written statement

Link to this record · paper-xii-cor-full_support_pointwise_automorphy

Source labels: cor:full_support_pointwise_automorphy

Written statement · Following proof block

Read formatted statement · Read formatted proof

Read statement and proof side by side

Lean mapping for this statement has not been transcribed here.

Read paper · Lean coverage · Code · Evidence · Worked examples · Search this paper · Back to filters

Index scope and other works · Glossary · Search the site