Integer determinants, rank, and lattice data — Exact Proof Explorer

Six explicit doubled-Cantor constructors code one exact matrix evaluation record with conservatively shared intermediate values.

A beta prefix is unchanged under its own exact code pair.

Actual beta-prefix preservation composes without changing any encoded entry.

An exact preserved beta prefix restricts to every constructively bounded shorter prefix.

Preserved beta entries carry the same actual seven-field evaluation record without expanding nested pairing polynomials.

An arbitrary actual evaluation record can be beta-appended without changing any previous record.

The empty evaluation history has no unsupported matrix records.

Every actual smaller-matrix child remains present when its evaluation DAG is extended.

A genuine local cofactor evaluation transports along preservation of all strictly earlier records.

A finite genuine determinant history is invariant under exact preservation of its beta-coded records.

Append one genuinely evaluated matrix node while preserving every earlier record and every strict-child certificate.

Every existing valid evaluation DAG can be extended by the exact empty determinant (1,0).

The empty minor-value prefix makes no unproved determinant claim.

Reencoding the two already computed cofactor-value streams preserves every actual minor evaluation.

Append one actual smaller determinant to the cofactor streams, preserving all previously certified columns.

Dimension recursion constructs every genuine cofactor determinant in one shared history, by finite prefix induction; the recursion premise is later discharged by HA induction.

If every dimension-q matrix can be genuinely evaluated, every dimension-(q+1) matrix can be appended using all q-dimensional minors and its exact signed Laplace sum.

Unrestricted first-order induction proves genuine determinant evaluation can extend every valid finite history, for every natural dimension.

Every signed beta-coded square matrix has an actual finite strictly well-founded cofactor evaluation, with no bound on dimension and no assumed determinant oracle.

The conservatively shared record determines all seven actual matrix/dimension/value fields uniquely, by six independently checked pairing injections.

A single actual beta entry cannot be interpreted as two different matrix evaluation records.

Every decoded in-range root of a genuine history satisfies its own actual cofactor rule, not merely a different record with the same code.

Every genuine zero-dimensional determinant has exactly the empty product value (1,0), with no exceptional code or trace boundary.

Every nonempty determinant is exactly the parity-correct Laplace fold of genuine recursively evaluated first-row minors; each child inherits an actual valid strict history.

Strict natural order is preserved by a common left summand, by explicit successor transport.

Every in-range row and column has an actual flattened index below the square matrix length.

A genuine row-major index below q squared has row coordinate below q, including the vacuous zero-width boundary.

Every actual first-row minor cell transports across equality of all in-range parent-matrix entries.

An actual finite cofactor-minor code remains the same minor after extensionally equal recoding of its parent matrix.

Two complete codes of the same actual cofactor minor agree at every in-range child entry; division uniqueness aligns the genuine row/column witnesses.

Every pair of corresponding actual signed cofactor minors of pointwise-equal matrices are themselves pointwise equal, regardless of their beta encodings.

The exact signed parity-correct product stream is unchanged when all four finite input streams preserve their actual entries.

An actual signed alternating sum transports to extensionally equal input encodings while preserving its genuine term and partial-sum witnesses.

Every finite signed alternating cofactor sum is functional across pointwise-equal input codes, not just identical beta parameters.

Every actual finite signed matrix is pointwise equal to itself.

Equality of all cells of a nonempty square matrix includes every actual first-row entry.

Genuine determinant functionality in dimension q makes every corresponding evaluated first-row cofactor stream of equal (q+1)-matrices pointwise equal.

Unrestricted HA induction proves exact determinant-component equality for any two actual pointwise-equal signed matrices, across arbitrary finite evaluation histories and arbitrary beta recodings.

Every actual signed matrix has unique recursive cofactor components, independently of the size, layout, or codes of its valid evaluation history.

Every unrestricted-dimensional signed beta-coded square matrix has exactly one positive/negative recursive determinant pair, with both existence and cross-history functionality proved.

A parity-correct fold over every genuinely evaluated actual minor is the determinant: existence supplies a genuine parent history and proved extensional functionality identifies its value.

For every natural dimension, a nonempty determinant is equivalent to its genuine first-row recursive cofactor equation, in both directions and without a supplied-determinant assumption.

The empty square matrix has an explicit valid one-node determinant history with value (1,0).

The exact zero-dimensional determinant equation is an iff, including arbitrary input beta codes and both output components.

The finite bounded-into witness bounds every actual decoded value, by beta uniqueness.

A common multiple contains each explicitly bounded positive natural divisor, with the exact legacy bound convention.

One fixed positive common multiple is divisible by all beta moduli in a finite selector prefix.

