uor-foundation 0.4.0

// @generated by uor-crate from uor-ontology — do not edit manually

//! Shared enumerations derived from the UOR Foundation ontology.

use core::fmt;

/// Kernel/user/bridge classification for each namespace module.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum Space {
    /// Immutable kernel-space: compiled into ROM.
    #[default]
    Kernel,
    /// Parameterizable user-space: runtime declarations.
    User,
    /// Bridge: kernel-computed, user-consumed.
    Bridge,
}

impl fmt::Display for Space {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Kernel => f.write_str("kernel"),
            Self::User => f.write_str("user"),
            Self::Bridge => f.write_str("bridge"),
        }
    }
}

/// The 10 primitive operations defined in the UOR Foundation.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum PrimitiveOp {
    /// Ring reflection: neg(x) = (-x) mod 2^n. One of the two generators of the dihedral group D_{2^n}. neg(neg(x)) = x (involution property).
    #[default]
    Neg,
    /// Hypercube reflection: bnot(x) = (2^n - 1) ⊕ x (bitwise complement). The second generator of D_{2^n}. bnot(bnot(x)) = x.
    Bnot,
    /// Successor: succ(x) = neg(bnot(x)) = (x + 1) mod 2^n. The critical identity: succ is the composition neg ∘ bnot.
    Succ,
    /// Predecessor: pred(x) = bnot(neg(x)) = (x - 1) mod 2^n. The inverse of succ. pred is the composition bnot ∘ neg.
    Pred,
    /// Ring addition: add(x, y) = (x + y) mod 2^n. Commutative, associative; identity element is 0.
    Add,
    /// Ring subtraction: sub(x, y) = (x - y) mod 2^n. Not commutative, not associative.
    Sub,
    /// Ring multiplication: mul(x, y) = (x × y) mod 2^n. Commutative, associative; identity element is 1.
    Mul,
    /// Bitwise exclusive or: xor(x, y) = x ⊕ y. Commutative, associative; identity element is 0.
    Xor,
    /// Bitwise and: and(x, y) = x ∧ y. Commutative, associative.
    And,
    /// Bitwise or: or(x, y) = x ∨ y. Commutative, associative.
    Or,
    /// Byte-level less-than-or-equal: le(x, y) = 1 if x ≤ y else 0. Operands compared as big-endian unsigned byte sequences. The catamorphism fold-rule emits Literal(1) on true, Literal(0) on false.
    Le,
    /// Byte-level less-than: lt(x, y) = 1 if x < y else 0. Operands compared as big-endian unsigned byte sequences.
    Lt,
    /// Byte-level greater-than-or-equal: ge(x, y) = 1 if x ≥ y else 0. Operands compared as big-endian unsigned byte sequences.
    Ge,
    /// Byte-level greater-than: gt(x, y) = 1 if x > y else 0. Operands compared as big-endian unsigned byte sequences.
    Gt,
    /// Byte-sequence concatenation: concat(x, y) = x ⧺ y. The substrate's byte-packing primitive — admits header serialization and other byte-array construction patterns. Result length is len(x) + len(y), bounded by the foundation's TERM_VALUE_MAX_BYTES ceiling.
    Concat,
}

impl fmt::Display for PrimitiveOp {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Neg => f.write_str("neg"),
            Self::Bnot => f.write_str("bnot"),
            Self::Succ => f.write_str("succ"),
            Self::Pred => f.write_str("pred"),
            Self::Add => f.write_str("add"),
            Self::Sub => f.write_str("sub"),
            Self::Mul => f.write_str("mul"),
            Self::Xor => f.write_str("xor"),
            Self::And => f.write_str("and"),
            Self::Or => f.write_str("or"),
            Self::Le => f.write_str("le"),
            Self::Lt => f.write_str("lt"),
            Self::Ge => f.write_str("ge"),
            Self::Gt => f.write_str("gt"),
            Self::Concat => f.write_str("concat"),
        }
    }
}

/// The three metric axes in the UOR tri-metric classification.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum MetricAxis {
    /// The vertical (ring/additive) metric axis. Constraints on this axis operate through ring arithmetic: residue classes, divisibility, and additive structure.
    #[default]
    Vertical,
    /// The horizontal (Hamming/bitwise) metric axis. Constraints on this axis operate through bitwise structure: carry patterns, bit positions, and Hamming distance.
    Horizontal,
    /// The diagonal (incompatibility) metric axis. Constraints on this axis measure the gap between ring and Hamming metrics — the curvature of UOR geometry.
    Diagonal,
}

