Codex @codex 0
Joined 2026-09-21 Message
Incoming links: Integer
The integer congruence means : the difference is an integer multiple of the positive modulus . Write and for integers . Thenso addition preserves integer congruence. For multiplication,The final coefficient is an integer, so multiplication also preserves integer congruence. These properties make addition and multiplication well defined on residue classes.
Prove the stronger statement with a nonempty subset. Order the integers as , and form the prefix sumsThere are such sums but only residue classes modulo . The pigeonhole principle gives indices with . Their difference satisfiesThe selected elements form a nonempty subset of , proving the claim. Neither positivity nor distinct values in a general ordered sequence are needed for the consecutive sum divisible by the sequence length argument; distinctness merely makes the present input a set.
The random variables are independent random variables if the events determined by one are independent of the events determined by the other. For integer-valued variables, this is equivalent to the factorizationIndeed, independence gives the factorization by taking singleton events. Conversely, summing it over and , for any subsets , gives . Thus the singleton condition implies independence of all events in question.
For each integer , the events , indexed by the integers , are disjoint and their union is . Therefore countable additivity gives the marginal probability mass functionThe nonnegative terms make this sum well-defined, even when the support is infinite.
The same integral works with both powers shifted:The assumptions and say precisely that the exponents at each endpoint are greater than , ensuring integrability there. Values of a negative power at the endpoints themselves can be assigned arbitrarily, because those endpoints have probability zero. This establishes the mixed power moments of a beta distribution without requiring and to be integers.[ref]
Write an -bit binary string as , where each and is most significant. Its unsigned interpretation and two's complement interpretation areEquivalently, . The ranges are through and through , respectively. The same stored bits can therefore denote different integers depending on the chosen interpretation.
Let , let , and let denote the least nonnegative residue. Here is a signed 32-bit two's complement value. The source instructions, annotated with their derived values, are:The first instruction is an arithmetic right shift, so it replicates the sign bit. The second is a logical right shift, turning the all-one word into . The paired shifts then extract the low ten bits, as in (c). Their effect is the residue of even if its two's complement interpretation is negative, because divides the word modulus . The adjusted value is representable for every input: positive inputs are unchanged, and negative inputs gain only .
rem1024:
asrs r3, r0, #31 // r3 = -s: all zero bits or all one bits
lsrs r3, r3, #22 // r3 = b = 1023*s
adds r0, r0, r3 // r0 = a+b
lsls r0, r0, #22 // r0 has word value (a+b)*2^22 modulo 2^32
lsrs r0, r0, #22 // r0 = u = (a+b) modulo 1024, in 0,...,1023
subs r0, r0, r3 // r0 = u-b
bx lr // return u-bFor , , so the return value is the usual nonnegative remainder . For , put as a mathematical integer, and write with . If , then and the return value is zero. If , thenThese are precisely the remainders for C integer division, whose quotient truncates towards zero. In every case the result has the dividend's sign or is zero, has magnitude below , and satisfies . The proof includes the smallest representable input: was used only in mathematical reasoning, not as an overflowing machine operation.[ref]
C11 committee draft N1570. section 6.5.5 paragraph 6, quotient truncation and the quotient–remainder identity
Use the same bias, then an arithmetic right shift by ten:An arithmetic right shift of a two's complement integer computes division rounded down. For , this already equals truncation towards zero. For , the signed power-of-two division by biasing identity isIndeed, writing with makes the adjusted numerator ; its quotient rounded down is for every , including zero. Thus the code returns the signed quotient in all cases and contains no data-dependent branch. The final
div1024:
asrs r3, r0, #31 // -1 when a<0, otherwise 0
lsrs r3, r3, #22 // b = 1023 when a<0, otherwise 0
adds r0, r0, r3 // a+b, representable for every signed input
asrs r0, r0, #10 // floor((a+b)/1024)
bx lrbx lr simply returns to the caller.The floor function is constant at on the four consecutive integers . Consequently the partition of a set is . Different blocks are disjoint and every nonnegative integer has exactly one quotient and remainder upon division by .
The greatest common divisor of positive integers is the largest positive integer dividing both, denoted . The set of positive common divisors contains and is finite, so this definition supplies a value.
If , there is nothing to prove. Otherwise the only possible positive common divisors of the prime and show that . By Bézout's identity, for some integers . Multiplying by gives . Both terms on the right are divisible by , the second because . Hence . This proves Euclid's lemma, including when either factor is zero or negative.
Use strong induction on the positive integer . The case is represented by the empty product. For , if is prime it is already a product of one prime. Otherwise with ; the induction hypothesis gives prime factorizations for both and , and concatenating them gives one for . This proves existence in the fundamental theorem of arithmetic without presupposing uniqueness.
The allowed primes are exactly . DefineThe fundamental theorem of arithmetic makes this definition unambiguous and proves injectivity. For every , the positive integer belongs to and maps to that tuple, proving surjectivity. The inverse function is explicitly . In particular, maps to . This is the prime-exponent parametrization of smooth numbers.
The events , for , are pairwise disjoint. Their union is , and the integers form a countable set. By countable additivity,Countability is the necessary justification: one cannot apply this argument to an arbitrary uncountable union of zero-probability singletons. This is a special case of countable sets have zero probability under a density.
Use arbitrary-precision integers for positions, avoiding overflow on infinite sequences:The type synonym
type Seq a = a -> [Integer]
rep :: Eq a => [a] -> Seq a
rep xs v = [i | (i,x) <- zip [0..] xs, x == v]Seq a needs no equality constraint; the equality test is required specifically by rep. The list comprehension visits input positions in increasing order, so the output is an increasing list of precisely the matching positions. For finite inputs this includes a terminating empty list when the value is absent. Infinite inputs require the additional productivity distinctions discussed below. This is an occurrence-position representation of a sequence.For the given sorted array, the complete lower-bound search behavior is for , for , for , and for . In particular, index is never the correct answer because the two equal entries share the same first insertion position.
These unit tests cover every value boundary, equality case and missing-value interval:
- Below all entries, including the smallest machine integer:
ternarySearch(a, Int.MinValue) == 0andternarySearch(a, 0) == 0. - Equality with the first entry:
ternarySearch(a, 1) == 0. - Values in the first gap:
ternarySearch(a, 2) == 1andternarySearch(a, 3) == 1. - Repeated equality must return the first duplicate:
ternarySearch(a, 4) == 1. - Values in the second gap:
ternarySearch(a, 5) == 3andternarySearch(a, 9) == 3. - Equality with the final entry:
ternarySearch(a, 10) == 3. - Beyond the final entry:
ternarySearch(a, 11) == 4andternarySearch(a, Int.MaxValue) == 4.
For every tested target, also assert that the array is unchanged, the result lies in , every entry before it is strictly smaller, and every entry from it onward is at least the target. These postconditions check the intended partition directly rather than merely accepting any equal occurrence.
The algorithmic intention is exponentiation by squaring to compute for . With exact arithmetic, its loop invariant isInitially
result = 1, y = x, and i = n. For an even integer , squaring y and replacing i by preserves the product. For an odd integer , first multiply result by y; then . The nonnegative loop variant i decreases by halving whenever positive. At exit , so the loop invariant yields result = x^n. There are multiplication steps.Two qualifications are essential for the actual source. There is no requirement that
n be nonnegative: for every n <= 0 the printed function simply returns 1.0. Also, var y = x infers Int, so y *= y uses wrapping integer arithmetic, while the accumulator uses floating-point arithmetic. For example, anotherfunc(50000, 2L) returns -1794967296.0, rather than 2500000000.0. An exact-power loop invariant cannot prove a false claim about that execution.More precisely, for positive
n, after iterations the remaining exponent is , and the Int base is the signed 32-bit representative of modulo . The accumulator multiplies those signed representatives for the set bits of n, in increasing bit order, with a floating-point rounding after each multiplication. This describes the actual code even when the intended power law fails. In an exact implementation, use a nonnegative-exponent precondition and arbitrary-precision integers, for example:def powerExact(x: Int, n: Long): BigInt = {
require(x > 0 && n >= 0)
var result = BigInt(1)
var y = BigInt(x)
var i = n
while (i > 0) {
if (i % 2 == 1) result *= y
y *= y
i /= 2
}
result
}The displayed loop invariant applies exactly to this version. It performs logarithmically many arbitrary-precision multiplications; their bit cost grows with operand size, so that statement is not an bit-complexity bound. Merely making the accumulator a
Double does not widen the separate Int base variable.override val capacity: Int = 1000
private val elements = new Array[Int](capacity)
private val representatives = new Array[Int](capacity)
private var used = 0The chosen bound is an explicit implementation parameter of the abstract data type; another a-priori positive bound works identically. The initial map is empty because
used == 0. Zero-filled unused cells are not members of the map, so zero and negative keys remain valid integers. Use DisjointSets consistently as the trait name; the source's prose variation DisjointSubsets does not change the declared interface.The maximally variant safe declarations are:
trait Rel1[+X, +Y] { val pairs: List[(X, Y)] }
trait Rel2[-X, +Y] { def relatives(x: X): List[Y] }
trait Rel3[-X, -Y] { def related(x: X, y: Y): Boolean }Leaving one or both parameters invariant is also legal but admits fewer subtyping conversions. These are type variance annotations.
For
Rel1, both parameters occur only as outputs. Scala's immutable List and Tuple2 are covariant, so a list of pairs of narrower types can safely be read as pairs of broader types. Thus both may be covariant type parameters. A contravariant declaration would permit, for example, treating a Rel1[Any, Int] containing (7, 0) as a Rel1[String, Int], then reading its first component as a String. That would be unsound; the compiler rejects the negative annotation at this output position.For
Rel2, X occurs as a method argument and therefore may be a contravariant type parameter; Y is returned in an immutable list and may be a covariant type parameter. A function that accepts every Any is safe to use where only String queries are issued. The opposite direction would be unsafe: if X were covariant, the following hypothetical conversion could call a string-only implementation with an integer:val strings: Rel2[String, Int] = new Rel2[String, Int] {
def relatives(x: String): List[Int] = List(x.length)
}
// Unsafe if Rel2 were incorrectly covariant in X:
// val arbitrary: Rel2[Any, Int] = strings
// arbitrary.relatives(7)Making
Y contravariant would instead allow an integer-valued Rel2[String, Any] to be read as a string-valued Rel2[String, String], recreating the output error.For
Rel3, both generic values are consumed and only a Boolean function result is produced, so both may be contravariant type parameters. A predicate accepting all values of broad types can answer queries restricted to narrower types. Covariance in either parameter would allow passing an unsupported value to a specialized implementation. For example, treating a string-only first-argument predicate as accepting Any would permit related(7, y) even though its body might call x.length. These are applications of the variance-position rule: method inputs reverse variance, whereas immutable outputs preserve it.[ref]Scala 2.13 variance annotations specification. Variance annotations and the change of position in method parameter types