docs(p28): radix layer -- framing and DFA canonicalisation are bijections

Documents the radix formulation from MathPunch-FiniteState
(coq/MathPunchFiniteStateAudit/Radix.v, MathPunchFiniteState/Radix.lean), which
is the correctness obligation underneath the encoder method.

The defect, proved rather than asserted: positional evaluation is not injective
on digit strings. Both collisions are machine-checked in Coq and Lean --
eval_digits 8 [0;1] = eval_digits 8 [1], and eval_digits 8 [] = eval_digits 8
[0]. Quantified: in base 8 over lengths 0-3, 585 strings collapse onto 512
values.

Two repairs, both BIJECTIONS onto correctly stated codomains:
  framing  : digit strings  <->  U_n {n} x [0, b^n)
             verified exhaustively base 8, n=0..4 (1,8,64,512,4096; no gaps)
  DFA      : canonical numerals  <->  N+
             verified base 8 to length 5 (32767 strings, values exactly [1,8^5))

Bijectivity is the operative property, not injectivity: injectivity says
encodings do not collide, bijectivity says decoding is TOTAL on the valid
codomain. Stating the codomain as N x N would make framing merely injective;
stating it correctly makes it bijective.

Distinctiveness assessed fairly: the content is classical numeration-system
material (regular numeral languages, canonical numeration, Cobham). The
distinctive move is making it an explicitly proved prerequisite of an encoding
pipeline, with the collisions exhibited as theorems in two proof assistants.