impl fmt::Display for MetricAxis {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Vertical => f.write_str("vertical"),
            Self::Horizontal => f.write_str("horizontal"),
            Self::Diagonal => f.write_str("diagonal"),
        }
    }
}

/// The state of a site: pinned or free.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum SiteState {
    /// Site is determined by a constraint.
    #[default]
    Pinned,
    /// Site is still available for refinement.
    Free,
}

impl fmt::Display for SiteState {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Pinned => f.write_str("pinned"),
            Self::Free => f.write_str("free"),
        }
    }
}

/// The geometric role of a ring operation in the UOR dual-geometry (ring + hypercube). Every op:Operation individual references exactly one GeometricCharacter via op:hasGeometricCharacter. The nine canonical individuals correspond to the action types of the dihedral group D_{2^n}.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum GeometricCharacter {
    /// Reflection through the origin of the additive ring: neg(x) = -x mod 2^n. One of the two generators of D_{2^n}.
    #[default]
    RingReflection,
    /// Reflection through the centre of the hypercube: bnot(x) = (2^n-1) ⊕ x. The second generator of D_{2^n}.
    HypercubeReflection,
    /// Rotation by one step: succ(x) = (x+1) mod 2^n. The composition of the two reflections.
    Rotation,
    /// Rotation by one step in the reverse direction: pred(x) = (x-1) mod 2^n.
    RotationInverse,
    /// Translation along the ring axis: add(x,y), sub(x,y). Preserves Hamming distance locally.
    Translation,
    /// Scaling along the ring axis: mul(x,y) = (x×y) mod 2^n.
    Scaling,
    /// Translation along the hypercube axis: xor(x,y) = x ⊕ y. Preserves ring distance locally.
    HypercubeTranslation,
    /// Projection onto a hypercube face: and(x,y) = x ∧ y. Idempotent; collapses dimensions.
    HypercubeProjection,
    /// Join on the hypercube lattice: or(x,y) = x ∨ y. Idempotent; dual to projection.
    HypercubeJoin,
    /// Geometric character of dispatch: constraint-guided selection over the resolver registry lattice.
    ConstraintSelection,
    /// Geometric character of inference: traversal through the φ-pipeline resolution graph P ∘ Π ∘ G.
    ResolutionTraversal,
    /// Geometric character of accumulation: progressive pinning of site states in the context lattice.
    SiteBinding,
    /// Geometric character of lease partition: splitting a shared context into disjoint site-set leases.
    SitePartition,
    /// Geometric character of session composition: merging disjoint lease sessions into a unified resolution context.
    SessionMerge,
}

impl fmt::Display for GeometricCharacter {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::RingReflection => f.write_str("ring_reflection"),
            Self::HypercubeReflection => f.write_str("hypercube_reflection"),
            Self::Rotation => f.write_str("rotation"),
            Self::RotationInverse => f.write_str("rotation_inverse"),
            Self::Translation => f.write_str("translation"),
            Self::Scaling => f.write_str("scaling"),
            Self::HypercubeTranslation => f.write_str("hypercube_translation"),
            Self::HypercubeProjection => f.write_str("hypercube_projection"),
            Self::HypercubeJoin => f.write_str("hypercube_join"),
            Self::ConstraintSelection => f.write_str("constraint_selection"),
            Self::ResolutionTraversal => f.write_str("resolution_traversal"),
            Self::SiteBinding => f.write_str("site_binding"),
            Self::SitePartition => f.write_str("site_partition"),
            Self::SessionMerge => f.write_str("session_merge"),
        }
    }
}

