Phi9 / research & engineering
Make the representation visible
Three small executable models of what a representation keeps, changes and loses.
Constructed mathematical demonstrations · no model training or external calls
Download the mechanics and invariant tests
Chapters 1–3 / information before computation
One total, two possible worlds
Both worlds contain ten counters. Move the split, then change the action. Does the total alone determine the new total?
World A
total 10 → 14
World B
total 10 → 17
Same retained total. Different next totals: 14 and 17.
Total closes under doubling both: z′ = 2z. Doubling only the left requires u as well: z′ = z + u. Identical splits agree trivially; they are not a test of two distinct hidden worlds.
Read the worked argument →Chapters 5–6 / coordinates are not a learned law
The same position can have a different future
For ṙ = s and ṡ = −r, the exact unit-frequency solution is (r,s) = (cos θ, −sin θ). Keeping position only merges opposite phases. Keep velocity and the direction becomes visible.
θ = 60° · position 0.500 · velocity −0.866
Writing c = r − is gives ċ = ic. This is an invertible coordinate change on the full pair, not compression or evidence of learned dynamics. Changing θ to 360° − θ keeps r and reverses s.
What does an imaginary coordinate buy?
Multiplication by i is the real matrix J = [[0,−1],[1,0]], with J² = −I. A quarter-turn is easier to write, but no new sensor information appears. Extending rational coefficients with √2 is a different operation: (a,b) represents a+b√2 and multiplication is (ac+2bd,ad+bc). These are established mathematical constructions, not new learning results.
Chapter 8 / specify the executable numbers
Equal algebra. Unequal execution.
Translate by +2²⁴, then by −2²⁴. Over exact integers the net map is identity. In IEEE-754 binary32, rounding an intermediate value can erase a coordinate.
Starting at 1: exact result 1; sequential binary32 returns 0, composed returns 1.
Math.fround applies binary32 rounding at each stated step. This browser fixture does not rerun Lean or Bend, prove compiler correctness or certify learned coefficients. The retained supplement reports the analogous F32 counterexample beside exact affine proofs.
Read the proof and roundoff boundary →From a demonstration to a research test
These models expose exact assumptions; they do not train a representation. Seed-conditioned flow, learned interaction fields and physical-agent prediction remain separate research directions requiring observed data and held-out consequences.
See a measured learning comparison · Return to runnable systems