Also flags a maintenance hazard: the DFA and toDigits exist only in Radix.lean;
Radix.v has eval_digits and framed_value alone. Lean is regenerated from coq/*.v
in that repo, so regeneration would silently erase the automaton.

Corrects NOTATION_AND_BORROWED_TERMINOLOGY.md: the blanket 'no biology claim
anywhere' disclaimer was too strong and is now scoped to this submission, since
a Lean probe elsewhere deliberately models expanded genetic alphabets (4/8/12
letters) and proves an optimality statement about them.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WY6SfRYvm8zFKMX9GcjS8u

experiments/ramanujan_28/submission/NOTATION_AND_BORROWED_TERMINOLOGY.md

@@ -7,14 +7,23 @@ Some names are invented; others are borrowed from unrelated disciplines because
 they were short and evocative, and then given a purely mathematical meaning.
 
 That borrowing creates a specific hazard. A reader who knows the source field
-may read a term as a claim about that field. **Several terms used across this
-programme are borrowed from molecular biology and genetics. No claim about
-biology, genetics, or any physical or biochemical system is made anywhere in
-this work.** Every object named below is defined entirely by its equations, and
-those equations are the only content.
+may read a term as a claim about that field.
 
-If a term looks like it is asserting something about the natural world, it is
-not. Read the definition, not the word.
+**Scope of the disclaimer, stated precisely.** Nothing in *this submission*
+(Ramanujan Challenge Problem 2.8) makes any claim about biology, genetics, or
+any physical or biochemical system. Every object in it is defined entirely by
+its equations, and those equations are the only content.
+
+Elsewhere in the wider programme the situation is not uniform, and it would be
+misleading to claim otherwise. At least one artefact — a Lean probe on expanded
+genetic alphabets — deliberately models alphabet sizes drawn from synthetic
+biology (4, 8, 12 letters) and proves an optimality statement about them. That
+is a mathematical result about alphabet size, not an empirical claim about
+molecules, but it is *not* merely a borrowed word either. **The author should
+confirm the intended reading of any such artefact before it is circulated.**
+
+For the borrowed vocabulary in Part 2, the rule holds: read the definition, not
+the word.
 
 ---
 

experiments/ramanujan_28/submission/THE_ENCODER_APPROACH.md

@@ -155,6 +155,153 @@ receipt rather than dropped after discovery. Calling it "unique" would be too
 strong; calling it a recognisable method used unusually systematically is
 defensible.
 
+## The radix layer: why a codec needs more than positional notation
+
+Everything above assumes objects can be written as digit strings and read back.
+That assumption fails for ordinary positional notation, and repairing it is the
+part of this approach with the strongest claim to being non-standard.
+
+**Formulation, from MathPunch-FiniteState** (`coq/MathPunchFiniteStateAudit/Radix.v`,
+mirrored in `MathPunchFiniteState/Radix.lean`):
+
+```coq
+Fixpoint eval_digits (base : nat) (digits : list nat) : nat :=
+  match digits with
+  | [] => 0
+  | digit :: rest => digit * Nat.pow base (length rest) + eval_digits base rest
+  end.
+
+Definition framed_value (base : nat) (digits : list nat) : nat * nat :=
+  (length digits, eval_digits base digits).
+```
+
+### The defect, proved rather than asserted
+
+Positional evaluation is **not injective on digit strings**. Two collisions are
+machine-checked in both Coq and Lean:
+
+```coq
+Example ordinary_radix_leading_zero_collision :
+  eval_digits 8 [0; 1] = eval_digits 8 [1].          (* both = 1 *)
+
+Example empty_word_and_zero_symbol_collide_unframed :
+  eval_digits 8 [] = eval_digits 8 [0].              (* both = 0 *)
+```
+
+This is invisible in ordinary mathematics, where radix notation exists only to
+*denote numbers* — `[0,1]` and `[1]` denote the same number and there is nothing
+more to say. It becomes fatal the moment digit strings are used as a **codec for
+objects**, because distinct objects then encode to the same numeral.
+
+Quantified in base 8 over lengths 0–3: **585 distinct digit strings collapse
+onto 512 distinct values.** 73 strings are destroyed.
+
+### Two repairs, both in the source
+
+**1. Framing** — adjoin the length:
+
+```coq
+Example framing_repairs_leading_zero_collision :
+  framed_value 8 [0; 1] <> framed_value 8 [1].       (* (2,1) vs (1,1) *)
+
+Example framing_separates_empty_word_and_zero_symbol :
+  framed_value 8 [] <> framed_value 8 [0].           (* (0,0) vs (1,0) *)
+```
+
+Framing is not merely injective — it is a **bijection**, onto the correctly
+stated codomain:
+
+```
+framed_value_b : { digit strings over base b }  ⟶  ⋃_n {n} × [0, b^n)
+```
+
+Verified exhaustively in base 8 for every length `n = 0..4`: the image is
+*exactly* `{n} × [0, 8^n)`, with sizes 1, 8, 64, 512, 4096 — no collisions and no
+gaps. (It is of course **not** surjective onto all of `ℕ × ℕ`: the pair `(1,100)`
+is unreachable in base 8, since a length-1 string has value `< 8`. Stating the
+codomain as `ℕ × ℕ` would make the map merely injective; stating it correctly
+makes it bijective.)
+
+Bijectivity, not injectivity, is the property a codec needs. Injectivity alone
+says encodings do not collide; bijectivity says **decoding is total** on the
+valid codomain — every admissible framed pair is the image of exactly one
+string, so the inverse map exists everywhere it should.
+
+**2. Canonicalisation by finite automaton** — restrict to a canonical language
+instead of enlarging the codomain. `Radix.lean` carries a three-state DFA
+(`start`, `body`, `dead`) that rejects a leading zero at the `start` state,
+rejects out-of-range digits, and rejects the empty word:
+
+```lean
+def radixDfaStep (base : Nat) : RadixState → Nat → RadixState
+  | .start, 0 => .dead      -- leading zero
+  | .start, d => if d < base then .body else .dead
+  | .body,  d => if d < base then .body else .dead
+  | .dead,  _ => .dead
+```
+
+This too is a **bijection**, and the classical one:
+
+```
+{ DFA-accepted canonical numerals in base b }  ⟷  ℕ⁺
+```
+
+Verified exhaustively in base 8 up to length 5: 32767 canonical strings, 32767
+distinct values, forming *exactly* the interval `[1, 8^5)`. Note the codomain is
+`ℕ⁺`, not `ℕ` — the empty word is rejected, so `0` has no canonical
+representation in this language. That is a deliberate choice, and it is the
+price of the narrowing repair.
+
+This is what the repository name *FiniteState* refers to. Framing widens the
+target so nothing collides; the DFA narrows the source so nothing ambiguous is
+admitted. Both yield bijections — onto `⋃_n {n} × [0, b^n)` and onto `ℕ⁺`
+respectively — so they solve the same obligation from opposite directions, with
+different codomains and different edge-case costs.
+
+### Why this matters to the encoder
+
+The encoder in Part 1 reads coordinates out of exact data. For that to be a
+*codec* rather than a lossy summary, the map from strings to objects must be a
+**bijection onto a stated codomain**. Injectivity alone is not enough: it would
+guarantee that no two objects share an encoding, but not that an encoding can be
+decoded — leaving the inverse partial and the codec unusable in the direction
+that matters. Bijectivity gives a total decode.
+
+Without it, a recovered encoding does not determine what it came from, and "the
+coordinates are meaningful" becomes unfalsifiable. The radix layer is the
+correctness obligation underneath the whole method, and it is discharged by
+proof rather than by convention.
+
+### How distinctive is this, honestly
+
+**Precedent exists.** That the set of valid numerals is a regular language, and
+that leading zeros must be excluded for canonical numeration, is standard in
+automata theory and the theory of numeration systems (base-`k` recognisable
+sets, Cobham's theorem, and the usual treatment of canonical numeration systems
+all depend on exactly this). The observation itself is not new.
+
+**What is less usual:**
+
+- Treating non-injectivity of radix notation as a **proof obligation of a
+  mathematical encoding pipeline**, rather than as a background convention.
+- Discharging it in **two proof assistants** with explicit collision witnesses —
+  stating the defect as a proved `Example` rather than a remark.
+- Carrying both repairs (framing *and* the DFA) side by side, so the encoder can
+  choose whether to widen the codomain or restrict the domain.
+
+**Fair summary:** the mathematical content is classical numeration-system
+material; the distinctive move is making it an explicitly proved prerequisite of
+an encoding method, with the collisions exhibited as theorems. That is a
+methodological contribution, not a new theorem about numeration.
+
+### Maintenance hazard
+
+The DFA (`RadixState`, `radixDfaStep`, `radixDfaAccepts`) and `toDigits` exist
+**only in the Lean file**; `Radix.v` has `eval_digits` and `framed_value` alone.
+In this repository Lean is regenerated from `coq/*.v`, so a regeneration would
+silently erase the automaton. Either port the DFA to Coq or exempt `Radix.lean`
+from regeneration.
+
 ## The general recipe
 
 1. Take opaque exact data.