Supporting results for pointwise provable equality.
The tag-4 induction case of certificate persistence #
evalnCertificateFormula_natCode_persist_of_tag_four concerns a standard index
q whose constructor number partrecCodeTag q is 4. It proves that the raw
evaluator certificate for q persists from a stage s to every stage t ≥ s,
assuming the same persistence for every standard index p < q, whatever the
constructor number of p. The persistence predicate is written out in both the
hypothesis and the conclusion. The theory assumptions are 𝐏𝐀 and 𝐈𝐎𝐩𝐞𝐧;
the proof obtains 𝐏𝐀⁻ from 𝐏𝐀 with models_of_subtheory.
The proof decomposes a successful source cell into certificates for the two
payload subcodes at stage s, applies the induction hypothesis once to each,
rebuilds the two table lookups at stage t with
eval_prefix_lookup_succ_of_codeHistoryEvaluator, and reconstructs the target
cell with eval_codeEvaluatorCell_succ_of_pair_component_lookups. The shared
helpers bound both payloads strictly below q and decompose the pairing branch.
The shared decoder readings and dispatcher branch theorem come from
Evaluator.CompositionDispatch. The fuel and the
program index that the cell reads are supplied by the generic public readings
eval_codeEvaluatorCell_fuel and eval_codeEvaluatorCell_index of
Evaluator.HistoryEvaluation.
The file states one induction case. It proves neither the cases for the other constructor numbers nor persistence for all standard indices.
Both subcodes of a standard constructor-4 index lie strictly below it.
Forward decomposition of a source tag-4 cell #
A successful source cell at a standard constructor-4 index yields a
history success for each subcode at the same stage, and the Cantor pair of the
two outputs.
The tag-4 strong-induction case #
Tag-4 induction case of certificate persistence. For a standard index
q of constructor number 4, persistence of the certificate for q from stage
s to any later stage t follows from persistence for every strictly smaller
standard index, whatever its constructor number. The persistence predicate is
written out in both the hypothesis and the conclusion.