Möbius divisor cancellation — Exact Proof Explorer

Cancel one actual nonzero factor in a witnessed square divisor; the quotient is genuinely divisible by p.

A prime divisor of n not dividing d can be adjoined to an actual divisor d: Euclid cancellation constructs the required quotient.

Two constructive divisibility decisions supply the added factor, a genuine quotient, or a fixed prime-square multiple.

Fresh, singly divisible and square-divisible branches are disjoint; cancellation of a nonzero p proves exact output uniqueness.

Adding and removing a fresh factor reverse each other, while the witnessed square-divisible branch is fixed.

Every raw toggle of a positive input by a nonzero p remains positive, including the quotient branch.

Every actual prime toggle of a divisor of n is again a divisor, provided p itself is a prime divisor of n.

Decide positive-divisor membership and construct the raw toggle there, using identity at zero and nondivisors.

The actual positive-divisor toggle and omitted-index identity define one output for every natural index.

For a prime divisor of positive n, toggling preserves positive divisors and reverses the actual graph; omitted indices stay fixed.

Every actual prime-toggle image of the finite interval 0..n remains in that interval, not in an assumed larger universe.

Ordinary finite induction constructs the actual beta-coded prime toggle at every index in the requested window.

Every actual decoded output of the constructed finite map obeys the independent positive-divisor toggle graph.

The actual S n-entry prime toggle is a bounded, injective and constructively surjective permutation, including all fixed omitted indices.

For every actual prime divisor of a positive input, construct the complete finite toggle permutation without supplying its code.

Actual prime toggling negates independently defined Möbius values, including fixed nonsquarefree values, which are proved to be zero.

Every retained entry of an actual Möbius divisor mask is the independent positive-input Möbius value at that divisor.

Every pair of actual Möbius-mask values along the finite prime toggle are signed opposites, including zero, nondivisors and squared-prime multiples.

Swapping the real positive and negative beta components constructs the exact negated signed lookup, with no canonical-component equality assumption.

Pointwise opposite canonical signed entries have opposite actual finite sums, by genuine swapped-component folds and representation independence.

A genuine finite signed sum whose actual permutation pullback is pointwise its opposite is zero; ordinary characteristic-zero cancellation is proved, not assumed.

A genuinely constructed prime-toggle permutation makes the actual zero-masked Möbius sum anti-invariant, hence zero; no cancellation formula is an input.

For every positive nonunit n, construct an actual prime divisor and prove that every genuine Möbius divisor sum is canonical zero.

Construct the actual finite divisor sum before identifying it with zero for every positive nonunit input.

The unit boundary is the genuine two-entry mask fold 0+mu(1)=+1, whose canonical signed code is two.

Full positive-divisor cancellation for independently defined Möbius values: the actual sum is +1 exactly at n=1 and zero at every n>1, with a constructed fold in both directions.

For each positive natural, construct the actual Möbius table, its real finite divisor-sum trace and the exact unit/nonunit result; no table or quotient is supplied.

Full Möbius divisor cancellation holds for any actual signed table with the correct positive values, with F(0) entirely unrestricted; positive-source extensionality transports genuine folds.