Skip to content

Commit 82ee24f

Browse files
HdpbillyHdpbilly
committed
README rewrite
1 parent cfedaef commit 82ee24f

1 file changed

Lines changed: 136 additions & 115 deletions

File tree

‎README.md‎

Lines changed: 136 additions & 115 deletions
Original file line numberDiff line numberDiff line change
@@ -12,131 +12,152 @@
1212
from positional notation as algebra, through certified digit-emission engines,
1313
to the geometry and conservation laws of coupled radix networks.**
1414

15-
[Specification](docs/fdrs.md) · [Index](docs/fdrs-index.md) · [Design records](docs/synthetic-place/) · [Toolchain](scripts/)
15+
[The spec](docs/fdrs.md) · [Item index](docs/fdrs-index.md) · [Design records](docs/synthetic-place/) · [Tooling](scripts/)
1616

1717
</div>
1818

1919
---
2020

21-
## What this is
22-
23-
This repository is a long-form mathematical research program carried out
24-
spec-first in a single document and machine-checked item by item in Lean 4
25-
against [Mathlib](https://github.com/leanprover-community/mathlib4). The
26-
specification ([`docs/fdrs.md`](docs/fdrs.md)) has grown through **fourteen
27-
phases** of numbered definitions, theorems, and propositions; every numbered
28-
item has a Lean proof, and the correspondence is maintained by tooling rather
29-
than by prose claims. The default build carries **zero axioms and zero
30-
sorries**.
31-
32-
The subject is *what number representation becomes when its structure is a
33-
free parameter*. Classical positional notation fixes a base; FDRS lets the
34-
radix at each position be computed by a function — of the position, the prefix
35-
already written, an external context, or the state of another number line
36-
entirely. The corpus develops what survives each generalization and what
37-
breaks, with the boundary in every case proven, not asserted.
38-
39-
**The arc:** foundations (canonical bijections with ℕ, the odometer, the
40-
prefix ultrametric, a conditional-expectation multiresolution analysis on
41-
mixed-radix cylinders, and the bridge to analytic number theory) → the three
42-
modes of function-defined radices and the design space of engineered
43-
ultrametrics → multi-timeline routing and spatialized digits → generated
44-
gauges, where continued-fraction timelines replace base products and digit
45-
emission becomes a *certified* act → the synthetic place complex: coupled
46-
radix networks, their geometry, their conservation laws, and the precise
47-
obstructions separating them from numbers.
48-
49-
## Selected results
50-
51-
A sample chosen to show the range; the [index](docs/fdrs-index.md) maps every
52-
item to its proof.
53-
54-
**Foundations and bridges.**
55-
- Canonical bijections between digit spaces and ℕ; the tick is `+1` under
56-
decode and `1`-Lipschitz in the ultrametric; balls are exactly cylinders.
57-
- A discrete multiresolution analysis: block projections as conditional
58-
expectations, detail operators, L² Pythagoras, and the commutant theorem —
59-
an operator commutes with every scale projection iff it is
60-
scale-block-diagonal in the Haar/contrast basis.
61-
- The cylinder-measurability bridge: a congruence condition is decidable from a
62-
positional prefix **iff** the modulus divides the place value (both
63-
directions, with the sharp converse) — the exact interface between the
64-
additive and multiplicative filtrations, including a constructive witness of
65-
their generic non-commutation.
66-
67-
**Realizability.** The full characterization of which ultrametrics are
68-
realizable by sibling-uniform radix laws (Theorem 43): an ultrametric is
69-
realizable **iff** every open ball is a prefix cylinder and every cylinder has
70-
canonical diameter — proven in both directions, with the two conditions doing
71-
provably separate work (the first pins the tree, the second pins the gauge)
21+
## The idea
22+
23+
You already use a number system whose base changes with position: 60 seconds
24+
to a minute, 60 minutes to an hour, 24 hours to a day. That is *mixed radix*,
25+
and it is classical — fix a list of bases `b₀, b₁, b₂, …` and the place value
26+
at position `m` is the running product `Bₘ = b₀·b₁ ⋯ bₘ₋₁`.
27+
28+
This corpus asks what number representation becomes when that list is replaced
29+
by a **function**. The central object is the *radix law*
30+
31+
```
32+
b : prefix ⟶ {2, 3, 4, …}
33+
```
34+
35+
— the base at each position is *computed*: from the position, from the digits
36+
already written, from an external context, or from the live state of another
37+
number line entirely. The digit space stops being a grid and becomes a rooted
38+
tree whose branching factor varies node by node; the "numbers" are its paths.
39+
40+
A surprising amount of classical structure survives the generalization: the
41+
bijection with ℕ, the carry dynamics of `+1` (the odometer), the prefix
42+
ultrametric in which balls are exactly cylinders. The subject of the corpus is
43+
*where each survival ends* — and the boundary is in every case proven, not
44+
asserted. The specification, [`docs/fdrs.md`](docs/fdrs.md), has grown through
45+
fourteen phases of numbered definitions, theorems, and propositions, and is
46+
machine-checked item by item in Lean 4 against
47+
[Mathlib](https://github.com/leanprover-community/mathlib4).
48+
49+
## Five results, as a sampler
50+
51+
Chosen for range; the [index](docs/fdrs-index.md) maps every numbered item to
52+
its proof.
53+
54+
**Which geometries can be numbered.** An ultrametric space is realizable by a
55+
sibling-uniform radix law **iff** every open ball is a prefix cylinder and
56+
every cylinder has canonical diameter (Theorem 43, Phase 6) — both directions
57+
proven, and the two conditions do provably separate work: the first pins the
58+
tree, the second pins the gauge
7259
([`MetricRealizability.lean`](FdrsFormal/Modes/VariableRadix/Realizability/MetricRealizability.lean)).
7360

74-
**Certified emission engines (Phase 13).** Continued-fraction timelines where
75-
the gauge is generated rather than multiplied out, with Gosper-style
76-
homographic/bihomographic engines that emit a digit only when *every* possible
61+
**A digit is emitted only when it is forced.** On continued-fraction timelines
62+
(Phase 13) the gauge is generated rather than multiplied out, and Gosper-style
63+
homographic/bihomographic engines emit a digit only when *every* possible
7764
continuation of the unread input forces it — the four-corner order trap at the
78-
Archimedean place, the congruence trap at p-adic places, the admissibility
79-
trap on finite grammars. Exact integer ledgers, no floating point anywhere;
65+
Archimedean place, the congruence trap at p-adic places, the admissibility trap
66+
on finite grammars. Exact integer ledgers, no floating point anywhere;
8067
`√2·√2` emits nothing, honestly.
8168

82-
**The adelic complex.** Heterogeneous place-engines under one scheduler with
83-
proven confluence; the product formula on ℚˣ in exact arithmetic; the
84-
finite-precision gauge bound; and the rigidity boundary — an FDRS gauge
85-
reproduces a p-adic place value **iff** its base is constantly p, so there are
86-
no synthetic places on ℚ. A function-field keystone stakes the genuinely
87-
synthetic instance ([`docs/function-field/`](docs/function-field/)).
88-
89-
**The synthetic place complex (Phase 14).** What survives when number lines
90-
couple: any positive monotone prefix gauge induces an ultrametric with
91-
ball = cylinder (both prior corpus metrics become instances); coupling
92-
generically destroys the odometer while the geometry survives; conservation
93-
migrates from product formulas — impossible for genuinely coupled systems, by
94-
a machine-checked separability no-go — to interface balance laws
69+
**You cannot counterfeit a prime.** Heterogeneous place-engines run under one
70+
scheduler with proven confluence, and the product formula on ℚˣ holds in exact
71+
arithmetic — but an FDRS gauge reproduces a p-adic place value **iff** its base
72+
is constantly p. There are no synthetic places on ℚ; a function-field keystone
73+
stakes the genuinely synthetic instance
74+
([`docs/function-field/`](docs/function-field/)).
75+
76+
**When number lines couple, they stop being numbers — lawfully.** Coupling
77+
generically destroys the odometer while the geometry survives (Phase 14).
78+
Conservation migrates from product formulas — impossible for genuinely coupled
79+
systems, by a machine-checked separability no-go — to interface balance laws
9580
(`issued = consumed + pending`, proven for arbitrary coupling in any
96-
commutative monoid of carries); no scalar gauge can metrize a concurrent
97-
network (proven), forcing the observer-glued construction; and "bigger digit"
98-
exists iff every coupling loop has trivial holonomy — with a verified
99-
three-digit Penrose staircase on the other side of the boundary. Together with
100-
ragged fibers and bilateral coupling, that gives three independent,
101-
machine-checked obstructions separating coupled radix complexes from number
102-
systems.
103-
104-
**The SU7 network machine (Phase 14, §14.12–14.13).** The coupled radix network
105-
as a verified abstract machine: a three-clause firing rule whose fan-out
106-
lawfulness is a guard (declared carry mass partitioned exactly across transport
107-
edges), whose well-formedness *is* dependency grading (Phase 8's deadlock
108-
certificate reused verbatim), with per-edge balance laws, a decidable
109-
couplability certificate (witnessed live and blocked), per-node emission traps
110-
transported unchanged, a conditional Kahn diamond whose independence
111-
side-condition is **derived** from the capacity-one latency discipline rather
112-
than assumed, and liveness in honest factored form. A concretization bridge
113-
proves the Phase-8 timeline-graph layer is an instance of this machine (a
114-
timeline graph IS a network shape; time-ordering IS grading; queue registers
115-
balance at every capacity).
116-
117-
**Applications (§14.14).** The corpus vocabulary load-bearing in production
118-
arithmetic: GF(2^255 − 19) under Ed25519 read as a ten-digit variable-radix
119-
ring — carries are ledger-balanced redistributions, the wrap has holonomy 19
120-
(a digit ring on the frustrated side of the grading dichotomy), and the
121-
eleven-carry schedule provably restores the digit bound, licensing the Rust
122-
kernel's lazy reduction
81+
commutative monoid of carries). No scalar gauge can metrize a concurrent
82+
network, forcing the observer-glued construction; and "bigger digit" exists
83+
**iff** every coupling loop has trivial holonomy, with a verified three-digit
84+
Penrose staircase on the other side of the boundary. Together with ragged
85+
fibers and bilateral coupling, three independent machine-checked obstructions
86+
separate coupled radix complexes from number systems.
87+
88+
**The vocabulary is load-bearing in production arithmetic.** GF(2²⁵⁵ − 19)
89+
under Ed25519, read as a ten-digit variable-radix ring: carries are
90+
ledger-balanced redistributions, the wrap has holonomy 19 — a digit ring on the
91+
frustrated side of the grading dichotomy — and the eleven-carry schedule
92+
provably restores the digit bound, licensing the lazy reduction used in
93+
deployed Rust kernels
12394
([`Field25519Carry.lean`](FdrsFormal/Applications/Field25519Carry.lean)).
12495

125-
## Method
96+
Beyond the sampler: a discrete multiresolution analysis with a commutant
97+
theorem, the cylinder-measurability bridge between the additive and
98+
multiplicative filtrations, and a verified abstract machine for coupled radix
99+
networks (the SU7 arc, §14.12–14.13) whose firing rule, balance laws, Kahn
100+
determinacy, and liveness are all proven — with the Phase-8 timeline-graph
101+
layer shown to be an instance of it.
102+
103+
## How to trust it
104+
105+
The default `lake build` target compiles the entire tree — **zero axioms and
106+
zero sorries** — against Mathlib at the revision pinned in the manifest. The
107+
spec contains **523 numbered items** across the fourteen phases, and the
108+
correspondence between items and Lean proofs is maintained by tooling, not by
109+
prose:
110+
111+
```bash
112+
python3 scripts/fdrs-summary # live status: axioms, sorries, scaffolds, coverage
113+
```
114+
115+
At this writing the scanner matches 520 of the 523 items (99.4%) to proofs and
116+
names the residue explicitly — one open Phase-7 item and three scaffold
117+
declarations it flags as such. Numbers printed in documentation, including this
118+
file, are treated as stale by default; the scanner reads the live source.
119+
120+
House rules, as working practice:
126121

127122
- **Spec first.** `docs/fdrs.md` is the single source of truth; Lean modules
128123
cite the numbered items they prove, and an erratum is preferred over a
129124
silent fix when the spec is wrong.
130-
- **Ask the tooling, not the prose.** `python3 scripts/fdrs-summary` scans the
131-
live source for axioms, sorries, stubs, and per-phase coverage; numbers in
132-
documentation are treated as stale by default.
133-
- **Honest scope, as working practice.** Every module carries an honest-scope
134-
banner; design documents carry anti-confabulation ledgers; finite witnesses
135-
use kernel `decide` (never `native_decide`); classical results are cited as
136-
classical — the contribution is the connection and the verified artifact.
125+
- **Honest scope.** Every module carries an honest-scope banner; design
126+
documents carry anti-confabulation ledgers.
127+
- **Kernel `decide`.** Finite witnesses are checked by the kernel, never by
128+
`native_decide`.
129+
- **Classical is cited as classical.** The contribution is the connection and
130+
the verified artifact, not a claim of novelty over the ingredients.
131+
132+
## The fourteen phases
133+
134+
| Phase | Name | What lands there |
135+
|:--|:--|:--|
136+
| 1 | Foundations | Mixed-radix spaces; decode/encode bijections with ℕ; the Tick; the prefix ultrametric |
137+
| 2 | Mixed-Radix Complexes | Cylinders and filtration; block projections as conditional expectations; the Haar/contrast MRA; the commutant theorem |
138+
| 3 | Import Analytic Number Theory | Dirichlet convolution, characters, valuations; the cylinder-measurability bridge |
139+
| 4 | Integers as Programs | Computation primitives from ANT; the factorization lens |
140+
| 5 | Function-Defined Radices | The radix law; variable-radix trees; Tick with variable carry; no-infinite-carry conditions |
141+
| 6 | Custom Ultrametric Design | Radix engineering; the realizability criterion (Theorem 43) |
142+
| 7 | Context-Dependent Radix Systems | Radix laws that consult an external context or oracle |
143+
| 8 | Multi-Timeline Routing | Composition of timelines; the dependency-grading deadlock certificate; timing bounds |
144+
| 9 | Extended Base Support | Base-0 walls and base-1 wires; spatialized digits; the spatial thermometer |
145+
| 10 | Base-Zero Sea Dynamics | Deterministic substrate dynamics; the linear-chain bridge |
146+
| 11 | Digit-Conditional Signal Analysis | The projection algebra; the Fourier ceiling |
147+
| 12 | Unit Complement Structure | The complement `x ↦ 1 − x` as a uniform frame for the corpus's normalized quantities |
148+
| 13 | Generated Timelines | Continued-fraction gauges, generated rather than multiplied out; the certified Gosper emission engines |
149+
| 14 | The Synthetic Place Complex | Coupled radix networks: geometry, conservation, obstructions; the SU7 network machine; applications |
137150

138151
## Layout
139152

153+
```
154+
docs/ # the spec (fdrs.md), the item index, design records, notation
155+
FdrsFormal/ # the Lean corpus (tree below)
156+
scripts/ # maintenance tooling — fdrs-summary and the index builder
157+
data/ # generated: the item index (YAML) and per-phase item graphs
158+
explorations/ # small Python sketches; exploratory, non-evidentiary
159+
```
160+
140161
```
141162
FdrsFormal/
142163
├── Core/ # Radix sequences, bijections, finite/infinite spaces
@@ -162,14 +183,14 @@ FdrsFormal/
162183
# the SU7 network machine + Phase-8 bridge
163184
```
164185

165-
The default `lake build` target compiles the entire tree — every module above is
166-
imported (transitively) by the root module (wiring pass of 2026-07-12).
167-
168-
`FdrsFormal.lean` is the root module aggregating the development; `Main.lean`
169-
is a trivial executable entry point. Design records for the newer complexes
170-
live in [`docs/synthetic-place/`](docs/synthetic-place/) and
171-
[`docs/function-field/`](docs/function-field/); superseded design documents
172-
are archived under [`docs/archive/`](docs/archive/).
186+
`FdrsFormal.lean` is the root module aggregating the development, and every
187+
module above is imported (transitively) by it, so the default `lake build`
188+
compiles the whole tree. `Main.lean` is a trivial executable entry point. A
189+
generated module dependency graph lives at
190+
[`docs/dependency-graph.svg`](docs/dependency-graph.svg). Design records for
191+
the newer complexes are in [`docs/synthetic-place/`](docs/synthetic-place/) and
192+
[`docs/function-field/`](docs/function-field/); superseded design documents are
193+
archived under [`docs/archive/`](docs/archive/).
173194

174195
## Building
175196

@@ -184,8 +205,8 @@ lake build # the formalization
184205
python3 scripts/fdrs-summary # live status: axioms, sorries, coverage
185206
```
186207

187-
[`docs/TESTING.md`](docs/TESTING.md) covers the work-in-progress modules
188-
outside the default target; [`docs/GENERAL_CONTEXT.md`](docs/GENERAL_CONTEXT.md)
208+
[`docs/TESTING.md`](docs/TESTING.md) covers work-in-progress modules outside
209+
the default target; [`docs/GENERAL_CONTEXT.md`](docs/GENERAL_CONTEXT.md)
189210
documents the trust hierarchy of the generated metadata;
190211
[`docs/notation.md`](docs/notation.md) is the symbol reference extracted from
191212
live code.

0 commit comments

Comments
 (0)