Every genuine first-row minor · arbitrary alternating sums · T13 partial

Complete signed cofactor families and alternating Laplace folds

Twenty-nine independently checked constructive theorems simultaneously encode every genuine signed first-row cofactor minor, prove exact parity-adjusted finite Laplace folds and establish uniqueness in every unrestricted finite dimension.

29 kernel- and Lean-verified Alpha-closed theorems · 19 conservative definitions · 26 notation dependencies

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

48 items
CE0001 matrix_minor_four_code_exists

Four arbitrary natural minor-code components have one exact nested doubled-Cantor record.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE0004 signed_cofactor_minor_record_exists

Every valid first-row column has one exact record containing the entire independently constructed signed cofactor minor.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE0006 signed_cofactor_minor_prefix_empty

Every beta code vacuously describes the genuinely empty signed cofactor-minor prefix.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE0007 signed_cofactor_minor_prefix_extend

Appending one genuinely constructed signed minor preserves every previously encoded cofactor record.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE0008 signed_cofactor_minor_prefix_exists_bounded

Every constructively bounded first-row cofactor prefix has one beta code containing all actual signed minors.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE0009 signed_cofactor_minor_family_exists

Every arbitrary-dimensional signed square matrix has one complete beta-coded family containing ALL exact first-row signed cofactor minors.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE000A signed_cofactor_minor_family_entry_exists

Each valid first-row column extracts its exact actual signed cofactor record from the complete family.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE000C signed_alternating_cofactor_term_exists

Every genuinely signed row/cofactor pair has its exact parity-correct alternating product.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE000E signed_alternating_cofactor_term_even

At every even cofactor column, the signed alternating product has the unswapped exact positive and negative components.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE000F signed_alternating_cofactor_term_odd

At every odd cofactor column, the signed alternating product swaps its exact positive and negative components.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE0012 signed_alternating_product_prefix_extend

Two beta recodings simultaneously append the exact parity-correct signed cofactor product and preserve all earlier terms.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE0013 signed_alternating_product_prefix_exists

Every arbitrary finite signed row and signed cofactor-value stream has complete beta-coded positive and negative alternating-product streams.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE0014 signed_alternating_product_prefix_restrict

An exact signed alternating cofactor prefix of successor length restricts to its genuine earlier prefix.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE0015 signed_alternating_product_prefix_exact_term

Any actual entries decoded from a signed alternating prefix satisfy the exact parity-correct signed cofactor term relation.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE0017 signed_alternating_cofactor_fold_exists

Every arbitrary-length pair of signed beta-coded row/cofactor streams has exact positive and negative alternating Laplace-sum components.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE0018 signed_alternating_cofactor_fold_functional

Both components of an arbitrary finite signed alternating Laplace cofactor fold are independent of every beta-coding and finite-sum witness.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE001B signed_matrix_first_row_components_exists

Every arbitrary-dimensional signed square matrix has two complete beta-coded first-row natural-component streams.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE001C signed_first_row_cofactor_fold_exists

The ACTUAL decoded first row of every signed square matrix has an exact arbitrary-arity alternating fold against any supplied signed cofactor values.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
CE001D signed_matrix_cofactor_family_and_fold_exists

Every arbitrary signed square matrix simultaneously has ALL genuine first-row signed minors and the exact alternating fold of its ACTUAL first row against separately supplied signed cofactor values.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable
ND0001 Beta(b,c,i,x)

Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.

Conservative definition · notation layer 0
PD0002 Lt(a,b)

Witness-defined strict order on natural numbers.

Conservative definition · notation layer 0
PD0009 Even(n)

n has an even decomposition.

Conservative definition · notation layer 0
PD0010 Odd(n)

n has an odd decomposition.

Conservative definition · notation layer 0
PD0013 BetaAt(b,c,i,x)

x is the bounded beta-decoded value at index i.

Conservative definition · notation layer 0
PD0015 Sum(b,c,l,z)

z is the sum of a beta-coded prefix of length l.

Conservative definition · notation layer 1
PD0001 Le(a,b)

Witness-defined non-strict order on natural numbers.

Conservative definition · notation layer 0
ND0046 MatrixSkipIndex(i,r,s)

The unique order-preserving source coordinate that skips one genuinely deleted matrix row or column.

Conservative definition · notation layer 1

Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.

Separate complete second-wave branches: Full T13 proof · Alpha v27.