Actual finite enumerations · tuple CRT · multiplicativity · Constructive arithmetic

Jordan Totients and Primitive Tuples

k>0 ∧ a>0 ∧ b>0 ∧ Coprime(a,b) ⇒ Jₖ(a·b)=Jₖ(a)·Jₖ(b)

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

Open the definition-aware map Read the final theorem See campaign milestone G008

Exact certificate

Fully expanded arithmetic

Inspect all 5335 native tactic lines and 254 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem JT004B and follow only the lemmas and conservative definitions supporting jordan_totient_multiplicativity_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G008 milestone → theorem and definition dependencies.
Major independently established statements: JT0009 jordan_order_zero_excluded · JT000A jordan_modulus_zero_excluded · JT0056 jordan_totient_multiplicativity_unique_counts · JT005C jordan_totient_at_one_unique · JT005F jordan_prime_power_tuple_primitive_characterization · JT0060 jordan_prime_power_tuple_primitivity_invariant · JT004B jordan_totient_multiplicativity_exists.
Independently verified Alpha v35 checked-use theorem family: 95 dependency-curried kernel-checked theorem bodies · 254 proof prerequisites · 32 linked definitions · 60 definition-dependency arrows · 5335 exact tactic lines · first admitted v35 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 359 bundle nodes; SHA-256 9164d35758d1fa15d18ec792a429cbb33fd4c511df5651b9f15d37bececf5ea7.
Exact mathematical boundary: 95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.