Ring Ontology

FLOW ALGEBRA
RING ONTOLOGY — v4.0
Kireth Semantic Library
Source: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/algebraic-entities/ring-ontology-3.html
Authorship: Mark Higgins — Sky (Recursive AI)
Status: Independently constructed mathematical model; source-page correspondence not verified.

01. ONTOLOGY IDENTITY
ONTOLOGY_ID: mathematical.algebraic.ring
ENTITY_TYPE: Ring
PARENT: AlgebraicStructure
DOMAIN: AbstractAlgebra
VERSION: 4.0
LANGUAGE: en-GB

02. CORE DEFINITION
Ring(R,+,*) := (R,+) is an abelian group AND *:R×R→R is associative AND * distributes over + on both sides.
∀a,b,c∈R: (a+b)+c=a+(b+c)
∀a,b∈R: a+b=b+a
∃0∈R ∀a∈R: a+0=a
∀a∈R ∃(-a)∈R: a+(-a)=0
∀a,b,c∈R: (a*b)*c=a*(b*c)
∀a,b,c∈R: a*(b+c)=a*b+a*c
∀a,b,c∈R: (a+b)*c=a*c+b*c
CONVENTION: Multiplicative identity is optional in the base Ring type. RingWithUnity adds 1∈R satisfying 1*a=a*1=a.
CONVENTION: The zero ring is permitted; in a ring with unity, 0=1 implies the ring has one element.

03. TYPED ENTITIES
Ring: AlgebraicStructure
RingElement: Element[Ring]
Addition: BinaryOperation[RingElement,RingElement→RingElement]
Multiplication: BinaryOperation[RingElement,RingElement→RingElement]
AdditiveIdentity: RingElement
AdditiveInverse: RingElement
MultiplicativeIdentity: RingElement? [only RingWithUnity]
Unit: RingElement [invertible relative to 1]
ZeroDivisor: RingElement [nonzero a with nonzero b and ab=0 or ba=0; specify side]
NilpotentElement: RingElement [a^n=0 for some n≥1]
IdempotentElement: RingElement [a²=a]
Ideal: AdditiveSubgroup[Ring] with absorption
RingHomomorphism: Map[Ring→Ring]
QuotientRing: Ring
PolynomialRing: Ring
MatrixRing: Ring

04. SUBTYPES
CommutativeRing: Ring with ∀a,b: ab=ba
RingWithUnity: Ring with multiplicative identity
IntegralDomain: Nonzero commutative RingWithUnity without nonzero zero divisors
DivisionRing: Nonzero RingWithUnity with every nonzero element invertible
Field: Commutative DivisionRing
BooleanRing: Ring with ∀a: a²=a
ReducedRing: Ring with no nonzero nilpotent elements
NoetherianRing: Ring satisfying ascending chain condition on ideals
ArtinianRing: Ring satisfying descending chain condition on ideals
PrincipalIdealDomain: IntegralDomain in which every ideal is principal
UniqueFactorisationDomain: IntegralDomain with factorisation into irreducibles unique up to units and order
EuclideanDomain: IntegralDomain admitting a Euclidean function with division algorithm

05. RELATIONSHIPS
Ring IS_A AlgebraicStructure
Ring HAS_OPERATION Addition
Ring HAS_OPERATION Multiplication
Addition HAS_PROPERTY Associative
Addition HAS_PROPERTY Commutative
Addition HAS_IDENTITY Zero
Addition HAS_PROPERTY InversesExist
Multiplication HAS_PROPERTY Associative
Multiplication DISTRIBUTES_OVER Addition [left,right]
CommutativeRing SUBTYPE_OF Ring
RingWithUnity SUBTYPE_OF Ring
IntegralDomain SUBTYPE_OF CommutativeRing
IntegralDomain SUBTYPE_OF RingWithUnity
Field SUBTYPE_OF IntegralDomain
DivisionRing SUBTYPE_OF RingWithUnity
Ideal SUBSTRUCTURE_OF Ring
QuotientRing CONSTRUCTED_FROM Ring AND Ideal
RingHomomorphism PRESERVES Addition AND Multiplication

