Convergents and best approximation — Exact Proof Explorer

Prepending a genuine quotient matrix reverses the determinant-one orientation.

The reverse determinant orientation has the same actual quotient-matrix transition.

A true Euclidean division transports one signed numerator error exactly.

The opposite signed numerator error transports with the same nonnegative magnitude.

The identity matrix gives the exact two initial signed errors b and a, including zero values.

A quotient prepended to both actual convergents transports both error magnitudes and the alternating determinant.

Every actual determinant-one adjacent pair has a coprime current numerator and denominator, including 0/1.

Substitution along the actual recurrence equations transports the determinant/error invariant without assuming it as part of a convergent certificate.

The invariant's current error is exactly the absolute cross-product error, including the zero terminal value.

A genuine Euclidean quotient transports an exact tail rational value to an exact value of the original fraction.

A genuine first Euclidean quotient applied to the actual identity matrix yields errors r<b and b, including quotient zero and remainder zero.

Actual quotient recurrence transports the derived determinant and decreasing errors while retaining the previous-error bound by the input denominator.

Every actual derived nonempty-prefix invariant forces a positive denominator; this is proved, rather than postulated to make the convergent predicate non-vacuous.

The determinant-one equation is a proved consequence of the actual-prefix invariant, not a field assumed by the computation relation.

Opposite signed errors combine without cancellation after subtracting the previous coefficient vector.

Actual numerator and denominator coordinate equations transport the represented rational error exactly.

The actual absolute error of a signed numerator difference is the nonnegative sum of the two error contributions.

Cancelling the common nonnegative coordinate representatives yields the actual pp signed linear combination.

Cancelling the common nonnegative coordinate representatives yields the actual pn signed linear combination.

Cancelling the common nonnegative coordinate representatives yields the actual np signed linear combination.

Cancelling the common nonnegative coordinate representatives yields the actual nn signed linear combination.

The determinant-one cofactor formula reconstructs every actual signed numerator, not merely positive vectors.

The same cofactor coefficients reconstruct the denominator in the exact determinant-one basis.

Normalizing two actual signed cofactor coefficients gives all four signed coordinate cases constructively.

Every signed candidate numerator and natural denominator have actual integral coordinates in a determinant-one adjacent basis.

Exchanging the two genuine basis columns exchanges their coefficients and preserves the represented integer.

The opposite unimodular orientation gives the same complete four-case signed basis decomposition.

Both determinant orientations represent every signed numerator and every natural denominator with actual integer coefficients.

A positive coefficient makes the nonnegative error contribution at least the current error, including error zero.

A nonnegative combination with denominator below the current denominator has zero current coefficient.

A strictly positive denominator in a difference of two nonnegative columns has a nonzero positive coefficient.

The only small-denominator nonnegative combination is an actual previous-column difference with zero current coefficient.

Every candidate with positive denominator below the current one lies in one of the two opposite-sign coordinate sectors; no sign case is omitted.

Exchanging adjacent vectors exchanges their actual error magnitudes and reverses their signs.

In either subtractive sector, a nonzero current coefficient gives the sharp lower bound for the actual absolute error.

Complete signed-numerator comparison from a genuine unimodular pair and its opposite decreasing errors; these premises still need the actual continued-fraction alignment theorem.

The actual determinant and signed-error invariant implies the full comparison with every smaller positive denominator, including signed candidate numerators and exact terminal error zero.

The derived invariant compares the actual, uniquely determined convergent error with every signed candidate's actual error.

Every natural numerator, including zero, is an actual signed numerator with negative component zero.

The existing G071 beta history has unique actual dividend, divisor, and forward quotient-list coordinates at each index.

An empty actual Euclidean history has divisor zero and the empty quotient list, not a spurious convergent.

A complete G071 history exposes its actual first quotient, strict remainder, tagged tail, and predecessor Euclidean history.

No natural index or remainder is strictly below zero.

Equality transport of the actual history length is ordinary substitution, not an index-membership assumption.

A genuine nonempty quotient list in G071 exposes an actual Euclidean first step and an actual shorter history length.

Conservative existential sharing constructs the exact five-coordinate state without adding a pairing function to HA.

