Lemma·L67
Formula parse balance agrees with term parse balance, on terms
Recomputing a term's balance with the wider formula-level weight function gives exactly the same values as before, since a term never contains a relation symbol or logical symbol.
For a language
and
with
:
and
In words
For any term of the language, with n its length: its formula-level parse balance still reaches exactly zero after all n symbols, and still stays at least one at every earlier position - recomputing with the wider weight function changes nothing on a term.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 (computed from the citation graph, not asserted).
Proof
- 1Every entry of a term is a variable or function symbol. By structural induction on : if , its only entry is . If with and every entry of every ( ) already a variable or function symbol (inductive hypothesis, "IH"): entry is (T29). For , using the bookkeeping from the proof of T31 (where increases from at to at , and ): falls in for a unique , and by T29 applied to , , a variable or function symbol by the IH applied to . So every entry of is a variable or function symbol.
- 2
- 3. Both are characterized as the unique function with value at and, at every , the step rule "value at equals value at , plus the weight at , minus " - for using weight (D090), for using weight (D088), each via the recursion theorem. By Step 2 these are the identical recursive characterization, so by its uniqueness clause as functions .
- 4By T31, and ; by Step 3 the same holds with in place of .
∎
Remarks
A term never contains a relation symbol or a logical symbol - it is built only from variable and function symbols - so the extra cases in h_tau never fire on a term, and
collapses to exactly "bal"_tau. This is what lets the formula balance invariant invoke the already-established term invariant directly in its atomic cases (equality, relation application), rather than re-deriving term balance from scratch inside the formula-level argument.