# Recorded Grassmann rotor field

This package contains four consumer assets: `rotor-field.json`,
`rotor-field.schema.json`, `manifest.json`, and this README. It contains no
Grassmann source, adapter source, local paths, transcripts, or execution logs.

The fixture was computed by the Grassmann Lean 4 port at source commit
`48f02068f9e9f6277271d1e4f439d8be3f823563`, using
`leanprover/lean4:v4.35.0-rc3`. Its source-tree identity, source-module hashes,
generator hashes, asset size, and content hash are recorded in `manifest.json`.
The source library reports AGPL-3.0-or-later. This task does not publish that
source. The fixture records mathematical inputs and outputs.

## Load the data

The schema identifier is `grassmann-rotor-field/v1`. Each frame contains samples:

```text
frames[i].samples[j].position = [x,y,z]
frames[i].samples[j].vector   = [vx,vy,vz]
```

`vector_exact` contains three normalized `{num: String, den: String}` rational
pairs with positive denominators. Numeric vectors are binary64 display
approximations of those exact Grassmann outputs. Positions are integer-valued.
`result_kind="Chain"` and `result_grade=1` record the actual sandwich result.

There are nine discrete rotor frames, each containing 27 positions on the grid
`[-1,0,1]^3`: 243 samples total. Samples are ordered x outermost, y middle,
z innermost. The input vector is `(x,y,z)` at position `(x,y,z)`. Positions stay
fixed while vectors rotate. The origin has a zero vector and needs no arrow.

## Coordinates and controls

Use right-handed axes e1=+X, e2=+Y, e3=+Z with Euclidean metric diag(+1,+1,+1).
Blade masks are e1=1, e2=2, e3=4, e12=3; e12=e1*e2 and e12 squared is -1.

The exact parameter values are:

```text
t = [-1,-3/4,-1/2,-1/4,0,1/4,1/2,3/4,1]
```

The actual operation is `Grassmann.TA.sandwich(v,R)`, with
`d=1+t*t`, `c=(1-t*t)/d`, `s=2*t/d`, and `R=c+s*e12`.
The existing Grassmann convention is `reverse(R)*v*involute(R)`; for this even
rotor it is `reverse(R)*v*R`. Positive t rotates +X toward +Y. The coordinate
formula independently checked for every sample is:

```text
C=c*c-s*s; S=2*c*s
vx=C*x-S*y; vy=S*x+C*y; vz=z
```

The angle is `theta=4*atan(t)`, from -pi to pi. The supplied approximate angle
is for labels; frame spacing is not uniform in angle. At t=1/2, +X becomes
`[-7/25,24/25,0]`. At t=1 it becomes `[-1,0,0]`. The first and last frames have
identical vectors, forming endpoints of a full turn.

Use `frames[].index` or `frames[].t` for stepped controls. These are recorded
Grassmann results, not live Lean execution in a browser or native app.
Interpolation and replay timing are renderer choices; interpolated results
are approximations and linear vector interpolation need not preserve norms.
There is no physical time variable, fluid solver, or continuous field engine.
This dataset is separate from any renderer's larger analytic grid or time domain.

## Evidence and integrity

All 243 samples passed exact unit-rotor, matrix, squared-norm, grade1-purity,
and actual public-product checks. The sandwich/public-product check compares
all eight blade coefficients, not raw constructor equality. Three finite
orientation certificates were checked by Lean's kernel, using only standard
propext, Classical.choice, and Quot.sound. Repeated actual Lean generation was
byte-identical. Independent verification rejected changes to the rotation
sign, axis order, grade, and display coordinate.

These are sample checks and finite kernel certificates, not a theorem covering
all rotors, fields, containers, or Float algebra. The JSON Schema documents the
structural contract; exact numerical checks were performed by the generator.

`rotor-field.json` is 47,723 bytes and has SHA256:

```text
97fe4133aaf86c3666f02817518e3e36e27927d513da201be503ad88da7e1090
```

Both renderers may load the same JSON file directly; neither needs to build
Grassmann. Preserve the source pin and recorded-evidence label when presenting
the fixture. The package is an integration asset, not a source-code release.