Actual finite enumerations · tuple CRT · multiplicativity

Jordan Totients and Primitive Tuples

Construct and count primitive tuples, prove Jordan-totient multiplicativity, and explore exact unit-modulus and prime-power primitivity laws.

95 kernel- and Lean-verified Alpha-closed theorems · 32 conservative definitions · 60 notation dependencies

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

127 items
JT0002 jordan_tuple_equal_symm

Coordinate equality is symmetric without selecting canonical codes.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0003 jordan_tuple_equal_trans

A real decoded middle coordinate witnesses transitivity.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0005 jordan_primitive_tuple_transport

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0007 jordan_tuple_divisor_downward

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0008 jordan_primitive_tuple_modulus_one

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0009 jordan_order_zero_excluded

Jordan is intentionally restricted to positive tuple order.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT000A jordan_modulus_zero_excluded

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT000E jordan_tuple_congruence_symm

Pointwise balanced congruence is symmetric on every finite prefix.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0010 jordan_tuple_all_divisible_empty

Every divisor vacuously divides all entries of an empty tuple.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0011 jordan_tuple_all_divisible_extend

Adjoining an actually decoded divisible entry preserves common divisibility.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0012 jordan_tuple_all_divisible_decidable

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0015 jordan_primitive_tuple_decidable

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0016 jordan_tuple_equal_empty

All actual empty tuples are coordinatewise equal.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0017 jordan_tuple_equal_drop_last

Restrict coordinate equality to the actual predecessor prefix.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0018 jordan_tuple_equal_extend

Extend equal prefixes using two actual equal last entries.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0019 jordan_tuple_equal_decidable

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT001A jordan_tuple_listed_empty

An empty actual outer list contains no representative.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT001B jordan_tuple_listed_lift

An existing list position remains below the successor bound.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT001C jordan_tuple_listed_decidable

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT001D jordan_tuple_scan_empty

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT001E jordan_tuple_prefix_equal

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT001F jordan_tuple_equal_entry

Coordinate equality transports an actual beta entry with unchanged value.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0020 jordan_tuple_bounded_transport

The canonical coordinate bound is independent of tuple encoding.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0021 jordan_tuple_outer_append_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0023 jordan_tuple_scan_skip

Skip precisely when the current admissible tuple is already represented.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0024 jordan_tuple_scan_complete

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0025 jordan_totient_from_complete_scan

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0026 jordan_tuple_scan_append

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0027 jordan_tuple_scan_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0028 jordan_tuple_representatives_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0029 jordan_totient_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT002A jordan_crt_tuple_empty

The empty simultaneous coordinate congruence has no missing witness.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT002B jordan_crt_tuple_extend

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT002C jordan_crt_tuple_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT002D jordan_crt_tuple_left

Every actual output coordinate has the required left congruence.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT002E jordan_crt_tuple_right

Every actual output coordinate has the required right congruence.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT002F jordan_tuple_normalize_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0030 jordan_tuple_congruence_trans

Actual decoded middle entries witness transitivity of coordinate congruence.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0031 jordan_tuple_congruence_divisor

Coordinate congruence descends along actual divisibility of moduli.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0032 jordan_canonical_crt_tuple_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0033 jordan_primitive_crt_tuple_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0034 jordan_rectangle_width_nonzero

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0035 jordan_rectangle_quotient_bound

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0036 jordan_rectangle_flat_bound

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0037 jordan_rectangle_pair_unique

Actual bounded quotient/remainder decomposition uniquely recovers both indices.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0038 jordan_tuple_equal_congruence

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0039 jordan_tuple_bounded_congruence_equal

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT003B jordan_crt_component_recovery

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT003C jordan_canonical_crt_tuple_unique

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT003D jordan_enumeration_actual_value

Every actual decoded enumeration entry is bounded and primitive.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT003E jordan_enumeration_complete