Every actual quotient-list/matrix state has a finite natural code with ordinary pairing witnesses.

The conservatively shared state code determines every actual quotient-list and matrix coordinate uniquely.

Every beta index of the genuine convergent computation has unique decoded quotient-list and matrix entries.

The zero-step actual prefix product is exactly the identity matrix, regardless of its unconsumed quotient tail.

Every nonempty actual prefix computation exposes a tagged first quotient and the exact four matrix recurrence equations.

A nonempty convergent prefix must consume an actual tagged quotient cell; nil cannot be mistaken for an initial convergent.

Equality of actual tagged quotient lists transports the finite computation by ordinary substitution.

Equality transports the length of the actual finite matrix computation without altering its entries or quotient list.

Ordinary simultaneous equality transport preserves the actual four terminal matrix entries of the finite computation.

Ordinary beta-prefix extension preserves every actually decoded matrix coordinate at all retained indices.

An actual encoded identity state constructs the zero-length quotient-prefix product with no transition obligations.

The zero-step matrix prefix has a genuine finite beta certificate for every unconsumed tagged list.

Appending the actual first-quotient matrix step preserves every earlier computed state and every transition under a genuine beta-prefix recoding.

A genuine tagged quotient prepends its exact matrix to any actually computed prefix and constructs a finite certificate of the longer computation.

The actual G071 history and actual matrix prefix consume the same first quotient and tagged tail; both predecessor computations and all recurrence equations are derived, not assumed.

Ordinary HA induction on the actual nonempty quotient-prefix length derives determinant one, both alternating errors, strict decrease, and the denominator bound directly from G071 histories.

HA induction on the actual complete Euclidean history constructs every valid quotient-matrix prefix, including the empty, initial, and full terminal products.

Every actual matrix prefix consumes at most the available number of G071 quotients; out-of-range indices cannot satisfy Convergent.

Every genuine in-range index of a G071 history constructs a convergent with proved positive denominator; zero numerators remain allowed.

The actual prefix computation proves the advertised index belongs to the complete G071 list; it is not merely a tagged pair of positive integers.

Every actual first quotient cell constructs the exact initial matrix [[q,1],[1,0]], including q=0.

The genuine zeroth convergent is q/1 for the actual first quotient q; no positivity condition is imposed on its numerator.

Actual numerator equality transports a convergent while preserving its index, positive denominator, and complete computation certificate.

For every positive G071 fraction below one, the genuine initial convergent is 0/1. This checked theorem explicitly corrects the old planning-only numerator-positivity error.

HA induction proves the complete quotient product represents the input rational exactly, including the empty zero-divisor boundary and the terminal zero error.

Every actual terminal convergent has zero cross-product error; the best-approximation theorem does not exclude this rational endpoint.

The terminal convergent is constructively present and exact for every nonempty complete history, not merely a conditional assertion about a hypothetical endpoint.

Every actual G071 positive rational has an explicitly constructed exact terminal convergent in the same indexed quotient-list relation.

HA induction proves the genuine quotient-prefix matrix is independent of its beta certificate and has unique actual entries for every tagged list and index.

An actual indexed convergent has a unique natural numerator and positive denominator, independently of every auxiliary matrix-history certificate.

Every and only valid history index has a uniquely determined actual convergent; all auxiliary finite certificates are immaterial to its value.

The uniquely determined zeroth convergent is the actual first quotient divided by one; this includes the zero-numerator boundary.

The second matrix column is proved to be the actual previous quotient prefix of the same original list, not an arbitrary auxiliary vector chosen to make the determinant or approximation proof work.

Two actual successive convergents of the same G071 list have determinant ±1; both columns are identified with their genuine indexed computations.

Every actual convergent is reduced, including 0/1 and the exact terminal rational; coprimality follows from the proved determinant, not the definition.

Full G072, strengthened to arbitrary signed numerator representatives: every actual convergent of the G071 quotient list minimizes absolute cross-product error among all smaller positive denominators.

Exact natural-domain G072: actual G071 fraction and actual indexed convergent imply |a*v-b*u|≤|a*t-b*r| for every natural numerator r and every 0<t<v, with no assumed approximation premise.