T2.1 — State space and Euclid step
States are pairs : Nat x Nat with S>0. One Euclid step produces quotient k = floor(L/S) and next state .
Foreground
- Define State, quot, step.
- Exact integer world.
Underlayers
- Nat with well-founded order.
- Deterministic guarded rule.
Error Capsule
- Exact arithmetic (bigint).
Trace: Def(State), Def(quot), Def(step), Check(0 <= rem < S)
T2.2 — Termination measure
Measure m() = S. Each step strictly decreases m, so the process terminates.
Trace
- OpenGoal(G1)
- Refine: m(next) < m(cur)
- Solve: wf-induction
Layer S
- Property tests: gcd = last remainder.
T2.3 — Convergents from quotients
Define convergents p_n/q_n via recurrence on quotient list.
Trace
- Def(ConvRecurrence)
- Check(q_n > 0)
sim_spec
- Output (p_i,q_i) prefixes.
- Cache updates O(1).
T2.4 — Matrix cocycle
Define M(k) = [[k,1],[1,0]]. Product yields convergents: M(k0)...M(kn) = [[p_n,p_{n-1}],[q_n,q_{n-1}]].
Trace
- Def(M), Solve induction.
- Check(det = +/-1)
Layer E
- Store matrices as (a,b,c,d).
Layer S
- Invariant checks: ad-bc=+/-1.
T2.5 — Rational to real evaluation
Finite prefix evaluates to p_n/q_n. Infinite digits converge to a real limit.
Trace
- Def(eval_prefix)
- OpenGoal: convergence
Error Capsule
- Interval guard for floating input.
Layer S
- Interval digit extraction.
T2.6 — Error envelope
For irrational x: |x - p_n/q_n| < 1/q_n^2. Bound is explicit and cheap.
Trace
- Def(err_bound_n)
- Check(q_{n+1} > q_n)
Layer E
- Render error bands in UI.
Layer S
- Tighten with next digit when available.
T2.7 — Geometric overlay
Matrix products act on the projective line x -> (ax+b)/(cx+d), linking to modular geometry.
Trace
- Def(Mobius)
- Check(action composition)
Layer S
- Optional hyperbolic tiling renderer.
T2.8 — Lyapunov growth
Define lambda_n = (1/n) log ||M_0..M_n||. Growth rates encode stability.
Error Capsule
- Numeric: rounding + sampling CI.
Layer E
- Batch runs, cache by seed.
T2.9 — Constraint overlay
Impose digit constraints (bounded digits, DFA language). Induces subdynamics.
Trace
- Def(P), Def(AllowedPrefix)
Error Capsule
- Filtering bias vs automaton-guided generation.
Layer S
- Adjacency matrix entropy baseline.
T2.10 — Euclid trace vs Gauss trace
Two digit sources coincide for rationals. This is a regression suite anchor.
Trace
- Def(embed), Solve digit equality
Layer E
- Differential testing across implementations.
Layer S
- Millions of cases cheaply.
T2.11 — Artifact schema
Define a plate artifact record so UI + distributed compute align.
Trace
- Def(PlateArtifact)
- Check(hash stability)
Layer E
- Store in IndexedDB + blob store.
T2.12 — UX closure
Reference-following, semantic palette, motion grammar. UI events resolve to artifact fetches.
Trace
- Def(SemanticClasses)
- Def(MotionGrammar)
- Check(contrast)
Error Capsule
- Reduced motion + high contrast.
Layer S
- Semantic search returns citations.
Semantic Color Legend
Type / Universe
- Left gutter marker, minimal chroma.
Proof Actions
- Def: pill outline
- OpenGoal: hollow diamond
- Refine: split chevron
- Check: tick
- Solve: solid diamond
Error Capsule
- Theorem-backed: shield
- Empirical: wave bracket
- Unknown: hazard
DSL Flow — Trace -> Artifact -> UI
Each plate is encoded in a trace DSL, compiled into a PlateArtifact (EDN), then rendered into the UI. This keeps proofs, sims, and surfaces aligned.
Trace DSL
Def(State, Nat x Nat)
Def(quot, -> floor(L/S))
Def(step, -> )
Check(bound, 0 <= rem < S)
Artifact (EDN)
{:plate/id "t2-1"
:defs ["State" "quot" "step"]
:trace [[:Def "State"] [:Def "quot"] [:Check "bound"]]
:delta "Introduced State, quot, step"
:sim_spec {:input "L,S" :output "k,next"}}
Artifact (JSON)
{
"plate_id": "t2-1",
"defs": ["State","quot","step"],
"trace": ["Def(State)","Def(quot)","Check(bound)"],
"delta": "Introduced State, quot, step",
"sim_spec": {"input": "L,S", "output": "k,next"}
}
UI Bindings
renderPlate(artifact)
-> section header
-> trace timeline
-> sim panel
-> error capsule
-> layer E/S callouts