Extract an actual list position for any primitive canonical tuple.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT003F jordan_enumeration_distinct

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0040 jordan_rectangle_crt_append

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0041 jordan_rectangle_crt_successor

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0042 jordan_rectangle_crt_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0043 jordan_rectangle_crt_actual_entry

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0044 jordan_rectangle_crt_pair_value

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0045 jordan_enumeration_reduce_primitive

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0046 jordan_rectangle_crt_distinct

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0047 jordan_rectangle_crt_covers

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0048 jordan_rectangle_crt_enumeration

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0049 jordan_product_enumeration_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT004A jordan_totient_coprime_product

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT004B jordan_totient_multiplicativity_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT004D jordan_enumeration_position_match_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT004E jordan_enumeration_index_map_empty

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT004F jordan_enumeration_index_map_append

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0050 jordan_enumeration_index_map_exists

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0051 jordan_enumeration_index_map_entry

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0052 jordan_enumeration_index_map_bounded_injective

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0053 jordan_enumeration_cardinality_le

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0054 jordan_enumeration_cardinality_unique

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0055 jordan_totient_count_unique

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0056 jordan_totient_multiplicativity_unique_counts

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0058 jordan_zero_tuple_bounded_one

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT0059 jordan_tuples_bounded_one_equal

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT005A jordan_unit_modulus_singleton_enumeration

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT005B jordan_totient_at_one

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
JT005C jordan_totient_at_one_unique

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

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
PD0001 Le(a,b)

Witness-defined non-strict order on natural numbers.

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

Witness-defined strict order on natural numbers.

Conservative definition · notation layer 0
PD0003 Dvd(d,n)

The natural number d divides n.

Conservative definition · notation layer 0
PD0004 Prime(p)

p is nonunit and every factorization of p has a unit factor.

Conservative definition · notation layer 0
PD0005 Coprime(a,b)

Every common divisor of a and b is one.

Conservative definition · notation layer 1
PD0007 DivRem(n,d,q,r)

q and r are a quotient and a strict remainder for n by d.

Conservative definition · notation layer 1
PD0008 ModEq(m,a,b)

Balanced-natural congruence modulo m.

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
PD0014 Product(b,c,l,z)

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

Conservative definition · notation layer 1
PD0019 Repeat(b,c,a,l)

The decoded prefix repeats a for l positions.

Conservative definition · notation layer 1
PD0020 Pow(a,e,z)

z is the relational e-th power of a.

Conservative definition · notation layer 2
ND0001 Beta(b,c,i,x)

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

Conservative definition · notation layer 0
ND0112 UniformBetaPrefixBox(c,T,l,B)

One fixed scale c and positive finite code bound T recode every actual length-l prefix with values below B; completeness is part of the relation.

Conservative definition · notation layer 1
ND0262 BetaPrefixInto(b,c,l,B)

Every actual beta entry below the strict length l has a witnessed value below B. The same generic graph describes canonical polynomial coefficients when B is the modulus; empty prefixes are allowed.

Conservative definition · notation layer 1
ND0263 BetaPrefixEqual(b,c,d,e,l)

Every decoded source entry at i<l also decodes in the target. Actual beta totality and functionality make this extensional prefix equality, not equality of the two code parameters.

Conservative definition · notation layer 1
ND0269 FpCoefficientReduction(p,b,c,d,e,l)

Actual source and target coefficient entries are related by the existing canonical-residue graph at each i<l. Normalization exists even at composite nonzero moduli; field laws require their own prime hypotheses.

Conservative definition · notation layer 2
ND0317 DivisorFactorPair(m,n,d,a,b)

Actual positive a,b divide m,n respectively and d=a*b. Coprimality of m,n, coordinate bounds, gcd recovery, existence and uniqueness are separate hypotheses or proved consequences, not clauses of this relation.

Conservative definition · notation layer 1
ND0375 JordanTotient(k,n,j)

Positive order and modulus with an actual tuple enumeration of length j. No product identity or existence theorem is a clause.

Conservative definition · notation layer 4

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