Euler's totient product formula — Exact Proof Explorer

Decide common-divisor coprimality from the actual canonical gcd; includes both zero coordinates.

Construct the bit from the actual decidable unit predicate, not from a proposed totient value.

The independently decided unit indicator is literally unique.

The empty unit prefix has no undecided entries.

Restrict a complete prefix of unit bits to its predecessor.

Every decoded bit has the actual common-divisor meaning, regardless of the chosen beta encoding.

Actually append the decided unit bit using beta-prefix extension.

HA induction constructs the complete mask for every modulus and every finite interval.

Unit masks consist of genuine zero/one entries.

All unit masks encode the same bits on their common interval.

Construct an actual finite unit count, with both characteristic and sum traces witnessed.

The count is independent of all beta-mask and sum-trace choices.

The unit count never exceeds the actual interval length.

The auxiliary empty interval count is zero even at modulus zero; this does not assert Phi(0,0).

A successor interval decomposes into its real previous count and the independently decided last unit bit.

The computed predecessor count and next bit construct the real successor count, not a supplied cardinality oracle.

Every integer, including zero, is a unit modulo one in the common-divisor sense.

The independently constructed unit count modulo one equals the actual interval length.

Every positive modulus has a genuinely constructed totient on its canonical residue interval.

The totient value is unique independently of all finite encoding choices.

The totient does not exceed its positive modulus.

Phi keeps the blueprint's positive-domain boundary; auxiliary empty counting does not manufacture Phi(0,0).

Phi(1)=1 because the sole canonical residue zero is coprime to one.

Construct the actual Phi(1,1) count witnesses, including the zero residue.

Total uniquely determined totient on all positive naturals, independently of the still separate Euler product theorem.

Transport the actual characteristic and summation traces along equality of interval lengths.

Changing a proved equal terminal value preserves the real finite count.

Construct the empty-interval zero count for every modulus, without admitting Phi at modulus zero.

Equivalent actual unit predicates have equal independently decided indicator bits.

HA induction proves equality of actual count increments on any two pointwise equivalent finite intervals.

The actual common-divisor unit predicate is periodic modulo n, including the degenerate auxiliary modulus zero.

Each complete period contributes exactly the actual count of one canonical residue interval.

The actual unit count on k complete periods equals k times the actual canonical count.

Equal actual unit predicates throughout a finite prefix have equal witnessed cardinalities.

A proved equal modulus preserves the actual finite count without changing its interval.

A proved equal value preserves the positive-domain actual totient graph.

A proved equal positive modulus preserves both the unit predicate and its canonical residue interval.

Every natural divides itself with the explicit quotient one.

Every divisor of a modulus is coprime to each unit of that modulus.

Units of a product are exactly the simultaneous units of both factors, without a coprime-moduli assumption.

For a prime modulus the independently defined unit predicate is equivalent to nondivisibility.

Adjoining a factor already dividing the modulus leaves the unit predicate unchanged.

Multiplication by a unit preserves common-divisor coprimality at every index.

A multiple of p is never a unit modulo n*p, including j=0.

The positive offsets inside a prime-width block cannot be multiples of its width.

Apart from its first index, each p-wide block has exactly the same unit mask for n and n*p.

When p already divides n, the actual canonical unit count of n*p is p times that of n.

Transport an actually decided characteristic bit along proved equivalence of its predicates.

The one first index and h remaining indices are exactly a block of width p=S h.

Subtraction-free cancellation propagates an exact finite count defect by one actual bit.

A genuine p-wide block loses exactly the unit indicator of j at its first index p*j; all positive offsets are unchanged.

Induction on the number of prime-width blocks counts all removed multiples using the actual unit count of their quotients.

For a new prime factor, the removed multiples account for exactly one old canonical unit count among p periods.

The actual canonical unit count of n*p is (p-1) times that of n when p is prime and coprime to n.

Construct Phi(n*p,p*Phi(n)) when the prime p already divides n, using the actual finite unit-count identity.

Construct Phi(n*p,(p-1)*Phi(n)) for a new prime factor; the predecessor is represented by p=S h.

A prime has exactly p-1 canonical units, with all beta witnesses constructed from Phi(1,1).

Induction proves Phi(p^(e+1))=(p-1)*p^e for the independent unit count, starting with the prime case.

For every positive prime exponent, construct p-1, e-1, the actual preceding power, and its product giving the uniquely defined totient.

Coprimality passes to any genuinely witnessed divisor on the left.

One genuine prime-factor step preserves multiplicativity, separating the new-prime and repeated-prime cases constructively.

Induction on an actual beta-coded prime list proves multiplicativity; no sorting, supplied count, or omitted prime-factor case is assumed.

The actual totient is multiplicative for every pair of positive coprime moduli; the needed finite prime list is constructed, not supplied.

Construct the arithmetic Euler factor from the actual prime and positive exponent, independently of any unit count.

The independently computed Euler factor equals the actual unit count of its prime power.

Predecessor and beta-encoding choices cannot change the computed arithmetic Euler factor.

Every actually decoded support power has its prime, positive exponent and genuine power witnesses at the same index.

The selected prime/exponent beta entries refer to the same actual power, not merely some unrelated factorization witnesses.

Distinct prime entries force their actual prime-power factors to be pairwise coprime; injectivity supplies the needed inequality witnesses.

Actual beta products of pairwise coprime moduli multiply their actual totient counts, including the empty product one.

The empty actual Euler-factor list has no entries or artificial zero-exponent factors.

A prefix retains all actual prime, exponent, factor, and preceding-power witnesses.

Actually append the computed Euler factor while preserving every earlier beta-decoded value and its arithmetic witnesses.

HA induction constructs the full beta-coded list of p^(e-1)*(p-1) from actual positive prime-valuation entries.

The factor and support lists share the very same decoded prime and exponent at each index, so each Euler factor is the actual totient of its power.

The actual Euler-factor product over complete distinct prime-valuation support equals the independently defined unit count of n.

Every genuine complete Euler product computes Phi; this is proved, not stipulated in either definition.

For every positive n construct complete distinct valuation support, every preceding power and Euler factor, and their actual finite product.

Changing the complete support ordering or any beta code cannot change the Euler-product value.

Every actual totient count has a fully constructed complete prime-support Euler product with that exact value.

The independently defined actual unit count and complete prime-support Euler product are equivalent on precisely the positive domain.

At n=1 construct the genuinely empty prime support and empty Euler-factor product one, with every list code explicitly zero.

The Euler product preserves the positive domain: no finite complete-support product is fabricated for zero.

G006: for every positive n construct an actual prime factorization, the actual unit count, and its equal product of p^(Val(p,n)-1)*(p-1) over every distinct prime divisor; n=1 gives the empty product one.