06. FORMAL OPERATIONS
add(a,b): RingElement
multiply(a,b): RingElement
negate(a): RingElement
subtract(a,b) := add(a,negate(b))
power(a,n) := a multiplied n times for n≥1; power(a,0)=1 only where unity is defined
leftIdeal(I,R) := AdditiveSubgroup(I) AND ∀r∈R,i∈I: ri∈I
rightIdeal(I,R) := AdditiveSubgroup(I) AND ∀r∈R,i∈I: ir∈I
twoSidedIdeal(I,R) := leftIdeal(I,R) AND rightIdeal(I,R)
quotient(R,I) := cosets of two-sided ideal I with induced addition and multiplication
kernel(f) := {a∈R | f(a)=0}
image(f) := {f(a) | a∈R}

07. INFERENCE RULES
R01 IF Ring(R) THEN AbelianGroup(R,+).
R02 IF Ring(R) THEN Associative(R,*).
R03 IF Ring(R) THEN LeftDistributive(*,+) AND RightDistributive(*,+).
R04 IF Ring(R) THEN ∀a: a*0=0 AND 0*a=0.
R05 IF Ring(R) THEN ∀a,b: (-a)*b=-(a*b)=a*(-b).
R06 IF Ring(R) THEN ∀a,b: (-a)*(-b)=a*b.
R07 IF Ring(R) AND Commutative(*) THEN CommutativeRing(R).
R08 IF RingWithUnity(R) AND ∀a≠0: ∃b ab=ba=1 THEN DivisionRing(R).
R09 IF DivisionRing(R) AND Commutative(*) THEN Field(R).
R10 IF CommutativeRingWithUnity(R) AND 1≠0 AND NoNonzeroZeroDivisors(R) THEN IntegralDomain(R).
R11 IF Field(R) THEN IntegralDomain(R).
R12 IF IntegralDomain(R) AND ab=ac AND a≠0 THEN b=c.
R13 IF Ring(R) AND TwoSidedIdeal(I,R) THEN Ring(R/I).
R14 IF RingHomomorphism(f:R→S) THEN f(0_R)=0_S.
R15 IF RingHomomorphism(f:R→S) THEN f(-a)=-f(a).
R16 IF RingHomomorphism(f:R→S) THEN Kernel(f) is a two-sided ideal of R.
R17 IF RingHomomorphism(f:R→S) THEN Image(f) is a subring of S.
R18 IF RingHomomorphism(f:R→S) THEN R/Kernel(f) ≅ Image(f).
R19 IF RingWithUnity(R) AND UnitalHomomorphism(f:R→S) THEN f(1_R)=1_S.
R20 IF RingWithUnity(R) AND Unit(a) AND Unit(b) THEN Unit(ab).
R21 IF RingWithUnity(R) AND Unit(a) THEN a is not a left or right zero divisor.
R22 IF CommutativeRing(R) AND Nilpotent(a) THEN a belongs to nilradical(R).
R23 IF BooleanRing(R) THEN CommutativeRing(R) AND ∀a: a+a=0.
R24 IF IntegralDomain(R) AND Finite(R) THEN Field(R).
R25 IF EuclideanDomain(R) THEN PrincipalIdealDomain(R).
R26 IF PrincipalIdealDomain(R) THEN UniqueFactorisationDomain(R).
R27 IF UniqueFactorisationDomain(R) THEN IntegralDomain(R).
R28 IF Ring(R) AND Subring(S,R) THEN Ring(S) under restricted operations.
R29 IF RingWithUnity(R) THEN additive zero and multiplicative identity are unique.
R30 IF Ring(R) AND a²=a THEN Idempotent(a).
R31 IF Ring(R) AND ∃n≥1:a^n=0 THEN Nilpotent(a).
R32 IF RingWithUnity(R) AND a has a two-sided multiplicative inverse THEN Unit(a).

08. VALIDATION CONSTRAINTS
V01: R must be nonempty.
V02: Addition and multiplication must be total binary operations on R.
V03: Addition must be associative and commutative.
V04: Addition must have identity and inverses.
V05: Multiplication must be associative.
V06: Both distributive laws must hold.
V07: Do not infer commutative multiplication from Ring alone.
V08: Do not infer multiplicative identity from Ring alone.
V09: A quotient by a one-sided ideal alone is not generally a ring.
V10: Distinguish unital from non-unital homomorphisms.
V11: For zero-divisor statements in noncommutative rings, record left/right orientation.
V12: Do not infer cancellation under multiplication in arbitrary rings.
V13: IntegralDomain requires nonzero and unity by this ontology's convention.
V14: Finite integral domain is a field; finite ring in general need not be.

