BROWSER DEMO
600 multivectors.24 frames × 25 samples.
This page loads a versioned JSON scene that Lean generated and validated. It then runs the same local React/SVG component as the Lean InfoView. The browser does not compute Clifford products, apply rotors, resample the field, or interpolate frames.
Phone controls
Drag an empty part of the field to orbit.
Tap a sample to inspect its coefficients.
Tap grade 2 to show or hide plane values. Drag the timeline slider or tap Play.
Loading the Lean-generated scene…
The program beside the view
def fieldAt (θ : Float) (p : Vec3) :
MV R3 .full :=
mvSandwich (rotor θ) (baseField p)
def stageScene :
Except String MultivectorFieldProps :=
defaultScene stageGrid 24
#eval stageScene.bind
MultivectorFieldProps.summary
#html sceneResultHtml stageScene
Compact excerpts from the real declarations. The links open their full context.
inductive Parity where
| even | odd | full
structure MV {n : ℕ}
(sig : Signature n) (p : Parity) where
private mk ::
coeffs : DataArray
instance instHMulMV :
HMul (MV sig p1) (MV sig p2)
(MV sig (p1 * p2)) where
hMul := mulDirectSignature 3 carries the metric. Parity records which grades may occur. DataArray is Lean’s contiguous FloatArray. Thus MV R3 .full stores 8 coefficients; MV R3 .even stores 4.
Two points to explain live
θ=0, p=0 · only a vectorF₀(0) = 0.35e₁ + 0.25e₃
Both p*v and τI vanish.
θ=0, p=e₁ · scalar + vector + planee₁e₁=1 · e₁e₂=e₁₂
p*v = 0.35 + e₁₂ + 0.25e₁₃. The repeated direction makes the scalar; the new direction makes the plane.
The slider can live in the editor.
This demo’s slider selects one of 24 Lean-computed frames. A custom InfoView slider could send θ through RPC and reevaluate fieldAt θ live. I precomputed the frames for stage reliability.
JavaScript is disabled. Open the Lean-generated static SVG fallback.
OPTIONAL SIDE LAB · BROWSER-SIDE
An eigenvector makes no new plane.
A = diag(2, ½)v(φ) = cos φ e₁ + sin φ e₂v ∧ Av = −¾ sin(2φ) e₁₂
1 · Eigenvectors
Av is parallel to v only on an eigenline.
e₁ · λ=2 e₂ · λ=½
v Av
2 · The multivector test
v ∧ Av is the oriented plane swept out by the two vectors. It is zero exactly on an eigenline.
This side lab evaluates the displayed elementary formulas in the browser. The multivector field above remains the Lean-generated computation.
