# A parity invariant for arbitrary word length [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-regular-language/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-regular-language-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope All words over {0,1} with an even number of 1s form a regular language. A complete DFA and an invariant for every prefix; no regex or NFA machinery. ## Givens and symbols - calc - G1 — Q={E,O}, alphabet={0,1}, start E, finals {E}; transitions E0 to E,E1 to O,O0 to O,O1 to E; L consists of words with an even number of 1s. - c(w) — number of 1s in the word - I(w) — prefix-parity invariant ## Rules and sources - calc · prerequisite — Assume finite sets, finite strings and indices, stepwise function updates and induction on natural numbers; epsilon denotes the length-zero word. - mko_definition · cited — The DFA certificate must cover every finite word over the declared alphabet. Mod-count and parity languages use a state invariant valid for arbitrary word length; a finite language can use a prefix-trie DFA construction. Finitely many tested words do not prove regularity or language equivalence. · mko-regular-language ## Main derivation S01 · impliesBefore Q\times\Sigma\text{ has four pairs} After \begin{array}{c|cc}\delta&0&1\\\hline E&E&O\\O&O&E\end{array} Conditions: none Rule: calc · Uses: G1 Leaf basis: calc All four cells have one valid output, so the DFA can read every finite word. S02 · impliesBefore c(w)=\#\{i:w_i=1\} After I(w):\ \delta^*(E,w)=E\iff c(w)\equiv0\pmod2 Conditions: none Rule: calc · Uses: G1, S01 Leaf basis: calc State the universal target invariant: the state records parity of the count of 1s in the prefix. S03 · induction_baseBefore w=\varepsilon After c(\varepsilon)=0,\quad\delta^*(E,\varepsilon)=E\Rightarrow I(\varepsilon) Conditions: none Rule: calc · Uses: G1, S02 Leaf basis: calc Base case: the empty word contains zero 1s, an even count, and with no input consumed the automaton remains in state E. S04 · induction_stepBefore I(w),\quad w'=w0 After c(w0)=c(w),\quad\delta(E,0)=E,\ \delta(O,0)=O\Rightarrow I(w0) Conditions: the induction hypothesis I(w) holds Rule: calc · Uses: G1, S01, S02 Leaf basis: calc Appending 0 preserves both count and state, covering either prior parity. S05 · induction_stepBefore I(w),\quad w'=w1 After c(w1)=c(w)+1,\quad E\xrightarrow{1}O,\ O\xrightarrow{1}E\Rightarrow I(w1) Conditions: the induction hypothesis I(w) holds Rule: calc · Uses: G1, S01, S02 Leaf basis: calc Appending 1 flips both parity and state, matching both cases. S06 · impliesBefore I(\varepsilon),\quad I(w)\Rightarrow I(w0),I(w1) After \forall w\in\{0,1\}^*:\ I(w) Conditions: none Rule: calc · Uses: G1, S03, S04, S05 Leaf basis: calc Every finite word is formed from epsilon by appending 0 or 1, so induction proves the whole-language invariant. S07 · impliesBefore F=\{E\},\quad\forall w:\ I(w) After w\text{ accepted}\iff w\in L\Rightarrow L\text{ regular} Conditions: none Rule: mko_definition · Uses: G1, S01, S06 Leaf basis: mko_definition The complete DFA accepts exactly words with even 1-count, a universal recognition certificate for L. S08 · impliesBefore w=1011,\quad v=1010 After c(w)=3\Rightarrow w\notin L;\quad c(v)=2\Rightarrow v\in L Conditions: none Rule: calc · Uses: G1, S06, S07 Leaf basis: calc Two examples illustrate the proven invariant without replacing the proof. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1, S06, S07 — Many different languages share finite samples, so samples alone cannot certify equivalence. - S07 · premise_audit · G1, S01, S06 — Both directions follow from I(w), not merely inclusion of L in the accepted language. - S06 · premise_audit · G1, S03, S04, S05 — Induction covers arbitrary length without a test cutoff. - S05 · premise_audit · G1, S01, S02 — O1 to E ensures odd plus one becomes even, covering the reverse direction too. - S04 · premise_audit · G1, S01, S02 — Both E and O zero-transitions are checked, not only the even case. - S03 · premise_audit · G1, S02 — Epsilon is not a character and contributes no symbol count. - S02 · premise_audit · G1, S01 — Naming E 'even' is not proof; induction below is required. - S01 · premise_audit · G1 — Model qualification alone is not recognition of the specified L; an invariant is still required. ## Error controls and negative controls Universal invariantUse induction on length, not a finite test list for L. Both directionsFinal state E iff even must cover both acceptance and nonacceptance. - Testing lengths at most 4 proves L regular. → reject — A complete DFA invariant for arbitrary length is required; finite samples do not determine a language. - Words with an odd number of 1s lie in L. → reject — The invariant ends at nonfinal O, for example word 1. - This certificate proves any two DFAs equivalent. → reject — It certifies this DFA and the specified L only. ## Result and limitations All words over {0,1} with an even number of 1s form a regular language. ## Verification and source binding 0 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 8b3f94b7386f3cfa6772b2ab39314f3cdfe8dbb931e9468ee42f746ee7293ecb - original source SHA-256: 1805ff983292495019f5c1345bf8dfe377b3ed25ba222aa28cd86de46fed3f90 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-regular-language-01.json)