Existing constructive CRT recoding yields all finite congruences at a fixed common-multiple scale; no selector-code bound is assumed.

Reducing a genuine CRT recoding modulo a fixed common multiple gives a strictly bounded code with every finite source value preserved.

Unconditionally construct one fixed scale and one positive finite code bound representing every bounded prefix of the requested length.

The empty finite domain has no index, by natural successor nonzeroness.

Finite beta-prefix equality is symmetric because beta decoding is total and functional.

Finite selector value bounds transport across actual pointwise equality of their code prefixes.

A recoded finite selector remains genuinely injective; code equality is not assumed.

Selector injectivity is constructively decidable using the existing witnessed-collision theorem.

Every beta code describes the empty bounded selector prefix.

Deleting the last index preserves a finite selector value bound.

A checked final decoded value extends an existing bounded selector prefix.

Actual finite prefix value bounds are decidable by HA induction and comparison of each decoded entry, without an unbounded-existential decision axiom.

Both in-range coordinates and distinctness survive the complete finite selector recoding.

A genuine finite matrix-selector relation, including every index bound and pairwise distinctness condition, is decidable.

Every actual distinct selector has length at most its matrix-coordinate bound, by constructive finite pigeonhole.

The empty row or column selector is valid even when its ambient dimension is zero.

Decode a genuine row selector, column selector, and parent entry at every flattened selected-matrix index.

Actual selected-matrix cells are functional, by quotient/remainder uniqueness and three genuine beta-decoding uniqueness arguments.

Every code witnesses the actual selected-submatrix prefix of length zero.

Append one actual selected parent entry while preserving every earlier selected entry in the same new beta code.

HA induction constructs arbitrary finite prefixes of actual selected matrices whenever the selected row width is positive.

Every arbitrary selected square submatrix has a complete actual beta code, including dimension zero.

Construct both genuine natural-component streams of an arbitrary signed selected square matrix.

Any two codes of the same actual selected square agree on every finite entry.

Both signed components of any two genuine selected-submatrix encodings are extensionally identical.

Every genuinely selected submatrix has an actual unrestricted-dimensional recursively evaluated signed determinant.

Actual selected-minor determinant values are functional even across different finite submatrix and evaluation-history encodings.

The genuine source cell is unchanged by extensionally equal finite row and column selectors; both selector coordinates are proved in range.

A complete actual selected-submatrix code remains valid under equality-preserving selector recoding.

Both signed component matrices transport across complete finite selector recoding.

Recoding selectors preserves the same actual determinant history and its exact signed output pair.

Nonzeroness of a genuinely evaluated selected determinant is decidable by total evaluation and cross-history functionality.

Actual nonzero minors with fixed selectors are decidable, checking all bounds, distinctness, and a genuine determinant evaluation.

Every genuine nonzero minor survives the complete finite row and column selector recoding with its nonzero value unchanged.

The selected zero-by-zero submatrix has its genuine determinant (1,0), for arbitrary ambient matrices and selector codes.

The order of every actual nonzero minor is bounded by both rectangular dimensions; no extra size premise is built into nonzeroness.

Every rectangular matrix has a genuine nonzero empty minor, including zero-row and zero-column matrices.

An ordinary HA induction exhaustively searches the finite code bound using an already proved actual-candidate decision; no unbounded existential decision is assumed.

An ordinary HA induction exhaustively searches the finite code bound using an already proved actual-candidate decision; no unbounded existential decision is assumed.

Every genuine nonzero minor, whatever its original selector encodings, occurs in the proved finite row/column code search box.

A successful bounded code search supplies actual distinct in-range selectors and a genuine nonzero determinant, not merely a Boolean flag.

Existence of a genuine nonzero minor of any requested order is constructively decidable, with completeness for all unbounded beta selector encodings proved.

A natural number bounded by a successor is either that successor or is bounded by its predecessor.

HA induction with complete finite minor decisions constructs an actual nonzero minor of greatest order within every finite dimension prefix; the empty minor seeds rank zero.

Absence of any actual nonzero minor implies that every genuinely selected evaluated minor has equal signed components, constructively using natural equality decision.

Universal vanishing rules out every witness to a genuine nonzero minor of the same order.

Every arbitrary finite rectangular signed matrix has an actual nonzero rank minor, rank bounded by both dimensions, and every higher minor is proved zero; all searches and determinant evaluations are object-level constructive proofs.

The genuine maximal-nonzero-minor rank is unique: either strict inequality contradicts one actual nonzero witness and the other certificate's universal higher-minor vanishing.

Every finite rectangular signed beta-coded matrix has exactly one genuine rank certificate value, with a nonzero rank minor and universal vanishing of all higher minors.

