diff --git a/experiments/ramanujan_28/submission/NOTATION_AND_BORROWED_TERMINOLOGY.md b/experiments/ramanujan_28/submission/NOTATION_AND_BORROWED_TERMINOLOGY.md index f4ea030..00a6267 100644 --- a/experiments/ramanujan_28/submission/NOTATION_AND_BORROWED_TERMINOLOGY.md +++ b/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. --- diff --git a/experiments/ramanujan_28/submission/THE_ENCODER_APPROACH.md b/experiments/ramanujan_28/submission/THE_ENCODER_APPROACH.md index 90ccd3c..03eba41 100644 --- a/experiments/ramanujan_28/submission/THE_ENCODER_APPROACH.md +++ b/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.