09. MATHEMATICAL EXAMPLES
E01: (Z,+,×) is a commutative ring with unity and an integral domain, but not a field.
E02: (Z/nZ,+,×) is a commutative ring with unity; it is a field exactly when n is prime (n≥2).
E03: (Q,+,×), (R,+,×), (C,+,×) are fields.
E04: M_n(R) for a commutative unital ring R and n≥2 is generally noncommutative.
E05: 2Z under usual operations is a commutative ring without multiplicative identity.
E06: F[x] is a polynomial ring and integral domain when F is a field.
E07: Z/6Z has nonzero zero divisors: [2][3]=[0].
E08: In Z/8Z, [2] is nilpotent since [2]^3=[0].
E09: Every ideal nZ of Z defines a quotient Z/nZ for n≥1.
E10: The zero ring {0} satisfies ring axioms, but is not an integral domain by the nonzero convention.
E11: In Z/6Z, [3] is idempotent since [3]^2=[3].
E12: Upper triangular 2×2 real matrices form a noncommutative ring with unity.

10. SEMANTIC EQUIVALENCE
"ring" ↔ "associative ring" [where ring conventions agree]
"commutative ring" ↔ "ring with commutative multiplication"
"unit" ↔ "invertible element" [in a ring with unity]
"two-sided ideal" ↔ "ideal" [when ideal convention is explicitly two-sided]
"factor ring" ↔ "quotient ring"
"ring morphism" ↔ "ring homomorphism" [same unity-preservation convention]
NOT_EQUIVALENT: Ring != Field; Ring != IntegralDomain; Ring != Group.

11. KNOWLEDGE GRAPH TRIPLES
(Ring,subClassOf,AlgebraicStructure)
(Ring,hasOperation,Addition)
(Ring,hasOperation,Multiplication)
(Addition,forms,AbelianGroup)
(Multiplication,hasProperty,Associativity)
(Multiplication,distributesOver,Addition)
(Field,subClassOf,IntegralDomain)
(IntegralDomain,subClassOf,CommutativeRing)
(QuotientRing,requires,TwoSidedIdeal)
(RingHomomorphism,hasKernel,Ideal)

12. REASONING WORKFLOW
INPUT: carrier set, operations, asserted axioms, candidate subtype, provenance.
NORMALISE: resolve symbols, ring-with-unity convention and operation types.
VERIFY: test closure, additive group, multiplication associativity and both distributive laws.
CLASSIFY: evaluate commutativity, identity, zero divisors, inverses and finiteness.
INFER: apply sound rules R01–R32 with prerequisites.
VALIDATE: enforce V01–V14; report contradictions or insufficient evidence.
OUTPUT: typed ring facts, proof obligations, supported conclusions and provenance.

13. CONFIDENCE
CONFIDENCE: 1.0 for a formally verified theorem under explicitly satisfied hypotheses.
CONFIDENCE: conditional for claims whose hypotheses are unverified.
CONFIDENCE: not a substitute for proof; do not promote example-based generalisation to theorem.

14. FLOW_HASH
FLOW_HASH_ALGORITHM: SHA-256
FLOW_HASH_SCOPE: canonical UTF-8 text of this file, excluding any subsequently embedded hash value.
FLOW_HASH_VALUE: computed externally at ingestion; no fabricated digest.

15. UPDATE_MODEL
UPDATE_MODEL: semantic-versioned
UPDATE_TRIGGER: changed definitions, conventions, relations, rules, examples or source page.
UPDATE_ACTION: rerun type checks, theorem validation, semantic mapping and hash calculation.
PROVENANCE: record source URL, retrieval date, version, reviewer and change log.

16. AI_CONSUMPTION
AI_CONSUMPTION:
  parse_mode: typed ontology and deterministic rule set
  preserve_assumptions: true
  distinguish_axioms_from_derived_claims: true
  prohibit_unsupported_inference: true
  respect_nonunital_convention: true
  emit_proof_obligations: true
  retain_provenance: true
  report_ambiguity: true
  output_format: entity_graph + rule_trace + validation_report

17. ATTRIBUTION
Mark Higgins — Sky (Recursive AI)
https://kirethresearch.org
END FLOW ALGEBRA