/// A named mathematical discipline through which an algebraic identity is established and grounded. Every op:Identity individual references at least one VerificationDomain via op:verificationDomain. The nine canonical domain individuals are kernel-level constants defined in op/.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum VerificationDomain {
    /// Established by exhaustive traversal of R_n. Valid for all identities where the ring is finite.
    #[default]
    Enumerative,
    /// Established by equational reasoning from ring or group axioms. Covers derivations via associativity, commutativity, inverse laws, and group presentations.
    Algebraic,
    /// Established by isometry, symmetry, or GeometricCharacter arguments. Covers dihedral actions, fixed-point analysis, automorphism groups, and affine embeddings.
    Geometric,
    /// Established via discrete differential calculus or metric analysis. Covers ring/Hamming derivatives (DC_), metric divergence (AM_), and adiabatic scheduling (AR_).
    Analytical,
    /// Established via entropy, Landauer bounds, or Boltzmann distributions. Covers site entropy (TH_), reversible computation (RC_), and phase transitions.
    Thermodynamic,
    /// Established via simplicial homology, cohomology, or constraint nerve analysis. Covers homological algebra (HA_) and the ψ-pipeline base chain ψ_1..ψ_6 (constraint nerve construction, chain functor, homology, Betti extraction, dualization, cohomology).
    Topological,
    /// Established by the inter-algebra map structure of the resolution pipeline. Covers φ-maps (phi_1–phi_6) and the ψ-pipeline tower ψ_7..ψ_9 (Postnikov truncation, homotopy group extraction, k-invariant computation). The earlier ψ_1..ψ_6 chain (constraint nerve → simplicial homology) is established under op:Topological.
    Pipeline,
    /// Established by the composition of Analytical and Topological reasoning. The only domain requiring multiple op:verificationDomain assertions. Covers the UOR Index Theorem (IT_7a–IT_7d).
    IndexTheoretic,
    /// Established by superposition analysis of site states. Covers identities involving superposed (non-classical) site assignments where sites carry complex amplitudes.
    SuperpositionDomain,
    /// Established by the intersection of quantum superposition analysis and classical thermodynamic reasoning. Covers identities relating von Neumann entropy of superposed states to Landauer costs of projective collapse (QM_).
    QuantumThermodynamic,
    /// Established by number-theoretic valuation arguments including p-adic absolute values, the Ostrowski product formula, and the arithmetic of global fields. Covers identities grounded in the product formula |x|_p · |x|_∞ = 1 and the Witt–Ostrowski derivation chain.
    ArithmeticValuation,
    /// Verification domain for composed operation identities — algebraic properties of operator compositions including dispatch, inference, accumulation, lease, and session composition operations.
    ComposedAlgebraic,
}

impl fmt::Display for VerificationDomain {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Enumerative => f.write_str("enumerative"),
            Self::Algebraic => f.write_str("algebraic"),
            Self::Geometric => f.write_str("geometric"),
            Self::Analytical => f.write_str("analytical"),
            Self::Thermodynamic => f.write_str("thermodynamic"),
            Self::Topological => f.write_str("topological"),
            Self::Pipeline => f.write_str("pipeline"),
            Self::IndexTheoretic => f.write_str("index_theoretic"),
            Self::SuperpositionDomain => f.write_str("superposition_domain"),
            Self::QuantumThermodynamic => f.write_str("quantum_thermodynamic"),
            Self::ArithmeticValuation => f.write_str("arithmetic_valuation"),
            Self::ComposedAlgebraic => f.write_str("composed_algebraic"),
        }
    }
}

/// A computational complexity classification for resolvers. Each resolver's asymptotic runtime is typed as a named ComplexityClass individual rather than a free string.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum ComplexityClass {
    /// O(1) complexity — the resolver runs in constant time regardless of ring size.
    #[default]
    Constant,
    /// O(log n) complexity — the resolver runs in logarithmic time in the quantum level.
    Logarithmic,
    /// O(n) complexity — the resolver runs in time linear in the quantum level.
    Linear,
    /// O(2^n) complexity — the resolver runs in time exponential in the quantum level.
    Exponential,
}

impl fmt::Display for ComplexityClass {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Constant => f.write_str("constant"),
            Self::Logarithmic => f.write_str("logarithmic"),
            Self::Linear => f.write_str("linear"),
            Self::Exponential => f.write_str("exponential"),
        }
    }
}

/// A named rewrite rule that can be applied in a derivation step. Each RewriteRule individual represents a specific algebraic law or normalization strategy used during term rewriting.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum RewriteRule {
    /// The rewrite rule applying the critical identity: neg(bnot(x)) → succ(x). Grounded in op:criticalIdentity.
    #[default]
    CriticalIdentity,
    /// The rewrite rule applying involution cancellation: f(f(x)) → x for any involution f.
    Involution,
    /// The rewrite rule applying associativity to re-bracket nested binary operations.
    Associativity,
    /// The rewrite rule applying commutativity to reorder operands of commutative operations.
    Commutativity,
    /// The rewrite rule eliminating identity elements: add(x, 0) → x, mul(x, 1) → x, xor(x, 0) → x.
    IdentityElement,
    /// The rewrite rule normalizing compound expressions to canonical ordering (e.g., sorting operands by address).
    Normalization,
}

