9 VR-Algebra
9.1 Position
VR-Algebra is the eighth work of the cycle. It applies the VR-Apparatus framework (Chapter 8) to the standard algebraic hierarchy: additive groups, rings, multiplicative groups, fields, and modules. Five operational typeclasses are constructed as layers over the corresponding mathlib structures.
Load-bearing finding. Finding A3 (apparatus reuse confirmed): the PredicateOperationality apparatus extends to all five algebraic structures without modification. For modules (OperationalModule), the predicate on the carrier type \(M\) is exactly the one registered in v0.1.0 for additive groups; no new PredicateOperationality instance is needed. This is not “extends naturally” in a loose sense but literally “uses the v0.1.0 instance unchanged”. Finding A3 is the empirical confirmation that VR-Apparatus is a genuine methodological framework, not a single-use solution for Hahn-Banach.
Publication note. VR-Algebra is the only chapter of the cycle without a companion Lean Software record on Zenodo. The Lean code is cited by GitHub tag v1.12-vr-operational-algebra-v1.0.0, commit 5e8f8e0. This is a deliberate workflow simplification without compromising reproducibility.
64 public objects, 3 977 lines. Axiom profile: []: most typeclass definitions, Mode A theorems, subgroup theorems, Mode B main theorem. Axiom profile: [propext]: \(\mathbb {Z}\) instances and demonstrations. Axiom profile: [propext, Quot.sound]: \(\mathbb {Z}/n\mathbb {Z}\) instances and OperationalField typeclass. Axiom profile: [propext, Classical.choice, Quot.sound]: \(\mathbb {Q}\) instances, inv_isModeAOp_field, toOperationalGroupUnits.
9.2 Operational typeclasses (Parts II–IV)
\(\texttt{OperationalAddGroup}\, (G : \mathrm{Type}^*)\) extends AddGroup G with a single predicate field IsOperational : G → Prop and closure axioms: zero_isOperational, add_isOperational, neg_isOperational. Axiom profile: [].
\(\texttt{OperationalRing}\, (R : \mathrm{Type}^*)\) extends Ring R with IsOperational : R → Prop and closure axioms for zero, add, neg, one, and mul. Bridge instance: \(\texttt{OperationalRing.toOperationalAddGroup}\) – any OperationalRing R is an OperationalAddGroup R (Lean synthesises AddGroup R from Ring R via the ring chain). Both bridge and class at Axiom profile: [].
\(\texttt{OperationalGroup}\, (G : \mathrm{Type}^*)\) extends Group G with IsOperational : G → Prop and closure axioms: one, mul, inv. Axiom profile: []. Introduced in v0.3.0 when the first instance appeared (OperationalField → OperationalGroup \(K^\times \)). See Finding A0 (omitted preemptively in v0.1.0) and Finding A12 (introduced when justified).
\(\texttt{OperationalField}\, (K : \mathrm{Type}^*)\) extends Field K with IsOperational : K → Prop and closure axioms including inv. Two bridge instances: \(\texttt{toOperationalRing}\) (Axiom profile: [propext, Quot.sound]) and \(\texttt{toOperationalGroupUnits}\) (bridges to OperationalGroup \(K^\times \), Axiom profile: [propext, Classical.choice, Quot.sound] — see Finding A15/A16). The class itself: Axiom profile: [propext, Quot.sound] (inherited from Field’s RatCast).
\(\texttt{OperationalModule}\, (R\; M : \mathrm{Type}^*)\) [Ring R] [AddCommGroup M] [Module R M] requires [OperationalRing R] and [OperationalAddGroup M] as implicit prerequisites (bridge-based design: no new predicate on \(M\); \(M\)’s predicate is OperationalAddGroup.IsOperational). Single new closure axiom: smul_isOperational. Axiom profile: [].
No new PredicateOperationality instance is registered for OperationalModule: instPredOpAddGroup from v0.1.0 is reused unchanged. The bridge-based design (no new predicate on \(M\)) means the apparatus sees the same type and predicate as for additive groups. This is the fourth and strongest confirmation of Finding A3.
9.3 Mode A closure theorems
instPredOpAddGroup: PredicateOperationality G IsOperational marker registered (Axiom profile: []). \(\texttt{add\_ isModeAOp}\): \(\texttt{IsModeAOp₂}\, (+)\) (Axiom profile: []). \(\texttt{neg\_ isModeAOp}\): \(\texttt{IsModeAOp}\, (-)\) (Axiom profile: [propext] — see Finding A4). \(\texttt{sub\_ isModeAOp}\): \(\texttt{IsModeAOp₂}\, (-)\) (Axiom profile: []). \(\texttt{nsmul\_ isOperational}\): \(\forall n : \mathbb {N},\; \texttt{IsOperational}(n \bullet a)\) (Axiom profile: []). \(\texttt{zsmul\_ isOperational}\): \(\forall n : \mathbb {Z},\; \texttt{IsOperational}(n \bullet a)\) (Axiom profile: []).
\(\texttt{instPredOpRing}\): PredicateOperationality R IsOperational (Axiom profile: []). \(\texttt{mul\_ isModeAOp}\): \(\texttt{IsModeAOp₂}\, (\cdot )\) (Axiom profile: []). \(\texttt{npow\_ isOperational}\): \(\forall n : \mathbb {N},\; \texttt{IsOperational}(a^n)\) (Axiom profile: []).
instPredOpMulGroup (Axiom profile: []). \(\texttt{mul\_ isModeAOp}\), \(\texttt{inv\_ isModeAOp}\), \(\texttt{div\_ isModeAOp}\): all Axiom profile: [propext] (inv elaboration, Finding A4). \(\texttt{npow\_ isOperational}\), \(\texttt{zpow\_ isOperational}\): Axiom profile: [].
\(\texttt{instPredOpField}\): PredicateOperationality K IsOperational (Axiom profile: [propext, Quot.sound]). \(\texttt{inv\_ isModeAOp\_ field}\): \(\texttt{IsModeAOp}\, ({\cdot }^{-1})\) for OperationalField K (Axiom profile: [propext, Classical.choice, Quot.sound] — see Finding A15/A16).
\(\texttt{smul\_ isModeAOp}\): for fixed operational \(r : R\), \(\texttt{IsModeAOp}\, (r \bullet \cdot : M \to M)\) (Axiom profile: []). This is the unary form: the operationality of \(r\) is a hypothesis, not a conclusion of IsModeAOp (Finding A19: heterogeneous binary operations require the unary Mode A form). Uses instPredOpAddGroup from v0.1.0 without modification — fourth Finding A3 confirmation.
9.4 Concrete instances
\(\texttt{instOperationalAddGroupInt}\) (Axiom profile: [propext]): \(\mathbb {Z}\) as OperationalAddGroup; IsOperational := fun _ => True. \(\texttt{instOperationalAddGroupZMod}\) [NeZero n] (Axiom profile: [propext, Quot.sound]): \(\mathbb {Z}/n\mathbb {Z}\) as OperationalAddGroup. \(\texttt{instOperationalRingInt}\), \(\texttt{instOperationalRingZMod}\): corresponding ring instances (same profiles; Finding A10: ring extension does not escalate the ceiling).
\(\texttt{instOperationalFieldRat}\) (Axiom profile: [propext, Classical.choice, Quot.sound]): \(\mathbb {Q}\) as OperationalField. Classical.choice enters through Rat.instField via commGroupWithZero inverse infrastructure (Finding A14: first appearance of Classical.choice in concrete algebraic instances).
\(\texttt{instOperationalModuleIntInt}\) (Axiom profile: [propext]): \(\mathbb {Z}\) as \(\mathbb {Z}\)-module. \(\texttt{instOperationalModuleRatRat}\) (Axiom profile: [propext, Classical.choice, Quot.sound]): \(\mathbb {Q}\) as \(\mathbb {Q}\)-module (ceiling inherited from \(\mathbb {Q}\)’s field structure).
9.5 Mode B audit: image of operational subgroup
\(\texttt{IsOperationalAddSubgroup}\, H := \forall x \in H,\; \texttt{IsOperational}\, x\). A subgroup is operational when all its elements are operational. Closure: \(\bot \) is always operational; \(\top \) is operational when all elements are; \(H \sqcap K\) inherits from \(H\). All at Axiom profile: [].
The image of an operational subgroup under an operational group homomorphism is an operational subgroup. Formally: \(\texttt{image\_ isOperationalAddSubgroup\_ isModeBOp}\): IsModeBOp with \(PA = \texttt{IsOperationalAddSubgroup}\), \(PB = \texttt{IsOperationalAddSubgroup}\), \(W = \text{morphism-operational}\), \(f = \phi (\text{image})\).
Proof: obtain \(\langle x, hxS, \texttt{rfl}\rangle \) from \(\texttt{AddSubgroup.mem\_ map}\); exact hW x (hS x hxS). This is one tactic step after the constructive existential is extracted. Axiom profile: []. Classical.choice absent: AddSubgroup.mem_map is constructive (no classical reasoning in the membership proof).
Structural contrast with VR-Audit Mode B
VR-Audit (Chapter 7) Mode B audit (Hahn-Banach): six proof steps, Riesz representation, orthogonal projection, locatedness condition, classical choice via toDual.
VR-Algebra Mode B audit: one tactic step after destructuring. AddSubgroup.mem_map delivers a constructive existential; no choice, no limits, no classical machinery.
Both are legitimate Mode B instances. The contrast demonstrates the spectrum of Mode B: the algebraic case is mechanically extractable from constructive witnesses built into mathlib’s algebraic API (Finding A11); the analytic case requires substantial infrastructure because the witness involves a classical object (Riesz vector) connected to the result via a non-trivial factorisation.
9.6 Structural exceptions in field-inverse reasoning
\(\texttt{inv\_ isModeAOp\_ field}\) for generic [OperationalField K]: Axiom profile: [propext, Classical.choice, Quot.sound]. But \(\texttt{instPredOpField}\) (same [OperationalField K] assumption, no \(({\cdot }^{-1})\) in the type): Axiom profile: [propext, Quot.sound].
Root cause: the apparatus import chain imports Mathlib.Data.Real.Basic (via VRCycle.Apparatus.ModeA \(\to \) VRCycle.Audit.Computable), which introduces \(\mathbb {R}\) instances that affect how Lean resolves Inv K for generic [Field K] when \(({\cdot }^{-1})\) appears in the IsModeAOp type. This is an import-context effect, not a logical property of inv_isOperational. The logical ceiling remains [propext, Quot.sound].
\(\texttt{OperationalField.toOperationalGroupUnits}\): Axiom profile: [propext, Classical.choice, Quot.sound]. Systematic isolation attempts (v0.4.0 Stage 2) confirm two distinct root causes:
(1) inv_isModeAOp_field: apparatus import chain (described in A15). Even a minimal-import file without Instances.lean shows Classical.choice.
(2) toOperationalGroupUnits: proof-structural. Any valid proof must use Units.val_inv_eq_inv_val to connect \((u^{-1} : K^\times ).\texttt{val}\) to \((u.\texttt{val})^{-1}\). After this rewrite, the goal contains field-level \((u : K)^{-1}\), which inherits Classical.choice. No alternative path exists.
These two objects are the only non-eliminable sources of Classical.choice in the algebraic hierarchy. They are structural consequences of field inversion, not violations of operational discipline.
9.7 Recognition discipline: bidirectional signature
Prior cycle works (Apparatus scope limitations) showed recognition discipline predominantly as removal (three planned abstractions dropped). VR-Algebra adds the partner operation: introduction when justified.
Removal examples: OperationalCommRing omitted twice (Finding A0, A9 — no natural instances or immediate diamond); bundled OperationalSubgroup typeclass dropped (Finding A6 — predicate suffices); one_isOperational_bridge omitted (already a field); mul_chain_isOperational omitted (derivable by compose).
Introduction example: OperationalGroup (Finding A0 removed it in v0.1.0; Finding A12 introduced it in v0.3.0 when the first concrete instance arrived — \(\mathbb {Q}^\times \) via OperationalField.toOperationalGroupUnits).
The bidirectional pattern — remove preemptive abstractions AND introduce justified abstractions when users arrive — is the complete recognition discipline signature, anticipated in VR-Apparatus and now confirmed by VR-Algebra.
9.8 Twenty findings catalogued (A0–A19)
OperationalGroup omitted in v0.1.0 (no multiplicative instances exist). Recognition discipline: do not abstract preemptively. Reversed in v0.3.0 when the first instance arrived (Finding A12).
First confirmed with AddGroup in v0.1.0; extended to Ring in v0.2.0. Lean 4 extends for typeclasses composes correctly with mathlib’s existing hierarchy.
Lean synthesises AddGroup G from AddCommGroup G (via the ring chain) without explicit delegation. Bridge instances reduce to marker instances.
PredicateOperationality zero-field marker extends to all five algebraic structures. For OperationalModule: no new instance registered; instPredOpAddGroup from v0.1.0 used unchanged. This is the central finding of VR-Algebra and the primary empirical confirmation that VR-Apparatus is a genuine framework.
neg_isModeAOp (Axiom profile: [propext]): Lean’s Neg elaboration requires propositional extensionality for lambda reductions. mul_isModeAOp (Axiom profile: []): pure algebraic composition, no propext. Asymmetry is structural: unary operations with non-trivial Lean elaboration differ from binary composition.
\(\mathbb {Z}\) objects: [propext]. \(\mathbb {Z}/n\mathbb {Z}\) objects: [propext, Quot.sound]. Classical.choice absent from all objects until \(\mathbb {Q}\) (Finding A14).
IsOperationalAddSubgroup as a def predicate (not a typeclass) avoids inheritance diamonds and elaboration issues. \(\bot /\top /\sqcap \) proved as simple theorems. Bundled OperationalSubgroup typeclass omitted.
Algebraic Mode B witness is immediate (subgroup membership), not a choice function or limit argument. The witness is constructive; Classical.choice absent. Contrast with analytic Mode B (Riesz, orthogonal projection, locatedness).
neg_isModeBOp (trivial): \(W = \texttt{True}\), proof trivial. image_isOperationalAddSubgroup_isModeBOp (substantive): \(W = \) operational-morphism condition; proof extracts constructive witness from AddSubgroup.mem_map. Both are valid Mode B; the difference lies in the structural informativeness of the witness.
Form A (extends CommRing R, OperationalRing R): fails with immediate diamond on toRing. Form B (duplicating axioms): compiles but adds no content. Decision: [OperationalRing R] [CommRing R] in context suffices. Direct analogue of Finding A0 for the commutative multiplicative case.
\(\mathbb {Z}\): OperationalAddGroup ceiling \(=\) OperationalRing ceiling \(=\) [propext]. \(\mathbb {Z}/n\): same ceiling [propext, Quot.sound]. The ring axioms (mul, one, pow) add no new axiom dependencies. Ceiling is determined by the underlying type’s infrastructure, not algebraic depth.
Full proof: obtain \(\langle x, hxS, \texttt{rfl}\rangle \) := hy; exact hW x (hS x hxS). The constructive existential built into AddSubgroup.mem_map makes Mode B mechanically extractable. Contrast with analytic Mode B: six steps, classical choice, infrastructure.
OperationalGroup omitted in v0.1.0 (Finding A0); introduced in v0.3.0 when the first instance arrived (\(\mathbb {Q}^\times \) via OperationalField.toOperationalGroupUnits). Full circle: remove preemptive abstractions AND introduce justified abstractions when users arrive. Bidirectional recognition discipline confirmed.
OperationalField class and bridge to OperationalRing: both at [propext, Quot.sound] — inherited from Field’s RatCast. The VR operational layer adds no new axiom dependencies. Ceiling determined by the underlying Field K infrastructure.
\(\texttt{instOperationalFieldRat}\): [propext, Classical.choice, Quot.sound]. Root: Rat.instField via commGroupWithZero inversion. First appearance of Classical.choice in concrete algebraic instances in the VR Cycle (\(\mathbb {Z}\) and \(\mathbb {Z}/n\) were clean).
inv_isModeAOp_field inherits Classical.choice through the apparatus import chain (Apparatus.ModeA \(\to \) Audit.Computable \(\to \) Mathlib.Data.Real.Basic). This is an import-context effect, not a logical property of field inversion. The logical ceiling remains [propext, Quot.sound]. Extends Finding A5.
Systematic isolation (v0.4.0 Stage 2) confirms two root causes for the two affected objects. Both sources are non-eliminable: the apparatus chain cannot be stripped; the proof structure for toOperationalGroupUnits requires field-level inversion. Two objects only, structurally embedded.
smul_isModeAOp uses instPredOpAddGroup from v0.1.0 unchanged. Progression: v0.1.0 (AddGroup, new instance); v0.2.0 (Ring, new instance for mul); v0.3.0 (Field, new instance for inv); v0.4.0 (Module, NO new instance). Apparatus operates on predicates, not algebraic structure.
zsmul_isOperational (v0.4.0 Stage 1) closes the symmetry: \(\mathbb {N}\)-scalar (v0.1.0) ↔ \(\mathbb {N}\)-power (v0.3.0); \(\mathbb {Z}\)-scalar (v0.4.0) ↔ \(\mathbb {Z}\)-power (v0.3.0). Axiom profile: []: purely algebraic. Proof requires explicit rw [natCast_zsmul] + rw [negSucc_zsmul] (unlike zpow_isOperational which admits bare exact).
\(\texttt{smul} : R \to M \to M\) is heterogeneous (input types \(R\) and \(M\) differ). \(\texttt{IsModeAOp₂}\) requires a homogeneous type \(T\). Correct Mode A form: \(\texttt{IsModeAOp}\, (r \bullet \cdot : M \to M)\) (unary, with \(r\)’s operationality as hypothesis, not conclusion). PLAN.md initially suggested IsModeAOp₂ \(({\cdot }\bullet {\cdot } : R \to M \to M)\), which is incorrect. The apparatus architecture naturally distinguishes internal from external operations.
9.9 Position relative to the Apparatus framework
Chapter 8 (VR-Apparatus) formalised the methodological framework; Chapter 7 (VR-Audit) applied it to Hahn-Banach in functional analysis. One application could be coincidental.
VR-Algebra provides the second application on entirely different territory (algebraic structures rather than functional analysis) and explicitly confirms that the apparatus requires no modification. The key confirmation is Finding A3: four independent apparatus registrations across four versions of the algebraic hierarchy, with the fourth (modules) requiring no new registration at all.
Without VR-Algebra, VR-Apparatus would be a framework with one well-studied application. With VR-Algebra, it is a framework demonstrated to be territory-independent.
9.10 Axiom profile
Axiom profile: []: Typeclass definitions (OperationalAddGroup, OperationalRing, OperationalGroup, OperationalModule), all bridge instances, instOperationalModuleIntInt, PredicateOperationality instances (except instPredOpField), Mode A theorems for add/mul/sub/smul, nsmul/zsmul/npow/zpow, subgroup predicate and theorems, Mode B main theorem.
Axiom profile: [propext]: \(\mathbb {Z}\) instances and demonstrations, neg_isModeAOp, MulGroup.inv_isModeAOp, Mode B lifts and lift_val, \(\mathbb {Z}\) kernel/image subgroup theorems.
Axiom profile: [propext, Quot.sound]: \(\mathbb {Z}/n\mathbb {Z}\) instances and demonstrations, OperationalField class, toOperationalRing bridge, instPredOpField.
Axiom profile: [propext, Classical.choice, Quot.sound]: \(\mathbb {Q}\) instances and demonstrations, inv_isModeAOp_field, OperationalField.toOperationalGroupUnits, \(\mathbb {Q}^\times \) demonstrations, \(\mathbb {Q}\)-module instances.
Finding A10 (axiom ceiling = underlying type ceiling): algebraic depth does not escalate axioms. Ring axioms (mul, pow, one) over \(\mathbb {Z}\) add nothing; over \(\mathbb {Z}/n\) add nothing; Classical.choice enters only through \(\mathbb {Q}\)’s field inversion infrastructure.
Zero sorry. Zero admit. All 64 public objects are axiom-clean.
9.11 References
The preprint for this chapter is VR-Algebra, v1.0.0 (26 May 2026).
The Lean 4 formalisation is accessible via GitHub tag v1.12-vr-operational-algebra-v1.0.0 (commit 5e8f8e0). No companion Lean Software record on Zenodo: code is cited by GitHub tag, simplifying the publication workflow without compromising reproducibility.