VR-Algebra is the eighth work of the cycle developing the VR programme (Reznik 2026, preprints VR. A Formal System, VR-Numbers, VR-Sets, VR-Forms, VR-Audit, VR-Sets-ZFA, VR-Apparatus). It applies the VR-Apparatus framework — the operational tracking discipline formalised as predicates carrying construction witnesses — to the standard algebraic hierarchy: additive groups, rings, multiplicative groups, fields, and modules. Five operational typeclasses are constructed as Lean 4 layers over the corresponding mathlib structures, each registering a predicate on its carrier and closure axioms for its operations. The construction reuses the VR-Apparatus identity (PredicateOperationality) without modification across five algebraic structures; in the case of modules the apparatus instance is literally inherited from the underlying operational additive group without a new registration. Substantive Mode A theorems are proved for all standard operations (closure under addition, multiplication, inverse, scalar multiplication, integer powers). One substantive Mode B audit is conducted — the image of an operational subgroup under an operational homomorphism is an operational subgroup — whose proof consists of a single inference step over the apparatus, contrasting structurally with the analytical Mode B audit of VR-Audit (Hahn-Banach). The cycle is logically constructive with two documented structural exceptions located in field-inverse reasoning; these exceptions trace to mathlib's encoding of `Inv K` resolution and are recorded as Finding A15/A16 with detailed reconnaissance. The recognition discipline pattern is observed in both removal (preemptive abstractions deleted) and introduction (justified abstractions added) forms, completing the bidirectional methodological signature anticipated in the VR-Apparatus formalisation. Twenty findings are catalogued (A0-A19) covering apparatus reuse, axiom hierarchy, recognition discipline, and engineering observations. Companion Lean formalisation. The Lean 4 code is at https://github.com/inventor1975/VRCycle, tag v1.12-vr-operational-algebra-v1.0.0, commit 5e8f8e0. 64 public objects across 8 files in the VRCycle/Algebra/ directory, 3,977 lines of Lean source, full axiom audit via #print axioms for every public object, zero sorry or admit. Unlike the prior seven works of the VR cycle, no companion Lean Zenodo record accompanies this preprint; the Lean code is cited by GitHub tag rather than DOI, simplifying the publication workflow without compromising reproducibility.
Vitaly Reznik (Tue,) studied this question.