F1 run_checks.sh exited 1 on any machine WITH SageMath. set -euo pipefail made
the declared-optional cross-checks fatal, so the script passed without the
optional tooling and failed with it. Optional calls are now guarded by
run_optional(), failures are counted and reported non-fatally, and the script
ends exit 0 with a summary line.
F2 false assertion in p28_lattice_hypotheses_certificate.sage. Component 1 read
216 + 108x + 46x; b2 = (1,2,1,0) contributes 216x, so the true value is
216 + 216x + 46x. The load-bearing identity below it (Bcomb == 4x*Crow) was
always correct, so no mathematics changes.
F3 Sage 10.9 raised 'keys do not match self's parent' at the subs() call: q
lives in the fraction field K while .numerator()/.denominator() return elements
of the underlying polynomial ring. The substitution key is now coerced into the
polynomial parent. This error had been MASKING F2.
Verified after the fixes:
run_checks.sh exit 0, 48 mandatory PASS (up from 43 -- the previously failing
certificate now runs to completion), 0 optional failures
falsifiability intact: 64R-44 -> 64R-43 exits 1, and 236337691420383 -> ...384
exits 1
pdflatex x3: 0 errors, 0 warnings, 0 undefined, 17 pages, 0 broken refs
Documentation: states plainly that no base is claimed superior to any other --
the non-injectivity holds for every b >= 2, [0,1] and [1] collide in decimal
exactly as in octal, and both repairs are stated for general b. Base 8 is only
the inherited worked example. Without this a reader could take the radix work
for a claim that base 8 beats base 10 or binary, which is not claimed anywhere.
Housekeeping: removes three Sage preparser .sage.py outputs that an earlier
'git add -A' in this branch had wrongly committed, and adds a .gitignore for
Sage and LaTeX build artifacts. Release zip and PDF rebuilt.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WY6SfRYvm8zFKMX9GcjS8u
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
Several terms across this programme are borrowed from molecular biology and
genetics (hachimoji, scar/scar-map, strand/braid, carrier, chirality, mutation)
and could be misread as claims about biological systems. They are not. This
document states the intended mathematical meaning of each, names the source
field it collides with, and says explicitly what is not being claimed.
Part 1 covers terms actually used in the 2.8 submission (seed, jet, carrier,
mutation, deformation, compact form, certificate, red case, authority tag),
grounded in solution.tex and the certificate scripts. Part 2 covers the
biology-adjacent vocabulary of adjacent repositories and is RECONSTRUCTED FROM
WORKING NOTES -- the author should confirm each entry before circulation.
Also records the load-bearing EXACT / NUMERICAL WITNESS / LITERATURE
distinction: the main claim rests only on EXACT and LITERATURE items, and
numerical enclosures are never used as premises.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WY6SfRYvm8zFKMX9GcjS8u