In particular, every actual minor of order rank plus one vanishes, with no choice of selector or determinant history left implicit.

Every zero-row rectangular matrix has rank zero, with the actual empty determinant supplying its nonzero zero-order minor.

Every zero-column rectangular matrix has rank zero, including the zero-by-zero matrix, without a positivity premise on either dimension.

Actual finite dot products add whenever their decoded multiplicands satisfy the displayed pointwise distributive equation; checked finite-sum additivity supplies the full arbitrary-length result.

Each genuine row-by-column multiplication cell distributes over an actual coded sum of coefficient vectors; the old affine row and column slices are aligned at every coordinate.

Every actual entry of a one-column coded matrix product is the genuine cell at that same row, by bounded column-zero and beta uniqueness, not an arbitrary output witness.

Arbitrary finite one-column matrix multiplication is genuinely additive in the coded right coefficient vector, at every output row.

Five actual pointwise sum relations imply the regrouped sixth relation at every coordinate, with no assumption about canonical beta encodings.

Swapping the actual coefficient vector's positive and negative codes swaps the exact signed product's output components, by the four original coded natural products.

Equal positive and negative coefficient streams construct a genuine coded matrix product with equal output streams, hence integer zero in every row.

The actual signed coded matrix product is componentwise additive in actual componentwise coefficient sums, by all four proved natural matrix-vector products and exact pointwise regrouping.

Equality of signed natural pairs is transitive by genuine cancellative arithmetic, not equality of the chosen positive and negative components.

Component addition represents the sum of integer pairs even when either input has a different noncanonical positive/negative encoding.

Any signed coded vector equals itself as an integer vector, using functionality of the actual positive and negative decoded entries.

Integer-vector equality is genuinely transitive across independently coded, noncanonical intermediate signed entries.

Swapping positive and negative components preserves actual integer-vector equality, independently of the chosen pair representatives.

Equal positive and negative beta streams represent the zero vector at every finite dimension.

An equal-component product represents every actual zero vector, including all noncanonical zero pair encodings.

Actual coded component sums yield integer-vector addition without requiring canonical representatives.

Every two finite signed vectors have a constructively produced coded integer sum, including the empty vector.

Integer-vector addition respects genuine signed-difference equality of both inputs, not merely recoding of equal natural components.

Two actual sums of the same signed vectors are equal as integer vectors, without claiming equality of their beta codes or separate components.

Every finite signed coefficient vector has a fully constructed matrix-vector image as represented integers; the output is an actual coded signed product.

A coefficient witness represents every integer-equal output vector, even when its two component streams differ.

The actual zero coefficient vector represents every zero integer vector through a genuine coded signed matrix product, for arbitrary matrix dimensions.

Swapping the constructed coefficient streams witnesses the negative image, and the image remains correct for arbitrary signed-pair output representations.

Actual componentwise coefficient addition produces the integer sum of both represented matrix images, after explicit signed-equality transport and width-one row-length normalization.

The sum of two represented images has constructively generated coefficient codes whose positive and negative streams are the actual sums of the original coefficient streams; those same codes represent the given integer-sum output.

Column-span membership depends on the represented integer vector, not on its beta codes or its separate positive and negative components.

Every actual zero integer vector belongs to the arbitrary finite integer column span, with the explicit all-zero coefficient code.

Every finite generating matrix has the literal zero vector in its integer column span, without nonemptiness or independence assumptions.

The negative of every column-span vector belongs to the same span, witnessed by swapping its actual positive and negative coefficient streams.

Column spans are closed under every actual integer-negative output, not only under literal swapping of one chosen output code.

Every actual integer sum of two arbitrary column-span vectors lies in the same span, with the constructed finite sums of their actual coefficient streams as witnesses.

Both the sum vector and its span-membership coefficient witnesses are constructively available for every two integer column-span vectors.

Every integer column-span vector has a constructively coded negative in the same span, together with actual negated coefficient witnesses.

Actual signed-integer equality restricts to every smaller finite prefix, without requiring equality of positive or negative components.

Signed-integer vector equality is symmetric at the actual decoded-entry level.

Actual signed-pair multiplication preserves integer equality in both inputs, by two checked multiplication transports and cancellative cross-sum composition.

Swapping both signed pairs preserves their represented integer equality.

Each genuine parity-correct signed cofactor term respects integer equality of its row entry and its evaluated cofactor, in both parity branches.

Arbitrary genuine finite signed sums preserve integer equality of their entries, via an actually constructed common cross-sum code and checked finite-sum additivity.

Every actual alternating-product stream respects integer equality, including all decoded input and output streams and the parity-correct product rule.

