Fresh-start bookkeeping for the DPDA characteristic grammar

The ordinary characteristic-grammar argument proves Knuth's condition for the grammar itself. CF_grammar.IsLRk, however, deliberately checks the grammar after adjoining one more fresh start symbol. This file discharges the extra start/start and start/ordinary cases. In particular, the wrapper below does not silently omit accept/reduce or accept/shift conflicts.

A generic no-reintroduction invariant

The outer augmentation is genuinely fresh

The characteristic start symbol is not reintroduced

Adding the outer fresh start preserves LR(1) here

theorem DPDA_to_LR.characteristic_isLR1_of_core {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hcore : (characteristicGrammar M).CoreIsLRk 1) : (characteristicGrammar M).IsLRk 1

For the reduced characteristic grammar, ordinary LR(1) handle uniqueness already implies the repository's augmented IsLRk 1 predicate.