Supporting results for pointwise provable equality.
Fixed component indices and evaluator-cell reconstruction #
When the index under evaluation has constructor number 5, the eager branches
of codeEvaluatorCell collapse to the composition branch, and a successful cell
yields the two table lookups that branch performs:
eval_codeEvaluatorCell_succ_of_tag_five.
For the canonical index of a composed program the two component indices are
known natural numbers. eval_codeEvaluatorCell_succ_of_canonicalPartrecCompIndex
replaces the decoded queries by the constant codes of those numbers, so that a
later argument can reason with fixed indices rather than with decoder terms.
The replacement is a graph equivalence at the given assignment, not a
definitional one: eval_codeTableLookup_query_congr performs it, and
eval_iff_codeConst_of_eval supplies its hypothesis.
The outer lookup needs one further step. Transporting the payload equivalence
under codeLift produces codeLift (codeConst (n := r) fCode), which is
evaluation-equivalent but not definitionally equal to the arity-r + 1 constant
the statement asks for; eval_codeLift_codeConst_iff closes that gap.
These results are forward extraction from a successful cell over 𝐏𝐀⁻. They
construct no cell, so the eager evaluation of the unused branches is not an
obstacle for them.
The composition reverse theorem,
eval_codeEvaluatorCell_succ_of_component_lookups, does construct a cell.
codeIfPos is a sum of products
containing both of its branches, so an evaluation of the cell needs a value for
every branch, not only the composition branch. Over 𝐏𝐀,
eval_codeEvaluatorCell_exists_of_values gives the entire eager cell a value;
positive fuel and tag 5 force the composition branch in that evaluation, and
eval_unique identifies the cell value with the value of the composition branch
built from the two component lookups.
The pairing analogue,
eval_codeEvaluatorCell_succ_of_pair_component_lookups, starts from a standard
constructor-4 index and successful lookups at its two decoded payloads. It
constructs the eager cell with the same existence theorem, forces the pairing
branch using positive fuel and the decoded tag, and identifies the result with
pair a b + 1. Its decoder-reading and branch-selection lemmas remain private.
This result does not transport certificates between stages or prove persistence
for recursively referenced subcodes.
A successful evaluator cell whose index has constructor number 5 performs
the two lookups of the composition branch.
Fixed component indices for canonical program composition.
From a successful evaluator cell whose index is the canonical index of the
composition of fCode and gCode, the inner lookup runs the constant gCode
and the outer lookup the constant fCode, both at their own arities.
Reverse direction of eval_codeEvaluatorCell_succ_of_canonicalPartrecCompIndex,
with positive fuel as an additional hypothesis: at the canonical index of the
composition of fCode and gCode, the two component lookups give the evaluator
cell the value y + 1.
The lookups are first returned to the decoded queries, and
eval_codeCompEvaluatorCell_succ_iff gives the composition branch the value
y + 1. Values of dtable and dn are read from the inner lookup, and
eval_codeEvaluatorCell_exists_of_values gives the entire cell some value z.
Positive fuel and tag 5 select the composition branch in that evaluation, so
z = y + 1 by eval_unique.
𝐏𝐀 is the only theory assumption; eval_codeEvaluatorCell_exists_of_values
assumes it. 𝐈Σ 1 is installed inside the proof and supplies 𝐏𝐀⁻ through
Foundation's instance chain, and the index enters through
ORingStructure.numeral.
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.
A successful evaluator cell whose constructor number is 4 is the value of
the pairing branch. Adapted from the accepted external tag-4 probe.
Fixed component lookups build the whole pairing cell.
For a standard index q of constructor number 4, two successful component
lookups at the constant codes of its two subcodes — both at the same fuel and the
same argument, as pairing requires — give the entire eager evaluator cell the
value pair a b + 1. Nothing about the cell's own success is assumed.