Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Exact Integer Division

Abstract

Exact integer division selects the unique canonical integer quotient and has a strictly smaller domain.

Formula projection does not express the dependent archive carriers here. The resolving Lean handles carry the typed statements; this narrative supplies no separate formula.

Theorem 1.1 (Nonzero divisibility gives a unique integer quotient).

Lean statement: D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.exact_quotient_exists_unique

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.exact_quotient_exists_unique (✓ std3). ∎

Source. Repository-derived.

Commentary.

ExactGuard requires a nonzero denominator readout and integer divisibility. Divisibility supplies the witness and nonzero multiplication cancellation proves uniqueness. Selection is defined only with this guard; no truncated division is used.

Theorem 1.2 (The output is the literal integer representative).

Lean statement: D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.exactDivide_literal

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.exactDivide_literal (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the unique integer k satisfying numerator readout equal to k times denominator readout, exactDivide returns representative d k as its underlying rich history. The balanced readout is k.

Theorem 1.3 (The exact guard is equivalent to an integral fraction value).

Lean statement: D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.exact_guard_iff_integer_value

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.exact_guard_iff_integer_value (✓ std3). ∎

Source. Repository-derived.

Commentary.

A legal rich fraction satisfies the exact guard precisely when its rational readout is an integer cast. This also makes the guard invariant under fraction equivalence.

Theorem 1.4 (Retaining the pair and selecting the integer have equal quotient value).

Lean statement: D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.quotient_exactDivide

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.quotient_exactDivide (✓ std3). ∎

Source. Repository-derived.

Commentary.

The original unquotiented fraction pair retains both input histories. Its quotient class equals the class of the integer embedding of the selected canonical output.

Theorem 1.5 (Canonical selection loses generated input history).

Lean statement: D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.exactDivide_loses_product_history

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.exactDivide_loses_product_history (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every dimension and integer n, multiply its canonical balanced history by the canonical history of one, then divide exactly by one. The output is canonical and differs from the input product history: the actual product archive has strictly more events. Only arbitrary-d producer APIs are used.

Theorem 1.6 (The half pair refutes equality of the two domains).

Lean statement: D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.division_domains_equal_refuted

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/SpacetimeArithmetic/IntegerExactDivision.division_domains_equal_refuted (✓ std3). ∎

Source. Repository-derived.

Commentary.

The independent closed claim states that integer exact division and guarded rational division of embedded integers have equal domains at dimension three. The actual half pair has nonzero denominator two; two does not divide one. The theorem proves the negation of that claim, without an unrelated conjunct.

References