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
7.7 KiB
Notation, invented terminology, and borrowed words
Why this document exists
This work crosses several fields, and its vocabulary was assembled accordingly. 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.
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.
Part 1 — Terms used in this submission
These are grounded in solution.tex and the certificate scripts, and are the
ones an evaluator of Problem 2.8 will actually meet.
| Term | Meaning here | Ordinary meaning it may collide with |
|---|---|---|
| seed, seed row | The two official integer initial-condition rows A_0, A_1 of the recurrence. Nothing grows; "seed" only marks where the iteration starts. |
Botany; also "seed" in cryptography/RNG, which is closer but still not this. |
| jet | Truncated local expansion data of a function at a point — the standard differential-geometry sense (an equivalence class of functions agreeing to finite order). | Aviation; fluid jets; the physics "jet" of particles. None apply. |
| carrier | The vector space or module on which an operator or representation acts — the object that carries the structure. Standard representation-theory usage. | Genetics: a carrier of an allele. Not intended, not implied. |
| mutation, mutant | Software mutation testing: deliberately corrupting a constant to confirm a passing check is capable of failing. E.g. changing 64R-44 to 64R-43 must produce an AssertionError. |
Genetic mutation. Entirely unrelated. The "mutant" is a modified copy of a Python file. |
| deformation, deformed family | Replacing the constant R by a free variable r = 1/x, giving a one-parameter analytic family that specialises to the official matrix at x_0 = 1/R. Standard deformation-theory usage. |
Materials science. |
| compact form | A short generating expression (Pascal rows b_0..b_3, the row C(x), constants A, B, S) that reproduces the large official integer data exactly. A re-encoding, not an approximation. |
"Compact" in topology — unrelated here. |
| certificate | An executable script whose assertions, if they all pass, witness a stated mathematical fact. | Cryptographic certificates; academic certificates. |
| red case, negative control | A deliberately false input included to prove the check can fail. Borrowed from experimental science, and used in the same spirit. | — |
| authority tag | A per-claim label recording how a statement is known: EXACT (integer/rational arithmetic), NUMERICAL WITNESS (high-precision identification, not proof), LITERATURE (cited, not re-proved). |
— |
On EXACT versus NUMERICAL WITNESS
This distinction is load-bearing and is not merely stylistic. EXACT means the
statement is closed under exact arithmetic with no floating point anywhere.
NUMERICAL WITNESS means a quantity was identified to some number of digits —
strong evidence, not a proof. The submission's main claim rests only on
EXACT and LITERATURE items; numerical enclosures appear as corroboration and
are never used as premises.
Part 2 — Borrowed words from biology, used in the wider programme
These do not appear in the Problem 2.8 submission, but they appear in adjacent repositories that an evaluator may encounter. They are the terms most likely to be misread as biological claims.
Reconstructed from working notes — the author should confirm each definition before this document is circulated.
| Term | Meaning in this work | Source field | Explicitly NOT a claim about |
|---|---|---|---|
| hachimoji | A base-8 encoding/decoding scheme (a codec) used to render algebraic invariants as short strings. The name was taken purely because the source system has eight symbols. | Benner et al.'s hachimoji DNA, a synthetic 8-letter genetic alphabet (Japanese 八文字, "eight letters"). | DNA, nucleotides, synthetic biology, base pairing, or any biochemical system. It is an integer-encoding convention and nothing else. |
scar (as in SCAR-013) |
A registry entry recording a route that has been proved impossible, together with its witness and a redirect to a live route. A permanent mark left by a closed-off attempt. | CRISPR / molecular cloning: a "scar" is residual sequence left after an editing or ligation step. | Gene editing, CRISPR, recombination, or any laboratory procedure. |
| scar-map | A tabulated collection of such exclusion records (e.g. the Δ₇ scar-map). |
as above | as above |
| strand, braid | Strands of a mathematical braid group B_n — topological curves in a cylinder, and their linear representations (Burau, Lawrence–Krammer–Bigelow). |
DNA strands, double helix. | DNA, chromosomes, or any molecular structure. The braid group is a purely topological/algebraic object. |
| chirality, chiral | Handedness — the orientation or sign convention of a basis or lookup table. | Chemistry (stereochemistry), particle physics. | Molecular handedness or any chemical claim. |
| codebook | An information-theoretic dictionary mapping objects to short canonical labels. | Coding theory (correct source); also espionage. | — |
The general rule
Where a borrowed word could be read as a claim about a natural system, it is being used metaphorically for structure only. The mathematics is defined by its equations; the name is a label chosen for brevity, and carries none of the source field's content, mechanisms, or empirical commitments.
Part 3 — Why the vocabulary is like this, stated plainly
The programme spans modular forms, hypergeometric series, braid representations, formal verification, and computational infrastructure. Working across that range produces a lot of objects that need names faster than the literature supplies them. Borrowing a short, memorable word from an unrelated field is efficient for a solo author and costly for a reader — the cost only becomes visible when the work is read by someone fluent in the source field.
This document is the correction. It is not an apology for the naming; it is a key, so that no reader has to guess whether a biological word implies a biological claim. It does not.
Part 4 — Reading rule for evaluators
- Every mathematical object is defined by displayed equations. If a name and an equation disagree, the equation governs.
- No statement in this work is a claim about genetics, molecular biology, chemistry, or any physical system.
- Where a term is borrowed, Part 1 or Part 2 gives the intended meaning and the collision it may cause.
- The distinction between
EXACT,NUMERICAL WITNESS, andLITERATUREis substantive; see Part 1.