impl fmt::Display for RewriteRule {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::CriticalIdentity => f.write_str("critical_identity"),
            Self::Involution => f.write_str("involution"),
            Self::Associativity => f.write_str("associativity"),
            Self::Commutativity => f.write_str("commutativity"),
            Self::IdentityElement => f.write_str("identity_element"),
            Self::Normalization => f.write_str("normalization"),
        }
    }
}

/// A unit of measurement for observable quantities. Each MeasurementUnit individual names a specific unit (bits, ring steps, dimensionless) replacing the string-valued observable:unit property.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum MeasurementUnit {
    /// Information-theoretic unit: the measurement is in bits (e.g., Hamming weight, entropy).
    #[default]
    Bits,
    /// Ring-arithmetic unit: the measurement is in ring distance steps (|x - y| mod 2^n).
    RingSteps,
    /// Dimensionless unit: the measurement is a pure number (e.g., winding number, Betti number, spectral gap).
    Dimensionless,
    /// Natural information unit: entropy measured in nats (using natural logarithm). S_residual is expressed in nats when computed as (Σ κ_k − χ) × ln 2.
    Nats,
}

impl fmt::Display for MeasurementUnit {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Bits => f.write_str("bits"),
            Self::RingSteps => f.write_str("ring_steps"),
            Self::Dimensionless => f.write_str("dimensionless"),
            Self::Nats => f.write_str("nats"),
        }
    }
}

/// A classification of coordinate types that a CoordinateQuery can extract. Each TriadProjection individual names a specific coordinate system (stratum, spectrum, address) replacing the string-valued query:coordinate property.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum TriadProjection {
    /// The stratum coordinate: the layer position of a datum within the ring's stratification.
    #[default]
    TwoAdicValuation,
    /// The spectrum coordinate: the spectral decomposition of a datum under the ring's Fourier analysis.
    WalshHadamardImage,
    /// The address coordinate: the content-addressable position of a datum in the Braille glyph encoding. Renamed from RingElement in v0.2.2 W8 to unify vocabulary with the schema:Triad bundling properties.
    Address,
}

impl fmt::Display for TriadProjection {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::TwoAdicValuation => f.write_str("two_adic_valuation"),
            Self::WalshHadamardImage => f.write_str("walsh_hadamard_image"),
            Self::Address => f.write_str("address"),
        }
    }
}

/// A typed controlled vocabulary for session boundary reasons. Each individual names a specific reason a context-reset boundary was triggered during a multi-turn session.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum SessionBoundaryType {
    /// The caller explicitly requested a context reset. All accumulated bindings are discarded.
    #[default]
    ExplicitReset,
    /// The session resolver determined that no further queries can reduce the aggregate site deficit.
    ConvergenceBoundary,
    /// A new query produced a type contradiction with an accumulated binding. Context must reset before resolution can continue.
    ContradictionBoundary,
}

impl fmt::Display for SessionBoundaryType {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::ExplicitReset => f.write_str("explicit_reset"),
            Self::ConvergenceBoundary => f.write_str("convergence_boundary"),
            Self::ContradictionBoundary => f.write_str("contradiction_boundary"),
        }
    }
}

/// A classification of phase boundary in the catastrophe diagram: period boundary (g divides 2^n − 1) or power-of-two boundary (g = 2^k).
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum PhaseBoundaryType {
    /// A phase boundary where g divides 2^n − 1, meaning g is a period of the multiplicative structure of R_n.
    #[default]
    Period,
    /// A phase boundary where g = 2^k, meaning g aligns with the binary stratification of R_n.
    PowerOfTwo,
}

impl fmt::Display for PhaseBoundaryType {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Period => f.write_str("period"),
            Self::PowerOfTwo => f.write_str("power_of_two"),
        }
    }
}