The complete actual alternating cofactor fold is independent of every input signed-pair representative, at arbitrary finite length.

Any genuine cofactor cell is the actual source beta value at the uniquely determined skipped row and column.

All four actual cofactor component cells satisfy the parent signed-integer equality at one genuinely shared in-range source position.

Every actual decoded minor output is its genuine cofactor cell at any valid quotient/remainder coordinates, by unique coordinates and beta functionality.

An actual index in a square prefix proves its row width is nonzero; zero-dimensional bounds remain genuinely vacuous.

Genuine cofactor minors of integer-equal matrices are integer-equal, even when every positive/negative code and representative differs.

The smaller-dimension integer-invariance induction hypothesis identifies all genuinely evaluated cofactor streams; the hypothesis is discharged by the final dimension induction.

Actual integer equality of a nonempty square matrix entails equality of its complete genuine first row.

Unrestricted HA dimension induction proves the true signed determinant is invariant under all entrywise integer-equal representations: p+N=P+n, with genuine cofactor evaluations and no assumed induction or quotient-invariance premise.

Every actual in-range rectangular row and column has flattened index below rows times columns, including vacuous zero boundaries.

Every actual selected cell is its genuine source entry for any matching quotient coordinates and selector values; all coordinate and selector equalities are proved.

Actual selected cells of integer-equal rectangular matrices are integer-equal at one proved in-range shared parent index.

Every output decoded from a complete selected-submatrix prefix has its actual source-point certificate, independently of the existential value witness used by the prefix.

Every pair of genuinely selected submatrices from integer-equal rectangular parents has equal represented integer entries, despite arbitrary component recodings.

Every actual selected-minor determinant represents the same integer in any entrywise integer-equal rectangular parent representation.

Nonzeroness of the represented integer is preserved by cross-sum equality, using actual additive cancellation.

Every genuine nonzero minor is transported using the same actual selectors and a newly constructed target determinant; cross-sum invariance proves that its represented value stays nonzero.

Universal actual-minor vanishing is independent of the chosen signed-integer parent representation.

The complete actual rank certificate—including nonzero witness and every higher zero minor—transports across arbitrary entrywise equal integer representations.

The genuine finite rectangular rank value is an invariant of the integer matrix itself, not of any positive/negative beta representatives or determinant histories.

Construct an actual natural absolute difference of every signed pair using constructive natural order.

Oppositely oriented nonnegative gaps can coexist only when both are zero, by actual cancellative natural arithmetic.

The actual natural absolute value of a signed pair is unique, including the zero and opposite-orientation boundaries.

A nonzero represented integer has a nonzero actual absolute difference, in either sign orientation.

A positive actual absolute difference rules out equal signed components, without assuming a canonical representative.

A genuine nonnegative signed gap transports across integer cross-sum equality by additive cancellation.

Natural absolute value is an invariant of the represented integer, not of the chosen positive and negative components.

Every square matrix in every natural dimension has an actual natural absolute determinant obtained from its genuine recursive evaluation.

The actual absolute determinant is unique across all recursive evaluation histories and sign orientations.

The actual absolute determinant is invariant under arbitrary entrywise equal integer matrix representations.

From a positive-dimensional square matrix with an actually nonzero recursive determinant, construct its genuine positive absolute-determinant data; this is data, not an unproved lattice index or covolume theorem.

Nondegenerate square-matrix data contains an actual nonzero full determinant witness, not only a positivity label.

The positive absolute determinant in the nondegenerate square-matrix data is uniquely determined by the actual matrix.

Positive-dimensional absolute-determinant data respects the integer matrix itself, not arbitrary signed beta representatives.

Construct an actual beta-coded identity selector of every natural length from the checked finite range construction.

The actual identity selector is in range and genuinely injective, not merely a supplied permutation label.

Selecting every actual row and column with the identity beta prefix yields exactly the original natural matrix code, by genuine row-major index arithmetic.

The actual identity-selected signed submatrix is the original signed square matrix in both component codes.

A nonzero actual full determinant gives a genuine full-order nonzero minor using proved identity selectors, including the exact zero-dimensional boundary.

A genuinely nonzero full determinant proves the square matrix has full determinantal rank d; identity selectors provide the witness and finite pigeonhole rules out every higher minor.

The explicit positive absolute-determinant matrix data entails genuine full determinantal rank, without claiming a lattice basis, index, or geometric covolume theorem.

Every square matrix has exactly one genuine natural absolute determinant, including zero determinant and dimension zero.

Construct the unique positive absolute-determinant data of every positive-dimensional square matrix with an actual nonzero full determinant.