Supporting results for pointwise provable equality.
Evaluation of the derived constructors at standard numerals #
Where CategoricalRiceShapiro.ArithmeticCode.Evaluation characterises the
graph of a constructor at arbitrary values, the results here compute it at the
image of a natural number. A code whose graph holds at (n : M) has, at the
same assignment, the graph of its truncated difference, integer square root and
Cantor components at the corresponding natural numbers.
eval_codeIfPos_of is the introduction rule for the eager conditional and is
used by every proof below; it evaluates both branches, as the construction does.
eval_of_computes is the bridge from the standard model: a code that realizes a
function over ℕ has, in any model of 𝐏𝐀⁻, the graph of that function at the
images of standard arguments. It is the only route by which a construction
proved correct over ℕ — here halving, defined by primitive recursion — becomes
usable in an arbitrary model.
The eager conditional #
Introduction rule for codeIfPos. Both branches are evaluated, and the
test selects which of their values the conditional takes.
Elimination rule for codeIfPos: a value of the conditional comes from one
of the two branches, chosen by the test. Converse of eval_codeIfPos_of.
Truncated subtraction #
Truncated subtraction at standard numerals.
Integer square root and Cantor unpairing #
The integer square root at a standard numeral.
The first Cantor component at a standard numeral.
The second Cantor component at a standard numeral.
The standard-model bridge #
A code realizing f over ℕ has the graph of f at standard arguments in
any model of 𝐏𝐀⁻.
Computes is a statement about ℕ. Sigma-one completeness transports the
corresponding sentence, whose free variables are all interpreted by numerals.
Halving at a standard numeral.
Divisibility, remainder and parity #
Introduction rule for the non-strict comparison.
Divisibility at standard numerals.
Remainder at standard numerals.
Parity at a standard numeral.
Truncated subtraction, square root and the Cantor components at #
arbitrary values
The results above compute a constructor at the image of a natural number. Those
below compute the same constructors at an arbitrary element, against the
operations the pinned IOpen theory of Foundation already supplies:
FFL.FirstOrder.Arithmetic.sqrt, pair, pi₁ and pi₂, together with their
specifications. No arithmetic identity is reproved here; each proof only
matches a code against the operation Foundation defines.
Truncated subtraction at arbitrary values.
The integer square root at an arbitrary value, given the defining bounds.
The integer square root at an arbitrary value.
Cantor pairing at arbitrary values.
The first Cantor component at an arbitrary value.
The second Cantor component at an arbitrary value.
The first Cantor component of a pair is its first argument.
The second Cantor component of a pair is its second argument.
Divisibility, remainder and the Gödel beta value at arbitrary values #
codeDvd searches for the least quotient candidate, codeRem searches for the
least amount whose removal leaves a multiple of the divisor, and codeBeta
composes the two Cantor components with that remainder. The three results below
compute each construction at arbitrary elements of a model of 𝐈𝐎𝐩𝐞𝐧, against
the division and remainder Foundation already defines there. No division
identity is reproved; each proof identifies the searched value and shows that
the search body vanishes below it.
Divisibility at arbitrary values.
The remainder at arbitrary values.
The Gödel beta value at arbitrary values. eval_codeBeta in Arithmetic
computes the same construction over ℕ; this result instead proves that the
graph of codeBeta N I holds at the displayed remainder in an arbitrary model.
It does not assert the existence of a finite sequence with that beta value.
The eager conditional has a value once its test and both of its branches have one. Both branches are evaluated whichever way the test goes.
The constructor number of a standard index, read inside a model.
The payload of a standard compound index, read inside a model.
The first subcode of a standard index, read inside a model.
The second subcode of a standard index, read inside a model.