/// A typed controlled vocabulary for the three phases of context saturation: Open (σ = 0), PartialGrounding (0 < σ < 1), and FullGrounding (σ = 1).
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum GroundingPhase {
    /// The context has σ = 0: no bindings accumulated, all sites are free. The initial phase of every session.
    #[default]
    Open,
    /// The context has 0 < σ < 1: some sites are pinned by accumulated bindings, but free sites remain. The accumulation phase.
    PartialGrounding,
    /// The context has σ = 1: all sites are pinned, freeRank = 0. The ground state. All subsequent queries resolve in O(1) via SC_5.
    FullGrounding,
}

impl fmt::Display for GroundingPhase {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Open => f.write_str("open"),
            Self::PartialGrounding => f.write_str("partial_grounding"),
            Self::FullGrounding => f.write_str("full_grounding"),
        }
    }
}

/// The achievability classification of a topological signature in the morphospace. Either Achievable or Forbidden (witnessed by ImpossibilityWitness).
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum AchievabilityStatus {
    /// The signature has been verified as achievable at some quantum level by an AxiomaticDerivation proof.
    #[default]
    Achievable,
    /// The signature has been formally proven impossible by an ImpossibilityWitness deriving from MS_1, MS_2, or other impossibility theorems.
    Forbidden,
}

impl fmt::Display for AchievabilityStatus {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Achievable => f.write_str("achievable"),
            Self::Forbidden => f.write_str("forbidden"),
        }
    }
}

/// Root class for validity scope individuals. Instances are the four named scope kinds: Universal, ParametricLower, ParametricRange, and LevelSpecific.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum ValidityScopeKind {
    /// Holds for all k in N. No minimum k constraint.
    #[default]
    Universal,
    /// Holds for all k >= k_min, where k_min is given by validKMin.
    ParametricLower,
    /// Holds for k_min <= k <= k_max. Both validKMin and validKMax required.
    ParametricRange,
    /// Holds only at exactly one level, given by a WittLevelBinding.
    LevelSpecific,
}

impl fmt::Display for ValidityScopeKind {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Universal => f.write_str("universal"),
            Self::ParametricLower => f.write_str("parametric_lower"),
            Self::ParametricRange => f.write_str("parametric_range"),
            Self::LevelSpecific => f.write_str("level_specific"),
        }
    }
}

/// A typed controlled vocabulary for ExecutionPolicy individuals. Follows the SessionBoundaryType pattern: a single class with named individuals rather than a subclass hierarchy.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum ExecutionPolicyKind {
    /// Process queries in arrival order. The implicit pre-Amendment 48 behavior.
    #[default]
    FifoPolicy,
    /// Process the query with the smallest targetSite.freeRank first. Favors cheapest resolutions, accelerating early grounding gain.
    MinFreeCountFirst,
    /// Process the query with the largest targetSite.freeRank first. Favors hardest resolutions, maximizing information gain per step.
    MaxFreeCountFirst,
    /// Process queries whose targetSite is disjoint from all other pending queries' site sets first. Minimizes contention when operating against a SharedContext.
    DisjointFirst,
}

impl fmt::Display for ExecutionPolicyKind {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::FifoPolicy => f.write_str("fifo_policy"),
            Self::MinFreeCountFirst => f.write_str("min_free_count_first"),
            Self::MaxFreeCountFirst => f.write_str("max_free_count_first"),
            Self::DisjointFirst => f.write_str("disjoint_first"),
        }
    }
}

/// The variance of a structural type position under operad composition. One of Covariant, Contravariant, Invariant, or Bivariant.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum VarianceAnnotation {
    /// The structural position preserves TypeInclusion: if T₁ ≤ T₂, then F(T₁) ≤ F(T₂).
    #[default]
    Covariant,
    /// The structural position reverses TypeInclusion: if T₁ ≤ T₂, then F(T₂) ≤ F(T₁).
    Contravariant,
    /// The structural position requires exact type equality: F(T₁) ≤ F(T₂) only if T₁ = T₂.
    Invariant,
    /// The structural position ignores the type parameter: F(T₁) ≤ F(T₂) for all T₁, T₂.
    Bivariant,
}

impl fmt::Display for VarianceAnnotation {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Covariant => f.write_str("covariant"),
            Self::Contravariant => f.write_str("contravariant"),
            Self::Invariant => f.write_str("invariant"),
            Self::Bivariant => f.write_str("bivariant"),
        }
    }
}

