Supporting results for pointwise provable equality.
Tag-6 certificate persistence #
Constructor number 6 is primitive recursion. This file proves conditional
certificate persistence at a standard index q with partrecCodeTag q = 6:
for arbitrary model stages s ≤ t, an arbitrary input and an arbitrary output,
a certificate for q at stage s persists to stage t, conditional on the
same persistence at every standard index p < q. The theory assumptions
throughout are 𝐏𝐀 and 𝐈𝐎𝐩𝐞𝐧; the proofs obtain 𝐏𝐀⁻ from 𝐏𝐀 with
models_of_subtheory.
The full theorem is assembled from two subcases distinguished by the recursion
argument of the input, and from the internal stage induction of
Evaluator.PersistenceInduction.
Write P_q(s) for the fixed-stage predicate of q at a model stage s: every
certificate for q at stage s, on every input and every output, persists to
every stage t ≥ s.
evalnCertificateFormula_natCode_persist_of_tag_six_zero concerns an input of
the form pair z 0, whose recursion argument is zero. It proves that the
certificate for q on that input persists from a stage s to every stage
t ≥ s, conditional on the same persistence for every standard index p < q,
whatever the constructor number of p.
evalnCertificateFormula_natCode_persist_of_tag_six_succ_step concerns an input
of the form pair z (a + 1), whose recursion argument is a successor. It
proves one step: a certificate at a stage k + 1 persists to every stage
t ≥ k + 1, conditional on both P_q(k) and persistence for every standard
index p < q. The two hypotheses govern disjoint lookups. The predecessor
lookup has index q, and only P_q(k) governs it; the step-payload lookup has
index partrecCodePayload₂ q < q, and only the smaller-index hypothesis governs
it. The theorem performs no induction on a model element.
The zero-argument proof derives the source history from the source certificate
and the source cell from the source history; the fuel s of that cell is
positive. It re-encodes q as the canonical primitive-recursion index of its
decoded payloads, reads the constructor number 6 and the two payloads inside
the model, and proves that the cell value is the value of the primitive-
recursion branch. By eval_codePrecEvaluatorCell_succ_iff_of_zero, at the
source stage the branch value is the value of the lookup of the base payload,
from which eval_codeHistoryEvaluator_succ_of_prefix_lookup derives a source
history of the base payload on z. The induction hypothesis is applied once,
at partrecCodePayload₁ q. At the target stage the reverse direction of the
same equivalence gives the branch its value; the target history value and
eval_codeEvaluatorCell_exists_of_values give the whole target cell a value,
and eval_unique identifies it with the branch value. The target cell then
gives the target history and the target certificate.
The successor-argument proof follows the same outline through the cell and the
branch, but uses eval_codePrecEvaluatorCell_succ_iff_of_succ, whose forward
direction produces an intermediate value x together with the predecessor
lookup and the step-payload lookup. The predecessor lookup at the source stage
becomes a history of q on pair z a at stage k, to which P_q(k) applies,
with k ≤ t - 1 derived from k + 1 ≤ t; the general earlier-row bridge
eval_codeTableLookup_succ_iff_codeHistoryEvaluator_of_history returns the
result to a lookup at the arbitrary target stage t, whose first environment
component is not a literal successor. The same general bridge, instantiated on
the lifted four-place environment of the step branch, relates both step-payload
lookups to histories of partrecCodePayload₂ q on pair z (pair a x), to which
the smaller-index hypothesis applies. The reverse direction of the successor
equivalence, at the same x, gives the target branch its value, and the
remaining steps are those of the zero-argument proof. No new public structural
bridge is required.
evalnCertificateFormula_natCode_persist_of_tag_six_succ assembles the complete
successor premise P_q(k) → P_q(k + 1) from the two subcases. An arbitrary
input u is pair (π₁ u) (π₂ u) by pair_unpair, and its recursion argument
π₂ u is split into the zero and positive cases by the dichotomy
0 < π₂ u ∨ 0 = π₂ u; the zero case is the zero-argument theorem at source
stage k + 1, and the positive case is the one-step successor theorem at
π₂ u - 1, the only case that uses P_q(k).
evalnCertificateFormula_natCode_persist_of_tag_six applies
certificate_persistence_of_stage_induction to that successor premise and to
the stage-zero premise evalnCertificateFormula_natCode_persist_of_stage_zero
of Evaluator.PersistenceInduction. The induction on the stage is internal to
the model and belongs to that interface; no induction on a model element occurs
in this file.
The generic readings of the history, the fuel and the program index are the
public theorems of Evaluator.HistoryEvaluation; the fourteen private helpers
below are local to this file.
Scope:
- this file proves tag-6 certificate persistence for a standard index of
constructor number
6, at arbitrary model stages, inputs and outputs, conditional on persistence at every smaller standard index; - that hypothesis is discharged only by the external induction on the standard index, which is not proved in the library;
- it proves no persistence case at constructor numbers
0–3or7; - it proves no persistence theorem for every standard index;
- it proves no theorem of Appendix B.
Re-encoding and readings at a standard tag-6 index #
A standard tag-6 index, cast into the model, is the canonical primitive-recursion index of its decoded payloads.
The constructor number 6, read at a standard tag-6 index.
The base payload, read at a standard tag-6 index.
The step payload, read at a standard tag-6 index.
The constructor-6 branch of the eager dispatcher #
With positive fuel and a tag reading of 6, the cell value is the value of
the primitive-recursion branch. The first comparison of the dispatcher, with
4, and the second, with 5, both fail, and the third, with 6, succeeds.
Fuel arithmetic and the readings the branch uses #
The dispatcher evaluates the branch at the decremented fuel k - 1; for
positive k, its successor, the key of the base lookup, is k.
Relating the base lookup of the branch to the history bridges #
The branch reads its table, key, query and argument through decoded codes; the history bridges use the fuel key, a constant query and the argument itself. The four congruences below prove that the two forms have the same values.
The branch key reading agrees with the source-stage constant.
The decoded base-program query agrees with its constant index.
The zero-argument case #
Tag-6 certificate persistence on a zero recursion argument. For a
standard index q of constructor number 6, a certificate on an input
pair z 0 persists from a stage s to any later stage t, given persistence
for every strictly smaller standard index. This is the zero-argument
induction subcase only; the successor argument is not treated here.
The step argument of the successor branch #
The step lookup reads the argument pair z (pair a x) in the lifted
environment, where the intermediate value x is the new head.
The successor-argument one-step persistence theorem #
Tag-6 certificate persistence on a successor recursion argument, one
step. For a standard index q of constructor number 6, assume persistence
for every smaller standard index (ih) and the whole fixed-stage predicate at a
model stage k (hpred). Then a certificate at stage k + 1 on an input
pair z (a + 1) persists to every stage t ≥ k + 1.
The predecessor lookup has index q, so it is governed by hpred; the
step-payload lookup has index partrecCodePayload₂ q < q, so it is governed by
ih. This theorem performs no induction and does not use
certificate_persistence_of_stage_induction.
The complete successor premise over arbitrary inputs #
The complete successor premise at constructor number 6. Assume
persistence at every standard index p < q and the whole fixed-stage predicate
of q at a model stage k. Then the fixed-stage predicate of q holds at
k + 1, over arbitrary inputs.
The arbitrary input u is decomposed by pair_unpair into
pair (π₁ u) (π₂ u), and the recursion argument π₂ u is split into its zero
and positive cases by the ordered-semiring dichotomy 0 < π₂ u ∨ 0 = π₂ u. The
zero case is the zero-argument theorem above, at source stage k + 1; the
positive case is the one-step successor theorem above, at π₂ u - 1, and is the
only case that uses the supplied predicate at k. The proof performs no
induction; that dichotomy is its only split.
Full conditional tag-6 persistence #
Tag-6 certificate persistence. For a standard index q of constructor
number 6, a certificate persists from every stage s to every stage t ≥ s,
on arbitrary input and output, conditional on persistence at every standard
index p < q. The internal induction on the stage is
certificate_persistence_of_stage_induction; this theorem supplies its two
premises, the stage-zero premise of Evaluator.PersistenceInduction and the
complete successor premise above, and does not reproduce the induction.