Jordan Totients and Primitive Tuples — Exact Proof Explorer

Coordinate equality is symmetric without selecting canonical codes.

A real decoded middle coordinate witnesses transitivity.

Divisibility of all coordinates is extensional across tuple encodings.

Primitive means common-divisor one and is independent of beta presentation.

Primitivity descends from a modulus to a genuine divisor of it.

A divisor of a common coordinate divisor is again a common divisor.

Every finite tuple is primitive modulo one, including the zero tuple.

Jordan is intentionally restricted to positive tuple order.

Jordan never counts a purported finite complete residue system modulo zero.

Actual coprime divisor decomposition proves primitivity for the product modulus.

Both primitive projections follow even without coprimality of the moduli.

A genuine common modulus divisor survives balanced congruence, including divisor zero.

Pointwise balanced congruence is symmetric on every finite prefix.

Primitivity is invariant under actual coordinatewise residue transport, not field evaluation.

Every divisor vacuously divides all entries of an empty tuple.

Adjoining an actually decoded divisible entry preserves common divisibility.

Finite induction decides common divisibility from genuine beta entries; no bounded-code oracle.

Decide each actual common-divisor-one implication constructively.

A finite sweep decides the primitive common-divisor condition up to any natural bound.

At positive modulus every possible common divisor lies below S n, giving genuine tuple-predicate decidability.

All actual empty tuples are coordinatewise equal.

Restrict coordinate equality to the actual predecessor prefix.

Extend equal prefixes using two actual equal last entries.

Inductively decide decoded coordinate equality, never equality of beta codes.

An empty actual outer list contains no representative.

An existing list position remains below the successor bound.

Finite list membership is decided by actual outer entries and coordinate equality.

Empty scan has soundness, no duplicate positions, and vacuous code coverage.

An actual one-way beta prefix extension preserves decoded coordinates.

Coordinate equality transports an actual beta entry with unchanged value.

The canonical coordinate bound is independent of tuple encoding.

Construct both outer beta streams after an append; no list witness is assumed.

List membership is a property of the represented coordinate tuple.

Skip precisely when the current admissible tuple is already represented.

A completed duplicate-free scan of a genuine representative box is the independent enumeration graph.

Package a genuinely completed scan as a Jordan cardinality, without assuming totality.

Append an actually absent primitive tuple and prove full soundness, distinctness and prefix coverage.

Construct the duplicate-free finite scan by HA induction and three genuine finite decisions.

Extract an actual finite coordinate-representative box from the existing beta recoding theorem.

Obtain an actual finite tuple cardinality from independently constructed duplicate-free enumeration.

The empty simultaneous coordinate congruence has no missing witness.

Append one genuine scalar CRT solution using an actual beta prefix extension.

Construct simultaneous residue representatives coordinate by coordinate, without any tuple totality premise.

Every actual output coordinate has the required left congruence.

Every actual output coordinate has the required right congruence.

Canonical coordinate reduction works for every nonzero modulus, not just fields.

Actual decoded middle entries witness transitivity of coordinate congruence.

Coordinate congruence descends along actual divisibility of moduli.

Construct an actual tuple bounded by the product modulus with both prescribed residue tuples.

The constructed canonical CRT tuple is primitive collectively, by coprime common-divisor decomposition.

A genuine index below u*v forces the rectangle width to be positive.

An actual bounded row-major index has a row index below u; no division oracle is assumed.

Every actual pair of bounded indices has a row-major index below the literal product.

Actual bounded quotient/remainder decomposition uniquely recovers both indices.

Equal decoded coordinates are congruent at every modulus, including zero.

Actual canonical residues with pointwise congruence are equal as coordinate functions.

The actual universal-property lcm merges both coordinate congruences.

Equal output tuples recover equal canonical input components, not equal raw beta codes.

The actual two-coordinate CRT output is unique below the product modulus.

Every actual decoded enumeration entry is bounded and primitive.

Extract an actual list position for any primitive canonical tuple.

The independent enumeration graph identifies equal coordinate tuples with equal positions.

At the next flat index, construct the actual primitive CRT tuple and append its code and scale to fresh beta lists.

Eliminate the four actual prefix witnesses and append one CRT output in a separate constructive proof scope.

HA induction constructs the genuine rectangular CRT output table at every prefix through u*v, including zero-width rectangles.

Decode an arbitrary actual output entry without identifying distinct beta representations.

The actual rectangular table realizes every prescribed pair of source entries at its unique flat index.

Reduce any primitive tuple to an actual canonical enumeration entry, retaining coordinate congruences and the genuine index.

Equal decoded CRT output tuples recover equal source positions and hence the same flat index.

Every primitive product-modulus tuple reduces to a genuine source pair and is formally equal to its table output.

The constructed table is a duplicate-free exhaustive primitive tuple enumeration of literal length u*v.

Construct an actual product enumeration; no count-uniqueness or multiplicativity premise is used.

Actual finite tuple-count Jordan values multiply at coprime moduli.

The requested constructive G008 coprime multiplicativity endpoint with all three actual counts supplied.

Actual outer beta functionality transports chosen tuple equality to every decoding at the same two positions.

Every actual source position has a bounded target position representing precisely the same coordinate tuple.

The zero-length index map is vacuous, independently of target length.

Append one genuine matched target index and preserve all previous mapped positions by beta extension.

Finite induction constructs an actual beta map for every source prefix, with no finite-choice axiom.

Every actual decoded map value is bounded and matches the represented source tuple.

Equal decoded map indices force coordinate-equal source tuples and hence equal source positions, not equal raw tuple codes.

A genuinely constructed bounded injection implies the source count is at most the target count, including empty lists.

Two complete duplicate-free enumerations of the same primitive coordinate tuples have equal lengths.

The independently defined Jordan relation has a unique count, regardless of all chosen beta encodings.

Any three genuine Jordan counts at coprime moduli obey multiplication, by the independently constructed product enumeration and count uniqueness.

Every decoded coordinate in a tuple bounded by one equals zero.

The literal beta tuple (0,0) has every coordinate below one, at every length.

Any two canonical tuples modulo one represent the same coordinate tuple.

An actual one-position beta list is sound, complete and duplicate-free for primitive tuples modulo one.

For every positive rank k, J_k(1)=1, proved by the explicit singleton enumeration.

Every genuine Jordan count modulo one equals one, independently of its beta encoding.

A prime divisor of the modulus cannot divide every coordinate of a primitive tuple.

Every nonunit common divisor has an actual prime divisor; prime-power support then forces a forbidden common factor p.

Over every positive power of a prime, a tuple is primitive exactly when p does not divide all its coordinates.

Primitivity of an actual beta tuple is invariant under changing the positive exponent of its prime-power modulus.