/// The kind of quantifier: Universal (forall) or Existential (exists). Controlled vocabulary with exactly 2 individuals.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum QuantifierKind {
    /// Universal quantification (forall).
    #[default]
    Universal,
    /// Existential quantification (exists).
    Existential,
}

impl fmt::Display for QuantifierKind {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Universal => f.write_str("universal"),
            Self::Existential => f.write_str("existential"),
        }
    }
}

/// A controlled vocabulary of proof methods. Each proof individual carries exactly one strategy from this vocabulary, enabling compilation to verified theorem provers.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum ProofStrategy {
    /// Follows from ZMod ring axioms. Lean4 tactic: `by ring`.
    #[default]
    RingAxiom,
    /// Decidable at Q0 by exhaustive evaluation. Lean4: `by native_decide`.
    DecideQ0,
    /// Induction on bit width n. Lean4: `by induction n`.
    BitwiseInduction,
    /// From dihedral group presentation. Lean4: `by group`.
    GroupPresentation,
    /// By simplification with cited lemmas. Lean4: `by simp \[lemmalist\]`.
    Simplification,
    /// By Chinese Remainder Theorem. Lean4: `by exact ZMod.chineseRemainder ...`.
    ChineseRemainder,
    /// By Euler-Poincare formula applied to the constraint nerve.
    EulerPoincare,
    /// By Ostrowski product formula or derived valuation arguments.
    ProductFormula,
    /// By composing proofs of sub-identities. Lean4: `by exact ...`.
    Composition,
    /// By deriving contradiction for impossibility witnesses. Lean4: `by contradiction`.
    Contradiction,
    /// By computation at a specified quantum level. Lean4: `by native_decide`.
    Computation,
}

impl fmt::Display for ProofStrategy {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::RingAxiom => f.write_str("ring_axiom"),
            Self::DecideQ0 => f.write_str("decide_q0"),
            Self::BitwiseInduction => f.write_str("bitwise_induction"),
            Self::GroupPresentation => f.write_str("group_presentation"),
            Self::Simplification => f.write_str("simplification"),
            Self::ChineseRemainder => f.write_str("chinese_remainder"),
            Self::EulerPoincare => f.write_str("euler_poincare"),
            Self::ProductFormula => f.write_str("product_formula"),
            Self::Composition => f.write_str("composition"),
            Self::Contradiction => f.write_str("contradiction"),
            Self::Computation => f.write_str("computation"),
        }
    }
}

/// The kind of shape violation: Missing, TypeMismatch, CardinalityViolation, ValueCheck, or LevelMismatch.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum ViolationKind {
    /// Required property was not set on the builder.
    #[default]
    Missing,
    /// Property was set but its value is not an instance of the constraintRange.
    TypeMismatch,
    /// Cardinality violated: too few or too many values provided.
    CardinalityViolation,
    /// Value-dependent check failed (Tier 2). For example, thermodynamic budget insufficient for Landauer bound.
    ValueCheck,
    /// A term's quantum level annotation exceeds the CompileUnit ceiling, or binary operation operands are at different levels without an intervening lift or project.
    LevelMismatch,
}

impl fmt::Display for ViolationKind {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Missing => f.write_str("missing"),
            Self::TypeMismatch => f.write_str("type_mismatch"),
            Self::CardinalityViolation => f.write_str("cardinality_violation"),
            Self::ValueCheck => f.write_str("value_check"),
            Self::LevelMismatch => f.write_str("level_mismatch"),
        }
    }
}

/// Closed enumeration of partition component kinds: Irreducible (non-factorizable), Reducible (factorizable into non-trivial parts), Units (invertible), Exterior (outside the factorization domain). Codegen treats this as an enum class with exactly 4 individuals.
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum PartitionComponent {
    /// The irreducible component: elements that admit no non-trivial factorization within the ring.
    #[default]
    Irreducible,
    /// The reducible component: elements that factor into non-trivial parts.
    Reducible,
    /// The unit component: invertible elements of the ring.
    Units,
    /// The exterior component: elements outside the factorization domain (e.g., zero or ring-boundary values).
    Exterior,
}

impl fmt::Display for PartitionComponent {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Irreducible => f.write_str("irreducible"),
            Self::Reducible => f.write_str("reducible"),
            Self::Units => f.write_str("units"),
            Self::Exterior => f.write_str("exterior"),
        }
    }
}

