Actual divisor sums and Möbius tables — Exact Proof Explorer

Preservation of both actual natural beta prefixes preserves canonical signed values without identifying distinct component representations.

Actual finite-domain lookup plus prefix equality transports a signed value; no table-component equality or unspecified choice is used.

Decode the requested signed value, extend both beta streams at l, and explicitly construct the new packed table preserving exactly its earlier signed entries.

Append at the next index after the inclusive input domain, preserving every existing value through N.

The base table contains an arbitrary prescribed signed value at index zero, with actual beta and packing witnesses.

A genuinely packed signed table has actual finite positive and negative sum traces at every requested prefix length.

A recoded prefix has the same actual signed sum; adding its prescribed next entry constructs the extended fold.

The zero-length inclusive table has its prescribed zero entry and no positive index; this does not define a Möbius value at zero.

An actual value of μ at the next positive index is appended by real beta recoding; every earlier signed value, including the zero convention, is preserved.

Ordinary induction constructs a genuine packed Möbius table for every finite bound, using independently proved positive-input μ totality at each step.

Every positive index in the finite domain has an actual canonical table entry and an independently defined Möbius value.

At a positive in-domain index, the actual table lookup is equivalent to the independently specified μ graph, by constructed lookup and literal value uniqueness.

Whenever index one lies in the table, it contains canonical +1 (code two), while the unrelated zero-index convention stays separate.

All valid Möbius tables have the same signed values through N; their packed codes and arbitrary component representatives need not coincide.

A larger actual Möbius table restricts to every smaller finite bound without changing its zero convention or any positive value.

Index zero is masked to canonical zero for every input table and n, without inspecting or restricting F(0).

A real quotient and a positive divisor justify retaining its actual signed input entry.

A proved nondivisor contributes zero independently of every signed input value.

Constructively decide zero and divisibility, then construct the actual retained lookup or zero code; no quotient or choice oracle is assumed.

The kept and omitted alternatives are constructively exclusive, and actual signed input functionality makes the resulting code unique.

At a witnessed positive divisor, a mask value is genuinely the input value, not a value attached to an unspecified quotient.

Every omitted index is exactly canonical zero, including the explicit d=0 branch for arbitrary F(0).

The genuine singleton zero table is the base mask prefix for any fixed divisibility target.

Append one actually decided divisor-mask value while preserving the whole previous signed prefix.

Ordinary prefix induction constructs every finite divisor mask inside the actual source domain, with explicit beta extensions at each step.

Any two real mask constructions agree on every signed value through l, not necessarily on their beta codes or component representatives.

The same actual mask code restricts to any smaller inclusive prefix for its fixed divisibility target.

The constructed mask retains precisely the canonical input value at every witnessed positive divisor inside its finite domain.

Every actual mask explicitly has zero at index zero and at each nondivisor; the source value there is not constrained.

Mask values depend only on positive input values: zero branches ignore F(0), while kept branches supply the positivity and quotient data needed for actual source equality.

Positive-only equality of arbitrary inputs yields full equality of their actual divisor masks, including the forced zero output at index zero.

For every positive n within the finite source domain, construct a real divisor mask and its S n-entry signed fold.

The canonical divisor-sum result is literally unique despite different mask codes and positive/negative representatives.

Every genuine finite signed arithmetic input has a unique actual divisor sum at every 0<n<=N, with no zero-value restriction or cancellation premise.

Divisor sums here are explicitly positive-input; the zero target is not assigned a spurious finite divisor sum.

At n=1, the real two-entry masked fold is 0+F(1), so its exact value is F(1) regardless of F(0).

Actual divisor sums depend only on positive in-domain input values; input entries at zero can be unrelated signed integers.