CE0001 matrix_minor_four_code_existsFour 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 StableEvery genuine first-row minor · arbitrary alternating sums · T13 partial
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.
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.
CE0001 matrix_minor_four_code_existsFour 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 StableCE0002 matrix_minor_four_code_output_functionalThe canonical four-component minor-record output is unique.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE0003 matrix_minor_four_code_components_injectiveAn exact nested doubled-Cantor cofactor record uniquely determines all four minor-code components.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE0004 signed_cofactor_minor_record_existsEvery 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 StableCE0005 signed_cofactor_minor_record_projects_minorEvery cofactor record projects an actual complete signed deleted-row/deleted-column matrix minor.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE0006 signed_cofactor_minor_prefix_emptyEvery beta code vacuously describes the genuinely empty signed cofactor-minor prefix.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE0007 signed_cofactor_minor_prefix_extendAppending one genuinely constructed signed minor preserves every previously encoded cofactor record.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE0008 signed_cofactor_minor_prefix_exists_boundedEvery 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 StableCE0009 signed_cofactor_minor_family_existsEvery 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 StableCE000A signed_cofactor_minor_family_entry_existsEach 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 StableCE000B signed_cofactor_minor_family_entry_projects_minorEvery decoded member of the complete first-row cofactor family is a genuine independently encoded signed matrix minor.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE000C signed_alternating_cofactor_term_existsEvery 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 StableCE000D signed_alternating_cofactor_term_functionalBoth components of the signed alternating cofactor product are uniquely determined.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE000E signed_alternating_cofactor_term_evenAt 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 StableCE000F signed_alternating_cofactor_term_oddAt 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 StableCE0010 signed_alternating_cofactor_term_exists_uniqueEvery arbitrary genuinely signed cofactor term has exactly one parity-correct subtraction-free component pair.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE0011 signed_alternating_product_prefix_emptyThe length-zero signed alternating product prefix has no unjustified cofactor terms.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE0012 signed_alternating_product_prefix_extendTwo 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 StableCE0013 signed_alternating_product_prefix_existsEvery 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 StableCE0014 signed_alternating_product_prefix_restrictAn 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 StableCE0015 signed_alternating_product_prefix_exact_termAny 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 StableCE0016 signed_alternating_product_prefix_pointwise_functionalBoth components of every arbitrary-arity signed alternating cofactor term are independent of all beta-recoding witnesses.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE0017 signed_alternating_cofactor_fold_existsEvery 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 StableCE0018 signed_alternating_cofactor_fold_functionalBoth 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 StableCE0019 signed_alternating_cofactor_fold_exists_uniqueEvery arbitrary-length signed row/cofactor pair has exactly one subtraction-free signed alternating Laplace value.
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE001A signed_alternating_cofactor_fold_emptyThe arbitrary signed alternating cofactor fold has the exact empty value (0,0).
Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not StableCE001B signed_matrix_first_row_components_existsEvery 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 StableCE001C signed_first_row_cofactor_fold_existsThe 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 StableCE001D signed_matrix_cofactor_family_and_fold_existsEvery 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 StableND0001 Beta(b,c,i,x)Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.
Conservative definition · notation layer 0PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0ND0012 MatrixAffineSlice(b,c,s,d,u,v,l)A complete beta-coded affine matrix slice whose exact target entry at i equals the source entry at s+d*i.
Conservative definition · notation layer 1PD0009 Even(n)n has an even decomposition.
Conservative definition · notation layer 0PD0010 Odd(n)n has an odd decomposition.
Conservative definition · notation layer 0ND0061 SignedAlternatingCofactorTerm(ap,an,bp,bn,i,p,n)The exact positive/negative natural-pair product with signs exchanged precisely at odd cofactor positions.
Conservative definition · notation layer 1ND0062 SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l)Complete beta-coded positive and negative streams of every exact signed parity-adjusted row/cofactor product.
Conservative definition · notation layer 2PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0PD0015 Sum(b,c,l,z)z is the sum of a beta-coded prefix of length l.
Conservative definition · notation layer 1ND0063 SignedAlternatingCofactorFold(ab,ac,db,dc,eb,ec,fb,fc,l,p,n)The two uniquely determined subtraction-free finite sums of an arbitrary signed alternating Laplace fold.
Conservative definition · notation layer 3ND0064 SignedFirstRowCofactorFold(pb,pc,nb,nc,q,eb,ec,fb,fc,p,n)The exact alternating fold of the genuinely beta-decoded first matrix row against supplied signed cofactor values.
Conservative definition · notation layer 4ND0058 MatrixMinorFourCode(z,up,us,un,ut)One canonical injective doubled-Cantor code for all four signed-minor beta-code parameters.
Conservative definition · notation layer 0PD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0ND0046 MatrixSkipIndex(i,r,s)The unique order-preserving source coordinate that skips one genuinely deleted matrix row or column.
Conservative definition · notation layer 1ND0047 MatrixMinorCell(b,c,w,r,d,i,j,z)The exact beta-decoded source entry after independently skipping the removed row and column.
Conservative definition · notation layer 2ND0048 MatrixMinorPrefix(b,c,w,r,d,u,v,q,l)One complete row-major beta code containing every genuine skipped-row/skipped-column matrix entry.
Conservative definition · notation layer 3ND0049 SignedMatrixMinor(pb,pc,nb,nc,w,r,d,q,up,us,un,ut)Both complete independently beta-coded natural components of a genuine signed square cofactor minor.
Conservative definition · notation layer 4ND0059 SignedMinorRecord(pb,pc,nb,nc,q,j,z)An exactly decoded record containing both beta-coded components of the genuine deleted-row/deleted-column signed minor.
Conservative definition · notation layer 5ND0060 SignedCofactorMinorPrefix(pb,pc,nb,nc,q,b,c,l)A beta-coded prefix whose every bounded entry is an actual complete signed first-row cofactor minor.
Conservative definition · notation layer 6Only 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.