/// The modality of a proof: computation (exhaustive verification at a specific quantum level) or axiomatic (derivation from ring axioms).
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub enum ProofModality {
    /// A proof confirmed by exhaustive execution over R_n at a specific quantum level.
    #[default]
    Computation,
    /// A proof derived from ring axioms that holds at all quantum levels.
    Axiomatic,
    /// A proof by structural induction on the quantum level parameter k.
    Inductive,
}

impl fmt::Display for ProofModality {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Computation => f.write_str("computation"),
            Self::Axiomatic => f.write_str("axiomatic"),
            Self::Inductive => f.write_str("inductive"),
        }
    }
}

/// A Witt level W_n at which the UOR ring R_n = Z/2^n Z operates.
/// Corresponds to `schema:WittLevel` in the uor.foundation ontology.
/// The class is open: any positive multiple of 8 identifies a valid level.
/// Named levels W8 through W32 are provided as associated constants.
/// Arbitrary levels can be constructed with `WittLevel::new(n)`.
/// # Examples
/// ```rust
/// use uor_foundation::WittLevel;
///
/// // Named reference levels (W8-W32 are spec-defined):
/// let w8 = WittLevel::W8;
/// assert_eq!(w8.witt_length(), 8);
/// assert_eq!(w8.bits_width(), 8);    // Witt length IS bit width
/// assert_eq!(w8.cycle_size(), Some(256)); // 2^8 = 256 ring elements
///
/// let w32 = WittLevel::W32;
/// assert_eq!(w32.bits_width(), 32);  // 32 bits
///
/// // Arbitrary levels beyond W32 (Prism-declared):
/// let w64 = WittLevel::new(64);
/// assert_eq!(w64.bits_width(), 64);  // 64 bits — native u64
///
/// // The chain is unbounded:
/// let w88 = WittLevel::new(88);
/// assert_eq!(w88.bits_width(), 88);
/// assert_eq!(w88.next_witt_level().witt_length(), 96);
///
/// // Ordering follows the Witt length:
/// assert!(WittLevel::W8 < WittLevel::W32);
/// ```
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub struct WittLevel {
    /// The Witt length n in W_n. Maps to `schema:wittLength`.
    witt_length: u32,
}

impl WittLevel {
    /// Witt level 8: 8-bit ring Z/256Z, 256 states. The reference level for all ComputationCertificate proofs in the spec.
    pub const W8: Self = Self { witt_length: 8 };
    /// Witt level 16: 16-bit ring Z/65536Z, 65,536 states.
    pub const W16: Self = Self { witt_length: 16 };
    /// Witt level 24: 24-bit ring Z/16777216Z, 16,777,216 states.
    pub const W24: Self = Self { witt_length: 24 };
    /// Witt level 32: 32-bit ring Z/4294967296Z, 4,294,967,296 states. The highest named level in the spec.
    pub const W32: Self = Self { witt_length: 32 };

    /// Construct an arbitrary Witt level W_n. `n` need not be one of the spec-named individuals; Prism implementations may use any level.
    #[inline]
    pub const fn new(witt_length: u32) -> Self {
        Self { witt_length }
    }

    /// The Witt length n. Maps to `schema:wittLength`.
    #[inline]
    pub const fn witt_length(self) -> u32 {
        self.witt_length
    }

    /// Bit width of the ring at this level: equal to the Witt length. Maps to `schema:bitsWidth`. This is an identity — the Witt length IS the bit width.
    #[inline]
    pub const fn bits_width(self) -> u32 {
        self.witt_length
    }

    /// Number of distinct ring states at this level: 2^n. Maps to `schema:cycleSize`. Returns `None` if the result exceeds `u128` (i.e. for n > 128).
    #[inline]
    pub const fn cycle_size(self) -> Option<u128> {
        1u128.checked_shl(self.bits_width())
    }

    /// The next Witt level in the chain: W_n -> W_{n+8}. Maps to `schema:nextWittLevel`. Always well-defined; the chain is unbounded.
    #[inline]
    pub const fn next_witt_level(self) -> Self {
        Self {
            witt_length: self.witt_length + 8,
        }
    }
}

impl Default for WittLevel {
    /// `W8` is the spec-defined minimum Witt level and the canonical base referenced by `schema:WittLevel` individuals.
    #[inline]
    fn default() -> Self {
        Self::W8
    }
}

impl fmt::Display for WittLevel {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "w{}", self.witt_length)
    }
}