Universal Object Reference Foundation Ontology — the complete vocabulary for the UOR kernel, type system, resolution pipeline, and state model.
Whether this module belongs to kernel-space (immutable, compiled), user-space (parameterizable, runtime), or bridge (kernel-computed, user-consumed). Values: 'kernel', 'user', 'bridge'.
Content-addressable identifiers for ring elements. Each element carries a unique content-derived identifier.
A content-addressable ring element. Each Element uniquely identifies a piece of content via its hash-derived identifier.
The number of Braille glyphs in an address string.
The datum that this address references. Inverse of schema:glyph.
The content hash of this address. Format: (blake3|sha256) colon followed by 64 lowercase hex characters. The algorithm prefix must match u:digestAlgorithm.
The hash algorithm used to produce u:digest. Allowed values: 'blake3' (primary), 'sha256' (secondary).
The canonical byte serialisation of the addressed datum, per Amendment 43 section 2: header(k) || le_bytes(x, k+1). This is the exact byte string hashed to produce u:digest.
The Witt level n of this element. The element encodes a datum in R_n = Z/(2^n)Z.
Core value types and term language for the UOR ring substrate. Defines Datum (ring element), Term (syntactic expression), and the Ring container.
An element of the ring Z/(2^n)Z at a specific Witt level n. The primary semantic value type. Disjoint from Term: datums are values, terms are syntactic expressions that evaluate to datums.
A syntactic expression in the UOR term language. Terms are evaluated to produce Datums. Disjoint from Datum.
A three-component structure encoding an element's position in the UOR address space: stratum (ring layer), spectrum (bit pattern), and glyph (Braille address).
A term that directly denotes a datum value. A Literal is a leaf node in the term language — it refers to a concrete Datum via schema:denotes without being a Datum itself.
A term formed by applying an operation to one or more argument terms. The application's value is the result of evaluating the operator on the evaluated arguments.
The ambient ring Z/(2^n)Z at a specific Witt level n. The Ring is the primary data structure of the UOR kernel. Its two generators (negation and complement) produce the dihedral group D_{2^n} that governs the invariance frame.
The concrete ring Z/(2^16)Z at Witt level 16. Subclass of schema:Ring. Carries 65,536 elements. W16Ring is the first extension of the default Q0 ring and is the target of Amendment 26's universality proofs.
A named Witt level Q_k at which the UOR ring operates. Level Q_k uses 8*(k+1) bits, 2^(8*(k+1)) states, and modulus 2^(8*(k+1)). The named individuals Q0-Q3 are the spec-defined reference levels. The class is open: Prism implementations operating at higher levels declare their own WittLevel individuals. The nextWittLevel property forms an unbounded chain Q0 -> Q1 -> Q2 -> ...
Root AST node for parsed EBNF term expressions. Identity lhs/rhs values are instances of TermExpression subtypes. Maps to the `term` production in the EBNF grammar.
A leaf AST node: an integer literal, variable reference, or named constant.
An AST node representing operator application: an operator applied to an argument list (e.g., add(x, y)).
An AST node for infix relations and logical connectives (e.g., x <= y, P -> Q, a = b).
An AST node for set-builder notation (e.g., {x : P(x)}).
An AST node for function composition (f compose g).
A structured quantifier binding: typed variable declarations with a domain and quantifier kind (universal or existential). Replaces the string-valued op:forAll property.
A single variable binding: a variable name bound to a domain type (e.g., x in R_n).
The kind of quantifier: Universal (forall) or Existential (exists). Controlled vocabulary with exactly 2 individuals.
An abstract leaf value that a grounding map can accept as surface input. Has no direct instances: every SurfaceSymbol is either a Datum-denoting schema:Literal or an xsd-typed schema:HostValue, and the two cases are disjoint.
An xsd-typed value that denotes a host datatype rather than a ring datum. Used in property-position slots whose range is xsd and as the host-side input of a grounding map.
A host string literal carrying an xsd:string value.
A host boolean literal carrying an xsd:boolean value.
The integer value of a datum element. For a Datum in Z/(2^n)Z, this is an integer in [0, 2^n).
The Witt level n of a datum, where the datum's ring is Z/(2^n)Z. Determines the bit width and modulus of the datum.
The ring-layer index of a datum, indicating its position in the stratification of Z/(2^n)Z.
The bit-pattern representation of a datum, encoding its position in the hypercube geometry of Z/(2^n)Z.
The content-addressable element associated with this datum, linking the algebraic value to its identifier.
The operation applied in an Application term.
An argument term in an Application. The ordering of arguments follows rdf:List semantics.
The bit width n of the ring Z/(2^n)Z. Distinct from schema:wittLength on Datum — ringWittLength is the container's bit width; datum wittLength is a membership property.
The modulus 2^n of the ring. Equals 2 raised to the power of ringWittLength.
The generator element π₁ (value = 1) of the ring. Under iterated successor application, π₁ generates all ring elements.
The ring reflection involution: neg(x) = (-x) mod 2^n. One of the two generators of the dihedral group D_{2^n}.
The hypercube reflection involution: bnot(x) = (2^n - 1) ⊕ x. The second generator of the dihedral group D_{2^n}.
The datum value that a Literal term denotes. Bridges the Term/Datum disjointness: a Literal refers to a Datum without being one. Evaluation of a Literal produces its denoted Datum.
The bit width 8*(k+1) of this Witt level.
The number of distinct states 2^(8*(k+1)) at this Witt level.
The next Witt level in the chain: Q_k -> Q_(k+1). The chain is unbounded; Q3 points to Q4, which is not a named individual in the spec but may be declared by Prism implementations.
The predecessor Witt level in the chain: Q_(k+1) -> Q_k. Inverse of nextWittLevel. If nextWittLevel(Q_k) = Q_(k+1), then wittLevelPredecessor(Q_(k+1)) = Q_k. Formalizes the chain extension protocol (QL_8).
The Witt level at which this Ring instance operates. Links a concrete Ring individual to its WittLevel.
Carrier set size of the Q1 ring: 65,536 elements.
The variable bindings in a quantifier declaration. Non-functional: a ForAllDeclaration may bind multiple variables.
The domain type of a variable binding (e.g., schema:Ring, type:ConstrainedType).
The name of a bound variable (e.g., 'x', 'y', 'n').
The kind of quantifier: Universal or Existential.
The operator in an application expression (e.g., op:add, op:neg).
The left operand of an infix expression.
The right operand of an infix expression.
The argument list of an application expression. Non-functional: an application may take multiple arguments.
The string representation of a literal expression value (e.g., '42', 'x', 'pi1').
The operator symbol in an infix expression (e.g., '=', '\u{2264}', '\u{2192}').
The string value carried by a HostStringLiteral.
The boolean value carried by a HostBooleanLiteral.
The unique generator of R_n under successor. Value = 1 at every Witt level. Under iterated application of succ, π₁ generates every element of the ring.
The additive identity of the ring. Value = 0 at every Witt level. op:add(x, zero) = x for all x in R_n.
Witt level 0: 8-bit ring Z/256Z, 256 states. The reference level for all ComputationCertificate proofs in the spec.
Witt level 1: 16-bit ring Z/65536Z, 65,536 states.
Witt level 3: 32-bit ring Z/4294967296Z, 4,294,967,296 states. The highest named level in the spec. nextWittLevel is absent — Prism implementations may extend the chain.
or(and(x_k,y_k), and(xor(x_k,y_k), c_k))
irredundant sub-collection (greedy removal)
x ∉ Unit ∪ Exterior AND no non-trivial factorization
factor g has optimal resolution at level n
directly computes set-theoretic partition
orbit decomposition yields same partition
all compute same set-theoretic partition
prefer vertical (residue) before horizontal (carry)
≤ TotalVariation(p₁) + TotalVariation(p₂)
ReductionLength(c₁) + ReductionLength(c₂)
ResidueConstraint(p, •) transitions visibility
trailing_ones(x) for t < n; n−1 for x = 2^n−1
measures failure of ring isometry to be Hamming isometry
complement each Braille character of glyph(x)
{xor, and, or, bnot}; NOT {add, sub, mul, neg, succ, pred}
Σ_i popcount(braille_i(a) ⊕ braille_i(b))
removes entropy; convergenceRate = cooling rate
temperature of partition phase transition
decreasing freeRank × cost-per-site order
{(n, g) : n ∈ Z₊, g constraint boundary}
= irreversible total cost (redistributed)
s' where type(s') ≡ type(s) under F.constraint
G: GroundingMap, P: ProjectionMap, F: Frame, s: Literal, G.symbolConstraints = P.projectionOrder
Boltzmann distribution at β* = ln 2, all n ≥ 1
C_prior, C_fresh: Context, SessionBoundary event
iff ∃ b, b': same address, different datum, same constraint
∃ ConstrainedType T over R_n realising target
target: χ* ≤ n, β₀* = 1, β_k* = 0 for k ≥ 1
target: realisable n-site type synthesis goal
iff CompletenessResolver certifies CompleteType
T: CompleteType at Q_n, T': WittLift to Q_{n+1}
T: CompleteType at Q_n with closed constraint set
every op:universallyValid identity, WittLift T'
valid and restricts to ChainComplex(T) on base nerve
HolonomyGroup(T) for additive constraints
T: all ResidueConstraint or DepthConstraint
HolonomyGroup(T) with neg + bnot in closed path
T: ConstrainedType with neg-related and bnot-related constraints in closed path
CompleteType (IT_7d) ⟹ β₁ = 0 ⟹ holonomy
monodromy(p₁) · monodromy(p₂) in D_{2^n}
non-zero class (non-trivial LiftObstruction)
freeRank(C) = 0 ↔ S(C) = 0 ↔ T_ctx(C) = 0
max(0, siteBudget(q.type) − |pinnedSites(C) ∩ q.siteSet|)
→ exact morphospace boundary in the limit
= Cost(T') for any geodesic T' on same type
T, T': GeodesicTrace on same ConstrainedType
∃ i: J_k(step_i) < max_{free} J_k(state_i)
apply(ResidueConstraint, collapsed_site)
WittLevel W_n with nextWittLevel defined
isAR1Ordered(trace) ∧ isDC10Selected(trace)
every chainStep has trivial or resolved LiftObstruction
basisSize(Q_j) + chainLength + obstructionResolutionCost
obstructionCount = 0 iff HolonomyGroup trivial at every step
CompleteType at Q_k satisfies IT_7d with witness chain
pin-site intersection residue-class compatible
CarryConstraint, ResidueConstraint pairs
all residues of C = modulus - 1, no Carry/Depth
count of monotone ConstrainedTypes at Q_n
CompleteType(A) and CompleteType(B) and Q(A)=Q(B)
no ConstrainedType with <= n constraints realises sigma
standard coefficient ring for psi-pipeline
pinsSites(killing constraint for obstruction c)
superset of pinsSites(C_i) cap pinsSites(C_j)
GluingObstruction c, cycle pair (C_i, C_j)
amplitude index set of SuperposedSiteState over T
monotone pinning trajectories consistent with T
SuperposedSiteState over ConstrainedType T at Q_n
∃ c: TransformCertificate. certifies(c, T)
∃ c: IsometryCertificate. certifies(c, T)
∃ c: InvolutionCertificate. certifies(c, f)
∃ c: GroundingCertificate. certifies(c, C)
∃ c: GeodesicCertificate. certifies(c, trace)
∃ c: MeasurementCertificate. certifies(c, event)
∃ c: BornRuleVerification. certifies(c, event)
∃ c: GroundingCertificate. certifies(c, map)
∀ j ≤ k: ∀ a ∈ pinnedSites(S_A, Q_j) ∩ pinnedSites(S_B, Q_j): datum(S_A, a, Q_j) = datum(S_B, a, Q_j)
S_A, S_B: Session at quantum level Q_k (k ≥ 0)
L_A, L_B: ContextLease on SharedContext C, L_A ≠ L_B
= finalState(R, P_2, Q) for any P_1, P_2: ExecutionPolicy
SessionResolver R with ExecutionPolicy P, pending query set Q
SharedContext C; leaseSet {L_1, …, L_k} covering all sites of C
ContextLease L held by Session S; binding step i within S restricted to leasedSites(L)
freeRank(S_A) + freeRank(S_B) − |pinnedSites(S_A) ∩ pinnedSites(S_B)|
S_A, S_B: Session; compose(S_A, S_B) valid (SR_8 satisfied)
S_A, S_B on ContextLeases L_A, L_B within SharedContext C; SR_9 holds
SessionResolver R; pending query set Q; ExecutionPolicy P_1, P_2
SharedContext C; leases {L_1, …, L_k} pairwise disjoint (SR_9) and fully covering C; each S_i with freeRank = 0 within L_i
q: RelationQuery; C* = compose(S_1, …, S_k) with σ(C*) = 1 by MC_6
max_i stepCount(S_i to convergence within L_i)
SharedContext C with totalSites = n; uniform partition into k leases
constraint configuration C, k > dim(N(C))
constraint configuration C, d = max simplex dim
H_k(N(C); Z) for smallest k with π_k ≠ 0
constraint configuration C, truncation level k
every CompleteType in exactly one stratum
|carryCount(x+y) − hammingDistance(x, y)|
enc where carry significance ≅ domain dependency
finite symbol set S, observed pairs (s_i, s_j)
high-significance sites → most informative observables
EncodingConfiguration over ordered domain
O(log n) via prefix computation on (g_k, p_k) pairs
guard evaluation at stage k with state s
adjacent stages k, k+1 with compatible guards
thermodynamicBudget(U) < bitsWidth(unitWittLevel(U)) × ln 2
elements a, b in division algebra at level k
elements a, b, c in division algebra at level k
Effects A, B with DisjointnessWitness(target(A), target(B))
ExternalEffect e satisfying conformance:EffectShape
DispatchTable D with isExhaustive=true, isMutuallyExclusive=true
requires eval(g, currentState) = true, then apply(e)
ReductionStep s with exitGuard g and stageEffect e
isExhaustive(D) ∧ isMutuallyExclusive(D)
ParallelProduct A ∥ B with DisjointnessCertificate
ParallelProduct A ∥ B, any interleaving σ
cert(A) ∧ cert(B) ∧ DisjointnessCertificate(A, B)
cert(f) ∧ cert(g) ∧ range(g) = domain(f)
ApplicationMorphism(partialBase(p), boundArguments(p))
PartialApplication p with remainingArity = 0
linearBudget(epoch_k) + leaseCardinality(L)
EpochBoundary b with LeaseAllocation L expiring at b
A ∥ B where result(A) = Failure, result(B) = Success
result(apply(recoveryEffect(r), failureState(f)))
LinearEffect e on site f, any subsequent effect e′
LeaseAllocation L with leaseCardinality k
remainingCount(budget before expiry) + leaseCardinality(L)
BoundedRecursion R with initialMeasure m
computable from N(C(T)) and stage k site targets
addresses accessed by resolver at stage k
surface symbol conforming to sinkType(s)
Ring operations, involutions, algebraic identities, and the dihedral symmetry group D_{2^n} generated by neg and bnot.
An operation on the ring Z/(2^n)Z. The root class for all UOR kernel operations.
A unary operation on the ring: takes one datum and produces one datum.
A binary operation on the ring: takes two datums and produces one datum.
A unary operation f such that f(f(x)) = x for all x in R_n. The two UOR involutions are neg (ring reflection) and bnot (hypercube reflection).
An algebraic identity: a statement that two expressions are equal for all inputs. The critical identity is neg(bnot(x)) = succ(x) for all x in R_n.
A group: a set with an associative binary operation, an identity element, and inverses for every element.
The dihedral group D_{2^n} of order 2^(n+1), generated by the ring reflection (neg) and the hypercube reflection (bnot). This group governs the symmetry of the UOR type space.
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/.
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}.
A record linking an op:Identity individual to a specific quantum level at which it has been verified. Non-functional: one WittLevelBinding per (Identity, WittLevel) pair verified.
A verification domain at the intersection of quantum superposition and classical thermodynamics. Identities in this domain require both SuperpositionDomain and Thermodynamic reasoning simultaneously.
Root class for validity scope individuals. Instances are the four named scope kinds: Universal, ParametricLower, ParametricRange, and LevelSpecific.
An operation formed by composing ring operations, witnessed by op:composedOf and morphism/CompositionLaw.
δ: Query × ResolverRegistry → Resolver. Non-commutative, non-associative, arity 2.
ι = P ∘ Π ∘ G (the φ-pipeline composed). Non-commutative, non-associative, arity 2.
α: Binding × Context → Context. Non-commutative, associative at convergence (SR_10), arity 2.
λ: SharedContext × ℕ → ContextLease^k. Non-commutative, non-associative, arity 2.
κ: Session × Session → Session. Commutative (disjoint leases), associative (SR_8), arity 2.
A structured group presentation: generators and relations as typed data rather than prose strings.
The number of arguments this operation takes. 1 for unary operations, 2 for binary operations.
The geometric role of this operation in the UOR ring and hypercube geometry. Functional: each operation has exactly one geometric character.
Whether this binary operation satisfies op(x,y) = op(y,x) for all x, y in R_n.
Whether this binary operation satisfies op(op(x,y),z) = op(x,op(y,z)) for all x, y, z in R_n.
The identity element of this binary operation: the value e such that op(x, e) = op(e, x) = x for all x in R_n.
The inverse operation: the operation inv_op such that op(x, inv_op(x)) = e for all x, where e is the identity.
Ordered list of operations this operation is composed from. Uses rdf:List to preserve application order (first element applied innermost). E.g., succ = neg ∘ bnot is encoded as [op:neg, op:bnot] meaning neg applied to the result of bnot.
The left-hand side of an algebraic identity as a typed AST node (schema:TermExpression).
The right-hand side of an algebraic identity as a typed AST node (schema:TermExpression).
The quantifier scope: a typed declaration of the variable(s) over which this identity holds.
An operation that generates this group. The dihedral group D_{2^n} is generated by op:neg and op:bnot.
The number of elements in the group. For D_{2^n}, the order is 2^(n+1).
The group presentation (generators and relations). Example: ⟨r, s | r^{2^n} = s² = e, srs = r⁻¹⟩
The mathematical discipline(s) through which this identity is established. Range is op:VerificationDomain. Non-functional: composite identities (e.g. IT_7a–IT_7d) reference multiple domain individuals.
Links an Identity individual to a WittLevelBinding attesting verification at a specific quantum level. Non-functional: one binding per (Identity, WittLevel) pair.
The quantum level at which this WittLevelBinding was verified.
True iff this identity holds for all n ≥ 1 (proved symbolically by induction on the ring axioms, not just exhaustively at Q0). Identities that reference 8-bit-specific constants receive universallyValid = false.
The canonical Rust enum variant name corresponding to this VerificationDomain individual. Provides formal alignment between the OWL individual and the generated Rust enum.
The structured validity scope of this identity, replacing the binary universallyValid flag. Required on all new Identity individuals.
Minimum quantum level index k for ParametricLower and ParametricRange scopes.
Maximum quantum level index k (inclusive) for ParametricRange scope.
References a constituent operation of a ComposedOperation. Non-functional: a composed operation may reference multiple constituent operations.
Human-readable type signature describing the domain and codomain of a composed operation (e.g., 'Query × Registry → Resolver').
The source selector for a dispatch operation.
The target resolver for a dispatch operation.
The source data for an inference operation.
The target type for an inference operation.
The pipeline through which inference is performed.
The base value for an accumulation operation.
The binding accumulator for an accumulation operation.
The source context for a lease partition operation.
The partition factor for a lease partition operation.
The number of partitions in a lease partition operation.
The left session in a session composition operation.
The right session in a session composition operation.
The domain type of a composed operation.
The computational complexity class of a composed operation.
Whether this composed operation is idempotent.
The number of constituent operations in a composed operation.
Whether applying this operation twice yields the identity.
Description of the convergence guarantee for this operation.
Established by exhaustive traversal of R_n. Valid for all identities where the ring is finite.
Established by equational reasoning from ring or group axioms. Covers derivations via associativity, commutativity, inverse laws, and group presentations.
Established by isometry, symmetry, or GeometricCharacter arguments. Covers dihedral actions, fixed-point analysis, automorphism groups, and affine embeddings.
Established via discrete differential calculus or metric analysis. Covers ring/Hamming derivatives (DC_), metric divergence (AM_), and adiabatic scheduling (AR_).
Established via entropy, Landauer bounds, or Boltzmann distributions. Covers site entropy (TH_), reversible computation (RC_), and phase transitions.
Established via simplicial homology, cohomology, or constraint nerve analysis. Covers homological algebra (HA_) and ψ-pipeline identities.
Established by the inter-algebra map structure of the resolution pipeline. Covers φ-maps (phi_1–phi_6) and ψ-maps (psi_1–psi_6).
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).
Established by superposition analysis of site states. Covers identities involving superposed (non-classical) site assignments where sites carry complex amplitudes.
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_).
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.
Verification domain for composed operation identities — algebraic properties of operator compositions including dispatch, inference, accumulation, lease, and session composition operations.
Holds for all k in N. No minimum k constraint.
Holds for all k >= k_min, where k_min is given by validKMin.
Holds for k_min <= k <= k_max. Both validKMin and validKMax required.
Holds only at exactly one level, given by a WittLevelBinding.
Reflection through the origin of the additive ring: neg(x) = -x mod 2^n. One of the two generators of D_{2^n}.
Reflection through the centre of the hypercube: bnot(x) = (2^n-1) ⊕ x. The second generator of D_{2^n}.
Rotation by one step: succ(x) = (x+1) mod 2^n. The composition of the two reflections.
Rotation by one step in the reverse direction: pred(x) = (x-1) mod 2^n.
Translation along the ring axis: add(x,y), sub(x,y). Preserves Hamming distance locally.
Scaling along the ring axis: mul(x,y) = (x×y) mod 2^n.
Translation along the hypercube axis: xor(x,y) = x ⊕ y. Preserves ring distance locally.
Projection onto a hypercube face: and(x,y) = x ∧ y. Idempotent; collapses dimensions.
Join on the hypercube lattice: or(x,y) = x ∨ y. Idempotent; dual to projection.
Geometric character of dispatch: constraint-guided selection over the resolver registry lattice.
Geometric character of inference: traversal through the φ-pipeline resolution graph P ∘ Π ∘ G.
Geometric character of accumulation: progressive pinning of site states in the context lattice.
Geometric character of lease partition: splitting a shared context into disjoint site-set leases.
Geometric character of session composition: merging disjoint lease sessions into a unified resolution context.
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).
Hypercube reflection: bnot(x) = (2^n - 1) ⊕ x (bitwise complement). The second generator of D_{2^n}. bnot(bnot(x)) = x.
Successor: succ(x) = neg(bnot(x)) = (x + 1) mod 2^n. The critical identity: succ is the composition neg ∘ bnot.
Predecessor: pred(x) = bnot(neg(x)) = (x - 1) mod 2^n. The inverse of succ. pred is the composition bnot ∘ neg.
Ring addition: add(x, y) = (x + y) mod 2^n. Commutative, associative; identity element is 0.
Ring subtraction: sub(x, y) = (x - y) mod 2^n. Not commutative, not associative.
Ring multiplication: mul(x, y) = (x × y) mod 2^n. Commutative, associative; identity element is 1.
Bitwise exclusive or: xor(x, y) = x ⊕ y. Commutative, associative; identity element is 0.
Bitwise and: and(x, y) = x ∧ y. Commutative, associative.
Bitwise or: or(x, y) = x ∨ y. Commutative, associative.
δ(q, R) = R(q): dispatches a query to the matching resolver in the registry. Non-commutative, non-associative.
ι(s, C) = P(Π(G(s, C))): the φ-pipeline composed into a single inference step. Non-commutative, non-associative.
α(b, C) = C': accumulates a binding into a resolution context, pinning a site. Non-commutative, associative at convergence (SR_10).
λ(S, k) = (L₁, …, Lₖ): partitions a shared context into k disjoint leases. Non-commutative, non-associative.
κ(S₁, S₂) = S₁ ∪ S₂: composes two sessions with disjoint leases into one. Commutative, associative (SR_8).
The foundational theorem of the UOR kernel: neg(bnot(x)) = succ(x) for all x in R_n. This identity links the two involutions (neg and bnot) to the successor operation, making succ derivable from neg and bnot.
Addressing bijection: addresses(glyph(d)) = d. Round-trip from datum through glyph and back is identity.
Embedding coherence: glyph(ι(addresses(a))) = ι_addr(a). The addressing diagram commutes through embeddings.
Additive associativity: add(x, add(y, z)) = add(add(x, y), z).
Additive commutativity: add(x, y) = add(y, x).
Subtraction definition: sub(x, y) = add(x, neg(y)).
Multiplicative associativity: mul(x, mul(y, z)) = mul(mul(x, y), z).
Multiplicative commutativity: mul(x, y) = mul(y, x).
Distributivity: mul(x, add(y, z)) = add(mul(x, y), mul(x, z)).
XOR associativity: xor(x, xor(y, z)) = xor(xor(x, y), z).
AND associativity: and(x, and(y, z)) = and(and(x, y), z).
OR associativity: or(x, or(y, z)) = or(or(x, y), z).
AND distributes over OR: and(x, or(y, z)) = or(and(x, y), and(x, z)).
De Morgan 1: bnot(and(x, y)) = or(bnot(x), bnot(y)).
De Morgan 2: bnot(or(x, y)) = and(bnot(x), bnot(y)).
Neg via subtraction: neg(x) = sub(0, x).
Complement via XOR: bnot(x) = xor(x, 2^n - 1).
Pred via subtraction: pred(x) = sub(x, 1).
Neg-bnot bridge: neg(x) = add(bnot(x), 1).
Complement predecessor: bnot(x) = pred(neg(x)).
XOR-add bridge: xor(x, y) = add(x, y) - 2 * and(x, y) (in Z before mod).
Conjugation: neg(succ(neg(x))) = pred(x).
Reverse composition: bnot(neg(x)) = pred(x).
Group closure: D_[2^n] = [succ^k, neg ∘ succ^k : 0 ≤ k < 2^n].
Unit group decomposition: R_n× ≅ Z/2 × Z/2^[n-2] for n ≥ 3.
Unit group special cases: R_1× ≅ [1]; R_2× ≅ Z/2.
Multiplicative order: ord(u) = lcm(ord((-1)^a), ord(3^b)).
Resonance period: ord_g(2) divides φ(g).
Step formula derivation: step_g = 2 * ((g - (2^n mod g)) mod g) + 1.
Scaling not dihedral: μ_u ∉ D_[2^n] for u ≠ ±1.
Affine group order: |Aff(R_n)| = 2^[2n-1].
Subgroup inclusion: D_[2^n] ⊂ Aff(R_n) with u ∈ [±1].
Addition decomposition: add(x,y)_k = xor(x_k, xor(y_k, c_k(x,y))).
Carry recurrence: c_[k+1](x,y) = or(and(x_k,y_k), and(xor(x_k,y_k), c_k)).
Zero carry: c(x, 0) = 0 at all positions.
Negation carry: c(x, neg(x))_k = 1 for k > v_2(x).
Carry-incompatibility link: d_Δ(x, y) > 0 iff ∃ k : c_k(x,y) = 1.
Constraint pin union: pins of a composite constraint equal the union of component pins.
Constraint composition identity element.
Constraint-depth invariant: carry complexity of the residue representation equals the type depth.
Constraint quotient lattice isomorphism to power set.
Lattice join equals constraint composition.
Lattice meet pins the intersection of component pins.
Constraint lattice complement existence.
Minimal cover via greedy irredundant removal.
Minimum constraint count to cover n sites.
Residue constraint cost is the step formula.
Carry constraint cost is the popcount of the pattern.
Depth constraint cost is sum of residue and carry costs.
Composite constraint cost is subadditive.
Optimal resolution order is increasing cost.
Site monotonicity: a pinned site cannot be unpinned.
Site budget upper bound: at most n pin operations to close.
Site budget conservation: pinned + free = total sites.
Site budget closure: closed iff all sites pinned.
Unit partition membership: x is a unit iff site_0(x) = 1 (x is odd).
Exterior partition membership: x is exterior iff x is not in the carrier of T.
Irreducible partition membership: x is irreducible iff x is not a unit, exterior, or reducible.
Reducible partition membership: x is reducible iff x is not a unit, exterior, or irreducible.
2-adic decomposition: every element factors as 2^{v(x)} times an odd unit.
Site extraction: site_k(x) is the k-th bit of x.
Progressive site determination: site_k given lower sites determines x mod 2^{k+1}.
Cumulative site determination: sites 0..k together determine x mod 2^{k+1}.
Complete site determination: all n sites determine x uniquely.
Stratum from sites: v_2(x) is the minimum k where site_k(x) = 1.
Depth bound: depth(x) ≤ v_2(x) for irreducible elements.
Resolution strategy equivalence: dihedral, canonical-form, and evaluation resolvers all compute the same partition.
Resolution monotonicity: pinned count never decreases.
Resolution convergence bound: at most n iterations.
Resolution termination: loop terminates if constraint set spans all sites.
Optimal resolution level for a factor: n ≡ 0 (mod ord_g(2)).
Constraint ordering by step cost: smaller step_g first.
Resolution determinism: same type and constraint sequence yield unique partition.
Order independence: complete constraint sets yield the same partition regardless of order.
Evaluation resolver directly computes the set-theoretic partition.
Dihedral factorization resolver yields the same partition via orbit decomposition.
Canonical form resolver yields the same partition via confluent rewrite.
All three strategies compute the same set-theoretic partition.
Benefit of a constraint is the number of new pins it provides.
Constraint cost is step or popcount depending on type.
Greedy selection maximizes benefit-to-cost ratio.
Greedy approximation achieves (1 − 1/e) ≈ 63% of optimal.
Tiebreaker: prefer vertical (residue) before horizontal (carry).
Minimum convergence rate: 1 site per iteration (worst case).
Maximum convergence rate: n sites in 1 iteration (best case).
Expected residue constraint rate: ⌊log_2(m)⌋ sites per constraint.
Stall detection: convergenceRate < 1 for 2 iterations suggests insufficiency.
Sufficiency criterion: pin union covers all site positions.
Iteration bound for k constraints: at most min(k, n) iterations.
Incompatibility metric is the absolute difference of ring and Hamming metrics.
Bitwise complement preserves Hamming metric.
Successor preserves ring metric but may change Hamming metric.
Negation-complement commutator is constant 2.
Additive paths have trivial monodromy (abelian ⇒ path-independent).
Dihedral generator paths have monodromy in D_{2^n}.
Successor-only closed path winding number.
Path length is additive under concatenation.
Total variation is subadditive under concatenation.
Reduction length is additive under sequential composition.
Odd prime catastrophe transitions visibility via residue constraints.
Catastrophe threshold is normalized step cost.
Composite catastrophe threshold is max of component thresholds.
Curvature flux is the sum of incompatibility along a path.
Resolution cost is bounded below by curvature flux of optimal path.
Successor curvature flux: trailing_ones(x) for most x, n−1 at maximum.
Total successor curvature flux over R_n equals 2^n − 2.
Additive holonomy is trivial (abelian group).
Dihedral generator holonomy group is D_{2^n}.
Unit multiplication holonomy equals the unit group.
Full holonomy group is the affine group.
Holonomy group decomposition into dihedral and non-trivial units.
Category left identity: compose(id, f) = f.
Category right identity: compose(f, id) = f.
Category associativity of transform composition.
Composability condition: f composesWith g iff target(f) = source(g).
Bitwise complement is a Hamming-metric isometry.
Successor as composed isometries: succ = neg ∘ bnot preserves d_R but not d_H.
Ring isometries form a group under composition.
CurvatureObservable measures failure of ring isometry to be Hamming isometry.
Embedding transitivity: composition of embeddings is an embedding.
Embedding address coherence: glyph ∘ ι ∘ addresses is well-defined.
Dihedral group acts on constraints by transforming them.
Dihedral group action on partitions permutes components.
Dihedral orbits determine irreducibility boundaries.
Fixed points of negation are {0, 2^{n−1}}; bnot has no fixed points.
Automorphism group consists of unit multiplications.
Automorphism group is isomorphic to the unit group.
Intersection of automorphism group with dihedral group is {id, neg}.
Affine group is generated by D_{2^n} and μ_3.
Embedding functor preserves composition.
Embedding functor composition is functorial.
Embedding functor preserves ring isometries.
Embedding functor maps dihedral subgroup into target dihedral group.
Embedding functor maps unit group into target unit group.
Braille glyph encoding: 6-bit blocks to Braille characters.
Braille XOR homomorphism: Braille encoding commutes with XOR.
Braille complement: glyph of bnot(x) is character-wise complement of glyph(x).
Addition does not lift to address space: no glyph homomorphism for add.
Liftable operations are exactly the Boolean operations.
Negation decomposes into liftable bnot and non-liftable succ.
Address metric is sum of per-character Hamming distances.
Address metric equals Hamming metric on ring elements.
Address metric does not preserve ring metric in general.
Maximum entropy: unconstrained state has S = n × ln 2.
Zero entropy: fully resolved state has S = 0.
Landauer bound on total resolution cost.
Critical inverse temperature for UOR site system.
Constraint application removes entropy; convergence rate equals cooling rate.
CatastropheThreshold is the temperature of a partition phase transition.
Step formula as free-energy cost of a constraint boundary.
Computational hardness maps to type incompleteness (high temperature).
Type resolution is measurement; cost ≥ entropy removed.
Adiabatic schedule: decreasing freeRank, cost-per-site ordering.
Adiabatic cost is sum of constraint costs in optimal order.
Adiabatic cost satisfies Landauer bound.
Greedy vs adiabatic cost difference: ≤ 5% for n ≤ 16.
Phase boundaries occur where g divides 2^n − 1 or g is a power of 2.
Parity boundary divides R_n into equal halves.
Phase count at level n is at most 2^n (typically O(n)).
Reversible pinning stores prior state in ancilla site.
Reversible pinning has zero total entropy change.
Deferred Landauer cost at ancilla erasure.
Reversible total cost equals irreversible total cost (redistributed).
Quantum UOR: superposed sites, cost proportional to winning path.
Ring derivative: ∂_R f(x) = f(succ(x)) - f(x).
Hamming derivative: ∂_H f(x) = f(bnot(x)) - f(x).
Hamming derivative of identity: ∂_H id(x) = -(2x + 1) mod 2^n.
Commutator from derivatives: [neg, bnot](x) = ∂_R neg(x) - ∂_H neg(x).
Carry dependence: the difference ∂_R f - ∂_H f decomposes into carry contributions.
Jacobian definition: J_k(x) = ∂_R f_k(x) where f_k = site_k.
Top-site anomaly: J_{n-1}(x) may differ from lower sites.
Rank-curvature identity: rank(J(x)) = d_H(x, succ(x)) - 1 for generic x.
Total curvature from Jacobian: κ(x) = Σ_k J_k(x).
Curvature-weighted ordering: optimal next constraint maximizes J_k over free sites.
Curvature equipartition: Σ_{x} J_k(x) ≈ (2^n - 2)/n for each k.
Constraint nerve: N(C) is the simplicial complex on constraints.
Stall iff non-trivial homology: resolution stalls ⟺ H_k(N(C)) ≠ 0 for some k > 0.
Betti-entropy theorem: S_residual ≥ Σ_k β_k × ln 2.
Euler-Poincaré formula for constraint nerve.
Spectral gap bounds convergence rate from below.
UOR index theorem (topological form): total curvature minus Euler characteristic equals residual entropy in bits.
UOR index theorem (entropy-topology duality).
UOR index theorem (spectral cost bound): resolution cost ≥ n - χ(N(C)).
UOR index theorem (completeness criterion): resolution is complete iff χ(N(C)) = n and all Betti numbers vanish.
Ring → Constraints map: negation transforms a residue constraint.
Constraints → Sites map: composition maps to union of site pinnings.
Sites → Partition map: a closed site state determines a unique 4-component partition.
Resolution pipeline: φ₄ = φ₃ ∘ φ₂ ∘ φ₁ is the composite resolution map.
Operations → Observables map: negation preserves d_R, may change d_H.
Observables → Refinement map: observables on a state yield a refinement suggestion.
ψ_1: Constraints → SimplicialComplex (nerve construction). Maps a set of constraints to its nerve simplicial complex.
ψ_2: SimplicialComplex → ChainComplex (chain functor). Maps a simplicial complex to its chain complex.
ψ_3: ChainComplex → HomologyGroups (homology functor). Computes homology groups from a chain complex.
ψ_5: ChainComplex → CochainComplex (dualization functor). Dualizes a chain complex to obtain a cochain complex.
ψ_6: CochainComplex → CohomologyGroups (cohomology functor). Computes cohomology groups from a cochain complex.
The dihedral group of order 2^(n+1), generated by neg (ring reflection) and bnot (hypercube reflection). Every element of this group acts as an isometry on the type space 𝒯_n.
The Surface Symmetry Theorem: the composite P∘Π∘G is a well-typed morphism iff G and P share the same state:Frame F. When the shared-frame condition holds, the output lands in the type-equivalent neighbourhood of the source symbol.
Completeness implies O(1) resolution: a CompleteType T satisfies ∀ x ∈ R_n, resolution(x, T) terminates in O(1).
Completeness is monotone: if T ⊆ T' (T' has more constraints), then completeness(T) implies completeness(T').
Witness composition: concat(W₁, W₂) is a valid audit trail iff W₁.sitesClosed + W₂.sitesClosed = n.
The CompletenessResolver is the unique fixed point of the ψ-pipeline applied to a CompletenessCandidate.
CompletenessCertificate soundness: cert.verified = true implies χ(N(C)) = n and for all k: β_k = 0.
neg(bnot(x)) = succ(x) holds in Z/(2ⁿ)Z for all n ≥ 1. Universal form of the Critical Identity across all quantum levels.
The dihedral group D_{2ⁿ} generated by neg and bnot has order 2ⁿ⁺¹ for all n ≥ 1.
The reduction distribution P(j) = 2^{-j} is the Boltzmann distribution at β* = ln 2 for all n ≥ 1.
The site budget of a PrimitiveType at quantum level n is exactly n (one site per bit).
Resolution complexity for a CompleteType is O(1) for all n ≥ 1.
Content addressing is a bijection for all n ≥ 1 (AD_1/AD_2 universality).
The ψ-pipeline produces a valid ChainComplex for any ConstrainedType at any quantum level n ≥ 1.
Binding monotonicity: freeRank(B_{i+1}) ≤ freeRank(B_i) for all i in a Session.
Binding soundness: a Binding b is sound iff b.datum resolves under b.constraint in O(1).
Session convergence: a Session S converges iff there exists i such that freeRank(B_i) = 0.
Context reset isolation: bindings in C_fresh are independent of bindings in C_prior after a SessionBoundary.
Contradiction detection: ContradictionBoundary fires iff there exist bindings b, b' with the same address, different datum, under the same constraint.
Nerve realisability: for any target (χ*, β₀* = 1, β_k* = 0 for k ≥ 1) with χ* ≤ n, there exists a ConstrainedType T over R_n whose constraint nerve realises the target.
Minimal basis bound: for the IT_7d target (χ* = n, all β* = 0), the MinimalConstraintBasis has size exactly n (one constraint per site position). No redundant constraints exist in the minimal basis.
Synthesis monotonicity: adding a constraint to a synthesis candidate never decreases the Euler characteristic of the resulting nerve (χ is monotone non-decreasing under constraint addition).
Synthesis convergence: the TypeSynthesisResolver terminates for any realisable target in at most n constraint additions (for n-site types).
Synthesis–certification duality: a SynthesizedType T achieves the IT_7d target if and only if the CompletenessResolver certifies T as a CompleteType. The forward ψ-pipeline and the inverse TypeSynthesisResolver are dual computations.
Jacobian-guided synthesis efficiency: using the Jacobian (DC_10) to select the next constraint reduces the expected number of synthesis steps from O(n²) (uninformed) to O(n log n) (Jacobian-guided).
Unreachable signatures: a Betti profile with β₀ = 0 is unreachable by any non-empty ConstrainedType — the nerve of a non-empty constraint set is always connected (β₀ ≥ 1).
Lift unobstructedness criterion: WittLift T' is a CompleteType iff the spectral sequence E_r^{p,q} collapses at E_2 (d_2 = 0 and all higher differentials zero).
Obstruction localisation: a non-trivial LiftObstruction is localised to a specific site at bit position n+1. The obstruction class lives in H²(N(C(T))) and is killed by adding one constraint involving the new site.
Monotone lifting for trivially obstructed types: if T is a CompleteType at Q_n and its constraint set is closed under the Q_{n+1} extension map, then T' is a CompleteType at Q_{n+1} with basisSize(T') = basisSize(T) + 1.
Spectral sequence convergence bound: for constraint configurations of homological depth d (H_k(N(C(T))) = 0 for k > d), the spectral sequence converges by page E_{d+2}.
Universal identity preservation: every op:universallyValid identity holds in ℤ/(2^{n+1})ℤ with the lifted constraint set. The lift does not invalidate any certified universal identity.
ψ-pipeline universality for quantum lifts: the ψ-pipeline produces a valid ChainComplex for any WittLift T' — the chain complex of T' restricts to the chain complex of T on the base nerve, and the extension is well-formed by construction.
Holonomy group containment: HolonomyGroup(T) ≤ D_{2^n} for all ConstrainedTypes T over R_n. The holonomy group is always a subgroup of the full dihedral group.
Additive flatness (extends OB_H1): if all constraints in T are additive (ResidueConstraint or DepthConstraint type), then HolonomyGroup(T) = {id} — T is a FlatType.
Dihedral generation: if T contains both a neg-related and a bnot-related constraint in a common closed path, then HolonomyGroup(T) = D_{2^n} — T has full dihedral holonomy.
Holonomy-Betti implication: HolonomyGroup(T) ≠ {id} ⟹ β₁(N(C(T))) ≥ 1. Non-trivial monodromy requires a topological loop. (Converse is false: β₁ ≥ 1 does not imply non-trivial holonomy.)
CompleteType holonomy: a CompleteType (IT_7d: χ = n, all β = 0) has trivial holonomy. IT_7d implies FlatType because IT_7d requires β₁ = 0, which by MN_4 implies trivial monodromy.
Monodromy composition: if p₁ and p₂ are closed constraint paths, then monodromy(p₁ · p₂) = monodromy(p₁) · monodromy(p₂) in D_{2^n} (group homomorphism from loops to dihedral elements).
TwistedType obstruction class: the monodromy of a TwistedType contributes a non-zero class to H²(N(C(T')); ℤ/2ℤ) where T' is any WittLift of T. TwistedTypes always have non-trivial lift obstructions.
Product type site additivity: siteBudget(A × B) = siteBudget(A) + siteBudget(B).
Product type partition product: partition(A × B) = partition(A) ⊗ partition(B).
Product type Euler additivity: χ(N(C(A × B))) = χ(N(C(A))) + χ(N(C(B))).
Product type entropy additivity: S(A × B) = S(A) + S(B).
Sum type site budget: siteBudget(A + B) = max(siteBudget(A), siteBudget(B)).
Sum type entropy: S(A + B) = ln 2 + max(S(A), S(B)).
Context temperature: T_ctx(C) = freeRank(C) × ln 2 / n.
Grounding degree: σ(C) = (n − freeRank(C)) / n.
Grounding monotonicity: σ(B_{i+1}) ≥ σ(B_i) for all i in a Session.
Ground state equivalence: σ(C) = 1 ↔ freeRank(C) = 0 ↔ S(C) = 0 ↔ T_ctx(C) = 0.
O(1) resolution guarantee: freeRank(C) = 0 ∧ q.address ∈ bindings(C) → stepCount(q, C) = 0.
Pre-reduction of effective budget: effectiveBudget(q, C) = max(0, siteBudget(q.type) − |pinnedSites(C) ∩ q.siteSet|).
Thermodynamic cooling cost: Cost_saturation(C) = n × k_B T × ln 2.
Connectivity lower bound: β₀(N(C)) ≥ 1 for all non-empty C.
Euler capacity ceiling: χ(N(C)) ≤ n for all C at quantum level n.
Betti monotonicity under addition: χ(N(C + c)) ≥ χ(N(C)) for any constraint c added to C.
Level-relative achievability: a signature achievable at quantum level n remains achievable at level n+1.
Empirical completeness convergence: verified SynthesisSignature individuals converge to the exact morphospace boundary.
Geodesic condition: a ComputationTrace is a geodesic iff its steps are AR_1-ordered and each step selects the constraint maximising J_k over free sites (DC_10).
Geodesic entropy bound: ΔS_step(i) = ln 2 for every step i of a geodesic trace.
Total geodesic cost: Cost_geodesic(T) = freeRank_initial × k_B T ln 2 = TH_4.
Geodesic uniqueness up to step-order equivalence: all geodesics for the same ConstrainedType share stepCount and constraint set.
Subgeodesic detectability: a trace is sub-geodesic iff ∃ step i where J_k(step_i) < max_{free sites} J_k(state_i).
Von Neumann–Landauer bridge: S_vonNeumann(ψ) = Cost_Landauer(collapse(ψ)).
Measurement as site topology change: projective collapse on a SuperposedSiteState is topologically equivalent to applying a ResidueConstraint that pins the collapsed site.
Superposition entropy bound: 0 ≤ S_vN(ψ) ≤ ln 2 for any single-site SuperposedSiteState.
Collapse idempotence: collapse(collapse(ψ)) = collapse(ψ). Measurement on an already-collapsed state is a no-op.
Amplitude normalization (Born rule): the sum of squared amplitudes equals 1 for any well-formed SuperposedSiteState.
Amplitude renormalization: a SuperposedSiteState can always be normalized to satisfy QM_5.
Partition exhaustiveness: the four component cardinalities sum to the ring size.
Exterior membership criterion: x is exterior iff x is not in the carrier of T.
Holonomy classification covering: every ConstrainedType with a computed holonomy group is either flat or twisted, not both.
Witt level chain inverse: wittLevelPredecessor is the left inverse of nextWittLevel.
Dihedral composition rule: (rᵃ sᵖ)(rᵇ sᵠ) = r^(a + (-1)ᵖ b mod 2ⁿ) s^(p xor q).
Classical embedding: superposition resolution of a classical (non-superposed) datum reduces to classical resolution.
Collapse–resolve commutativity: collapsing then resolving classically equals resolving in superposition then collapsing.
Amplitude preservation: the SuperpositionResolver preserves the normalized amplitude vector during ψ-pipeline traversal.
Born rule outcome probability: the probability of collapsing to site k equals the squared amplitude of that site.
Product type partition tensor: the partition of a product type is the tensor product of the component partitions.
Sum type partition coproduct: the partition of a sum type is the coproduct of the variant partitions.
Geodesic predicate decomposition: a trace is geodesic iff it is both AR_1-ordered and DC_10-selected.
LiftChain(Q_j, Q_k) is valid CompleteType tower iff every chainStep WittLift has trivial or resolved LiftObstruction.
Obstruction count bound: the number of non-trivial LiftObstructions in a chain is at most the chain length.
Resolved basis size formula: the basis size at Q_k equals basisSize(Q_j) + chainLength + obstructionResolutionCost.
Flat tower characterization: isFlat(chain) iff obstructionCount = 0 iff HolonomyGroup trivial at every step.
LiftChainCertificate existence: a CompleteType at Q_k satisfies IT_7d with a witness chain.
Single-step reduction: QT_3 with chainLength=1 and cost=0 reduces to QLS_3.
Flat chain basis size: for flat chains, resolvedBasisSize(Q_k) = basisSize(Q_j) + (k - j).
Carry-constraint site-pinning map: pinsSites(CarryConstraint(p)) equals the set of bit positions where p has a 1 plus the first-zero stopping position.
Carry-constraint cost-to-site count: the number of sites pinned by a CarryConstraint equals popcount plus one for the stopping position.
CRT joint satisfiability: two ResidueConstraints are jointly satisfiable iff the gcd of their moduli divides the difference of their residues.
Carry-residue joint satisfiability: a CarryConstraint and ResidueConstraint are jointly satisfiable iff the carry-pinned sites are compatible with the residue class.
Carry-carry joint satisfiability: two CarryConstraints are jointly satisfiable iff their bit-patterns have no conflicting positions.
Dihedral inverse formula: the inverse of r^a s^p in D_(2^n) is r^(-(−1)^p a mod 2^n) s^p.
Dihedral reflection order: every reflection element r^k s^1 in D_(2^n) has order 2.
Monotone carrier characterization: a ConstrainedType has an upward-closed carrier iff every ResidueConstraint has residue = modulus - 1 and no CarryConstraint or DepthConstraint appears.
Monotone constraint count: the number of expressible monotone ConstrainedTypes at quantum level Q_n is 2^n, corresponding to the principal filter count.
SumType carrier semantics: the carrier of a SumType is the coproduct (disjoint union) of component carriers, not the set-theoretic union.
SumType Euler characteristic additivity: for a SumType with topologically disjoint component nerves, the Euler characteristic is additive.
SumType Betti number additivity: for disjoint component nerves, all Betti numbers are additive.
SumType completeness transfer: a SumType A+B is CompleteType iff both A and B are CompleteType and they have equal quantum levels.
Betti-1 minimum constraint count: the minimum number of constraints needed to achieve first Betti number beta_1 = k in the constraint nerve is 2k + 1.
TypeSynthesisResolver termination: the resolver terminates in at most 2^n steps for any target signature at quantum level Q_n, returning either a ConstrainedType or a ForbiddenSignature certificate.
ForbiddenSignature membership criterion: a topological signature is a ForbiddenSignature iff no ConstrainedType with at most n constraints realises it at quantum level Q_n.
ObstructionChain length bound: the length of the ObstructionChain from Q_j to Q_k is at most (k-j) times C(basisSize(Q_j), 3).
TowerCompletenessResolver termination: the resolver terminates for any finite LiftChain within the QT_8 bound, producing a CompleteType certificate or a bounded ObstructionChain.
Standard coefficient ring: the coefficient ring for all psi-pipeline cohomology computations in uor.foundation is Z/2Z, consistent with MN_7.
GluingObstruction feedback: given a GluingObstruction class in H^1(N(C)), the killing RefinementSuggestion adds a constraint whose pinned sites contain the intersection of the cycle-generating pair.
Grounding re-entry free rank: for a session at full grounding, a new query q has freeRank equal to the number of q's site coordinates not already bound.
Grounding degree degradation: after re-entry with query q, the grounding degree becomes min(current sigma, 1 - freeRank(q)/n).
Amplitude index set characterization: the amplitude index set of a SuperposedSiteState over ConstrainedType T at Q_n is the set of monotone pinning trajectories consistent with T's constraints.
Certificate issuance: every valid Transform admits a TransformCertificate attesting correct source-to-target mapping.
Certificate issuance: every metric-preserving Transform admits an IsometryCertificate attesting distance preservation.
Certificate issuance: every involutive operation f where f(f(x)) = x admits an InvolutionCertificate.
Certificate issuance: full saturation (σ = 1, freeRank = 0) admits a GroundingCertificate.
Certificate issuance: an AR_1-ordered and DC_10-selected trace admits a GeodesicCertificate.
Certificate issuance: a MeasurementEvent verifying the von Neumann–Landauer bridge at β* = ln 2 admits a MeasurementCertificate.
Certificate issuance: a MeasurementEvent verifying P(outcome k) = |α_k|² admits a BornRuleVerification certificate.
Certificate issuance: shared-frame grounding that lands in the type-equivalent neighbourhood admits a GroundingCertificate.
Session composition validity: compose(S_A, S_B) is valid at Q_k iff all pinned-site intersections agree at every tower level Q_0 through Q_k.
ContextLease disjointness: two distinct leases on the same SharedContext have non-overlapping site sets.
ExecutionPolicy confluence: different execution policies on the same pending query set produce the same final resolved state (Church-Rosser for session resolution).
Lease partition conserves total budget: the sum of freeRank over all leases equals the SharedContext freeRank.
Per-lease binding monotonicity: within a leased sub-domain, freeRank decreases monotonically (SR_1 restricted to lease).
General composition freeRank via inclusion-exclusion.
Disjoint-lease composition is additive: the intersection term vanishes when leases are site-disjoint (SR_9).
Policy-invariant final binding set: different execution policies produce identical SiteBinding records.
Full lease coverage implies composed saturation: k sessions on disjoint covering leases, each locally converged, produce a GroundedContext via composition.
Distributed O(1) resolution: a query against a composed GroundedContext resolves in zero steps.
Parallelism bound: per-session resolution work is bounded by lease size, not by total site count n.
Witt coordinate identification: the bit coordinates (x_0, …, x_[n−1]) of x ∈ Z/(2ⁿ)Z are exactly its Witt coordinates under the canonical isomorphism W_n(F_2) ≅ Z/(2ⁿ)Z.
Witt sum correction equals carry: the k-th Witt addition polynomial correction term S_k − x_k − y_k (mod 2) is exactly the carry c_k(x,y).
Carry recurrence is the Witt polynomial recurrence: CA_2 implements the ghost equation for S_[k+1] at p=2.
The δ-correction at level k equals the single-level carry c_[k+1](x,y). Each application of δ divides by 2, consuming one unit of 2-adic valuation.
LiftObstruction is equivalent to δ-nonvanishing: a nontrivial LiftObstruction at Q_[k+1] means δ_k ≠ 0 for some element pair.
Metric discrepancy equals Witt defect: d_Δ(x,y) > 0 iff the ghost map correction (carry) is nonzero.
D_1 is the Witt truncation order relation: succ^[2ⁿ](x) = x is the group relation r^[2ⁿ] = 1 in the Witt-Burnside ring of D_[2∞].
D_3 is the Witt-Burnside conjugation relation: neg(succ(neg(x))) = pred(x) is srs = r⁻¹ in the pro-dihedral group.
D_4 is a Witt-Burnside reflection composition: bnot(neg(x)) = pred(x) is the product of two reflections yielding inverse rotation.
The δ-ring Frobenius lift on W_n(F_2) is the identity map because F_2 is a perfect field of characteristic 2 (a² = a for a ∈ F_2).
The Verschiebung on W_n(F_2) is multiplication by 2: V(x) = 2x = add(x,x). This is a coordinate shift with zero Witt defect.
The δ-operator on W_n(F_2) is the squaring defect divided by 2: δ(x) = (x − mul(x,x)) / 2. Expressible entirely in existing op/ primitives (sub, mul, arithmetic right shift).
Ostrowski product formula at p=2: |2|_2 · |2|_∞ = 1. The 2-adic and Archimedean absolute values of 2 are multiplicative inverses.
Crossing cost equals ln 2: the Archimedean image of one unit of 2-adic valuation, under the product formula, is ln 2 nats.
QM_1 grounding: the Landauer cost β* = ln 2 is the crossing cost from OA_2, derived from the prime p=2 that structures the Witt tower.
Born rule bridge (conditional on amplitude rationality): P(outcome k) = |α_k|_∞², where |·|_∞ is the Archimedean image of the 2-adic amplitude via the product formula.
Entropy per δ-level equals the crossing cost: each application of the δ-operator (division by 2) costs ln 2 nats in the Archimedean completion, which is the per-bit Landauer cost.
KanComplex(N(C)) — the constraint nerve satisfies the Kan extension condition for all horns of dimension ≤ d where d is the maximum simplex dimension of N(C).
Path components of nerve recover β₀: π₀(N(C)) ≅ Z^{β₀} counts the connected components of the constraint configuration.
MN_6 monodromy is abelianisation of full π₁: the fundamental group π₁(N(C)) surjects onto the HolonomyGroup D_{2^n} via abelianisation.
Higher homotopy groups vanish above nerve dimension: π_k(N(C)) = 0 for all k > dim(N(C)), because the nerve is a finite CW-complex.
1-truncation determines flat/twisted classification: τ_{≤1}(N(C)) captures the holonomy action that distinguishes FlatType from TwistedType.
Trivial k-invariants beyond depth d imply spectral collapse: if κ_k is trivial for all k > d then the spectral sequence collapses at E_{d+2}.
Non-trivial Whitehead product implies lift obstruction: [α, β] ≠ 0 in π_{p+q−1} implies a non-trivial LiftObstruction that Betti numbers alone cannot detect.
Hurewicz isomorphism for first non-vanishing group: π_k(N(C)) ⊗ Z ≅ H_k(N(C); Z) for the smallest k with π_k ≠ 0, linking homotopy invariants to homology.
ψ_7: KanComplex → PostnikovTower — compute the Postnikov truncations τ_{≤k} for k = 0, 1, …, dim(N(C)).
ψ_8: PostnikovTower → HomotopyGroups — extract the homotopy groups π_k from each truncation stage.
ψ_9: HomotopyGroups → KInvariants — compute the k-invariants κ_k classifying the Postnikov tower.
Pipeline composition: nerve construction + Kan promotion = ψ_7 ∘ ψ_1.
Homotopy extraction agrees with homology on k-skeleton.
k-invariant computation detects QLS_4 convergence.
Complexity bound for homotopy type computation.
Moduli space dimension equals basis size of any contained type.
Zeroth deformation cohomology = automorphism group intersected with dihedral group.
First deformation cohomology = tangent space to the moduli space at T.
Second deformation cohomology = LiftObstruction space.
FlatType stratum has codimension zero in the moduli space.
TwistedType stratum has codimension at least 1.
VersalDeformation existence is guaranteed when the obstruction space H² vanishes.
A deformation family preserves completeness iff H²(Def(T_t)) = 0 along the entire path.
The site of a ModuliTowerMap at T has dimension 1 when the obstruction is trivial.
The site of a ModuliTowerMap at T is empty iff T is a TwistedType at every level.
ModuliResolver boundary agrees with MorphospaceBoundary.
StratificationRecord covers every CompleteType in exactly one stratum.
Achievable signatures correspond to membership in some HolonomyStratum.
Carry generates at site k iff and(x_k, y_k) = 1. Extends CA_1 (addition decomposition) and WC_2 (Witt sum correction).
Carry propagates at site k iff xor(x_k, y_k) = 1 and c_k = 1. Extends CA_2 (carry recurrence) and WC_3 (Witt polynomial recurrence).
Carry kills at site k iff and(x_k, y_k) = 0 and xor(x_k, y_k) = 0. Complement of CY_1 and CY_2.
d_Δ(x,y) = |carryCount(x+y) − hammingDistance(x,y)|. The metric incompatibility IS the discrepancy between carry count and Hamming distance. Strengthens WC_6.
Optimal encoding theorem: the encoding that minimizes Σ d_Δ over observed pairs is the one where the carry chain’s significance hierarchy matches the domain’s dependency structure.
Site ordering theorem: d_Δ is minimized when high-significance sites (upstream in the carry chain) encode the most structurally informative observables.
Carry lookahead: the carry chain for n sites is computable in O(log n) using prefix computation on generate/propagate pairs.
σ(C) = (n − freeRank(C)) / n. The saturation metric is the complement of free site ratio. Derives from SC_2.
χ = Σ(−1)^k β_k. The Euler characteristic of the constraint nerve. Derives from IT_2.
Index theorem: Σκ_k − χ = S_residual / ln 2. Links all six metrics. Derives from IT_7a.
J_k = 0 for pinned sites. The Jacobian vanishes on resolved sites.
d_Δ > 0 iff carry ≠ 0. The metric discrepancy equals the Witt defect. Derives from WC_6.
Metric composition tower: d_Δ → {σ, J_k} → β_k → χ → r. Each metric derives from previous ones.
σ = lower adjoint evaluated at current type. The saturation metric is the lower adjoint of the Galois connection. Derives from SC_2.
r = complement of upper adjoint image. The residual freedom is what the type closure does not reach.
CompleteType = fixpoint of Galois connection, σ=1, r=0. Derives from IT_7d.
Type refinement = ascending in type lattice = descending in site freedom. The Galois connection reverses order.
nerve(C₁ ∪ C₂) = nerve(C₁) ∪ nerve(C₂) for disjoint constraint domains.
Mayer–Vietoris: β_k(C₁ ∪ C₂) computable from parts and intersection.
Single constraint addition: Δβ_k ∈ {−1, 0, +1} per dimension.
Constraint accumulation monotonicity: β_k non-increasing under SR_1. Derives from SR_1.
ScalarType grounding: quantize(value, range, bits) produces ring element where d_R reflects value proximity.
SymbolType grounding: argmin_{encoding} Σ d_Δ over observed pairs (CY_5).
SequenceType = free monoid on element type with backbone constraint.
TupleType site count = Σ field site counts, site ordering follows CY_6.
GraphType constraint nerve = graph nerve, β_k equality.
SetType d_Δ invariant under element permutation, D_{2n} symmetry.
TreeType β_1=0, β_0=1 topological constraints.
TableType = SequenceType(TupleType(S)), functorial decomposition.
Dispatch determinism: same query and same registry always yield the same resolver.
Dispatch coverage: every query in the registry domain has a matching resolver.
Inference idempotence: ι(ι(s,C),C) = ι(s,C) on GroundedContext.
Inference soundness: ι(s,C) resolves to a type consistent with C.
Inference composition: ι = P ∘ Π ∘ G (references phi_4).
Inference complexity: O(n) worst case, O(1) on CompleteType.
Inference coherence: roundTrip(P(Π(G(s)))) = s.
Accumulation permutation invariance: accumulating bindings in any order yields the same saturated context (derives from SR_10).
Accumulation monotonicity: α(b,C) ⊇ C (the context only grows, never loses bindings). Derives from SR_1.
Accumulation soundness: α(b,C) preserves all previously satisfied constraints. Derives from SR_2.
Accumulation base preservation: α does not modify previously pinned sites.
Lease disjointness: partitioned leases have pairwise disjoint site sets (derives from SR_9).
Lease conservation: union of all leases equals the original shared context (derives from MC_1).
Lease coverage: every site in the shared context appears in exactly one lease (derives from MC_6).
Composition validity: κ(S₁,S₂) is a valid session if S₁,S₂ have disjoint leases (derives from SR_8).
Distributed resolution: resolving in κ(S₁,S₂) equals resolving in S₁ or S₂ independently (derives from MC_7).
Pipeline unification: κ(λₖ(α*(ι(s,·))),C) = resolve(s,C). The full composed pipeline equals the top-level resolution function.
Stage 1 dispatches resolver (δ selects).
Stage 2 produces valid ring address (G grounds).
Stage 3 resolves constraints (Π terminates).
Stage 4 accumulates without contradiction (α consistent).
Stage 5 extracts coherent output (P projects).
Full pipeline is the composition PE_6 ∘ … ∘ PE_1.
Gate failure triggers complex conjugate rollback.
Machine is deterministic given initial state.
Stage transition requires guard satisfaction.
Effect composition is order-independent within a stage.
Epoch admits one datum or one refinement pass.
Adjacent stages with compatible guards may fuse.
Total reduction cost bounded by n × stage_max_cost.
Budget solvency rejection: a CompileUnit whose declared thermodynamicBudget is strictly less than the Landauer minimum (bitsWidth(Q_k) × ln 2) is rejected at the BudgetSolvencyCheck preflight.
Unit address identity: the unitAddress of a CompileUnit is the u:Element computed by hashing the canonical byte serialization of the root term’s transitive closure.
Every pending query eventually reaches a stage gate.
No starvation under bounded epoch admission.
Fair lease allocation under disjoint composition.
Window slide preserves saturation invariant.
Active → Suspended → Active round-trip preserves state.
AllOrNothing transaction rolls back on any failure.
BestEffort transaction commits partial results.
Transaction atomicity within a single epoch.
Partial saturation is monotonically non-decreasing across stages.
Approximation quality improves with additional epochs.
Deferred queries are eventually processed or explicitly dropped.
Ω⁶ = −1: reduction converges in 6 stages (phase half-turn).
Complex conjugate rollback involutory: (z̄)̄ = z.
Pairwise convergence: commutator converges to identity.
Triple convergence: associator converges to zero.
Associator monotonicity: associator norm non-increasing.
Associator finiteness: reaches 0 in bounded steps.
Associator vanishing implies associativity on resolved site space.
Adams termination: no convergence level beyond L3_Self.
Cayley-Dickson R→C: adjoin i with i²=−1, conjugation (a+bi)* = a−bi.
Cayley-Dickson C→H: adjoin j with j²=−1, ij=k, ji=−k, k²=−1.
Cayley-Dickson H→O: adjoin l, Fano plane products, associativity fails.
Adams theorem: no normed division algebra of dimension 16 exists.
Convergence level k lives in k-th division algebra: L0 in R, L1 in C, L2 in H, L3 in O.
Commutator vanishes iff algebra at that level is commutative.
Associator vanishes iff algebra at that level is associative.
d_Δ as interaction cost between entities.
SR_8 implies negotiation converges (commutator decreases monotonically).
Convergent negotiation selects U(1) ⊂ SU(2).
Outcome space of pairwise negotiation is S².
Interaction nerve β_k bounds coupling complexity at dimension k.
β_2(nerve) × max_disagreement bounds associator norm.
δ-ι-κ non-associativity: δ reads registry written by κ.
ι-α-λ non-associativity: λ reads lease state written by α.
λ-κ-δ non-associativity: δ reads state written by κ.
Root cause: non-associativity from read-write interleaving through mediating entity.
Certificate composition: cert(A⊗B) contains cert(A) and cert(B).
σ(A⊗B) ≥ max(σ(A), σ(B)): sequential composition does not lose saturation.
r(A⊗B) ≤ min(r(A), r(B)): residual can only shrink under sequential composition.
Site additivity: siteCount(F(G)) = F.sites + Σ_i G_i.sites.
Grounding distributivity: grounding(F(G(x))) = F.ground(G.ground(x)).
d_Δ decomposition: d_Δ(F(G)) decomposes into outer + inner d_Δ.
Table(Tuple(fields)): standard tabular data structure decomposition.
Tree(leaves): standard hierarchical data structure (AST, XML, JSON).
Pinning decrements free count by exactly 1.
Unbinding increments free count by exactly 1.
Every ReversibleEffect has an inverse (PinningEffect⁻¹ = UnbindingEffect on same site, PhaseEffect⁻¹ = conjugate phase).
External effects must match their declared shape.
Every predicate is total: evaluation terminates for all inputs.
Every predicate is pure: evaluation does not modify state.
Exhaustive + mutually exclusive dispatch is deterministic.
Match evaluation is deterministic given exhaustive, ordered arms.
Stage transition requires typed guard satisfaction.
Entry guard must be satisfied to enter a stage.
Exit guard must be satisfied, then the stage effect is applied.
The root resolver dispatch table is exhaustive and mutually exclusive over all TypeDefinitions.
Resolver dispatch is deterministic for every type.
Disjoint parallel computations commute: A ⊗ B = B ⊗ A when site targets are disjoint.
Parallel free-count deltas are additive.
Partitioning is exhaustive: component cardinalities sum to total site budget.
All interleavings of disjoint parallel computations yield the same final context.
Parallel certificate is the conjunction of component certificates plus disjointness.
A ComputationDatum’s ring value is the content hash of its certificate.
Composition certification requires both components certified and type-compatible.
Fully saturated partial application equals direct application.
Every epoch terminates: the reduction within each epoch reaches convergence angle π.
Grounding preservation across epoch boundaries.
Every finite prefix computes in finite time.
The first epoch starts from the unfold seed context.
Each subsequent epoch starts from the previous boundary’s continuation context.
Lease expiry at an epoch boundary returns claimed sites to the next epoch’s linear budget.
Every partial computation produces exactly one of Success or Failure.
Sequential failure propagation: if A fails, B is not evaluated.
Parallel failure independence: one component’s failure does not prevent the other’s success.
Recovery produces a new ComputationResult.
The reduction’s existing rollback mechanism is a Recovery whose effect is the conjugate phase rotation.
In a linear trace, every site is targeted exactly once. Total effect count equals site budget.
After a LinearEffect, the target site is pinned.
A consumed LinearSite cannot be targeted again.
Lease allocation decrements the linear budget by the lease cardinality.
Lease expiry returns claimed sites to the budget.
Subtyping is constraint superset: more constraints = more specific.
The constraint nerve of the supertype is a sub-complex of the subtype’s nerve.
Every recursive step strictly decreases the descent measure.
Recursion depth is bounded by the initial measure value.
Structural recursion’s measure is the input type’s structural size.
The base predicate is satisfied exactly when the measure reaches zero.
The working set is determined by the constraint nerve and the stage’s site targets.
All addresses within a region are within the region’s diameter under the chosen metric.
Total working set size is bounded by the addressable space at the quantum level.
The resolver at stage k accesses only addresses within its working set.
Ingested data conforms to the source’s declared type.
Emitted data conforms to the sink’s declared type.
Every ingestion through a source produces a valid ring datum via grounding.
Every emission through a sink produces a valid surface symbol via projection.
Every boundary effect touches at least one site.
Information extraction queries. Users initiate queries; the kernel resolves them against the ring substrate.
A request for information from the UOR kernel. The root abstraction for all query types.
A query for the ring-coordinate position of a datum: its stratum, spectrum, and address within the ring geometry.
A query for a metric value between two datums: ring distance, Hamming distance, or their divergence (curvature).
A query for the canonical representation of a datum or term: its normal form under the active resolver strategy.
A Query with a known source address, a typed relation constraint, and an open target partition:FreeRank. Represents any question of the form: given this source symbol and relation type, what is the target? The relation type is read from the observable coordinate triple (d_R, d_H, d_I) — not externally supplied. Applies across NLP, ARC-AGI grids, music, images, sensor streams, and logical formulae.
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.
A RelationQuery that explicitly declares its session membership, allowing the conformance suite to validate session-scoped site reduction across multi-turn Prism deployments.
The typed coordinate kind this query extracts. Replaces the string-valued query:coordinate property with a typed reference to a TriadProjection individual.
The ring address of the grounded source symbol.
The transformation type, expressed as a type:CompositeConstraint composed from the primitive basis. At inference time this is the output of an observable coordinate read on example pairs — computed from (d_R, d_H, d_I). Not an externally supplied input; read from the representation space.
The open site budget for the unknown target. Begins fully free; closes to isClosed = true upon resolution.
The GroundingMap that resolved the source symbol to its ring address.
The ProjectionMap that will render the resolved address neighbourhood back to surface symbols.
Accumulated session state carrying all state:Binding instances produced by prior queries. Each binding records a resolved address, its datum, and the type under which it was resolved. Prior bindings monotonically reduce the free site space for subsequent queries.
The stratum coordinate: the layer position of a datum within the ring's stratification.
The spectrum coordinate: the spectral decomposition of a datum under the ring's Fourier analysis.
The address coordinate: the content-addressable position of a datum in the Braille glyph encoding.
Type resolution strategies implementing the partition map Π : T_n → Part(R_n). Resolvers transform type declarations into ring partitions.
A strategy for resolving a type declaration into a partition of the ring. The kernel dispatches to a specific resolver based on the type's structure.
Resolves types by factoring the ring under dihedral group action. Identifies orbits under D_{2^n} to determine irreducibility boundaries.
Resolves types by computing canonical forms via term rewriting. Applies the critical identity and normalization rules to reduce terms to unique canonical representatives.
Resolves types by direct evaluation: applies operations to enumerate ring elements and classify them as irreducible, reducible, unit, or exterior.
The current state of an iterative resolution: tracks how many iterations have been performed, whether the resolution is complete, and the current site deficit.
A suggestion from the resolver for how to refine an incomplete resolution: which metric axis to explore, which class to narrow to, and which sites to target.
A computational complexity classification for resolvers. Each resolver's asymptotic runtime is typed as a named ComplexityClass individual rather than a free string.
The simplicial complex whose vertices are constraints and where a k-simplex exists iff the corresponding k+1 constraints have nonempty intersection. The nerve's topology governs resolution convergence: trivial homology ↔ smooth convergence, non-trivial homology ↔ potential stalls.
A specialisation of Resolver driving the completeness certification loop. Accepts a CompletenessCandidate, runs the ψ-pipeline (reading nerveEulerCharacteristic from ResolutionState), and either issues a CompletenessCertificate or produces a RefinementSuggestion.
A Resolver parameterised by quantum level. The same resolver strategy runs at any quantum level n ≥ 1 by substituting the appropriate R_n ring.
A Resolver that maintains a BindingAccumulator across multiple RelationQuery evaluations. The top-level resolver for multi-turn Prism deployments.
A Resolver that runs the ψ-pipeline in inverse mode. Accepts a TypeSynthesisGoal and returns a TypeSynthesisResult. Internally maintains a ConstraintSearchState tracking which constraint combinations have been explored and which Betti profiles they realise.
Internal resolver state tracking the boundary of explored constraint combinations during synthesis. Carries exploredCount, currentCandidate, and a link to the best SynthesisSignature achieved so far.
A Resolver that determines whether a CompleteType T at Q_n lifts to a CompleteType at Q_{n+1} without re-running the full ψ-pipeline from scratch. It computes the SpectralSequencePage sequence, reads the LiftObstruction, and either confirms the lift or returns a LiftRefinementSuggestion.
A RefinementSuggestion produced when a WittLift has a non-trivial LiftObstruction. Specialises RefinementSuggestion with liftSitePosition (the new bit position n+1) and obstructionClass.
A Resolver that computes the HolonomyGroup of a ConstrainedType by enumerating closed paths in the constraint nerve and accumulating DihedralElement values. Outputs a MonodromyClass and classifies the type as FlatType or TwistedType.
A resolver that uses the Jacobian matrix to guide constraint selection, implementing DC_10: select the constraint that maximises total curvature reduction.
A resolver that handles superposed site states, computing amplitudes and determining when superposition collapses to a classical site assignment (Amendment 32).
A resolver that exploits accumulated session bindings at full saturation (σ = 1) to provide O(1) resolution via direct coordinate reads (SC_5).
A resolver that validates whether a ComputationTrace satisfies the dual geodesic condition (AR_1-ordered and DC_10-selected). Produces GeodesicViolation individuals on failure.
A resolver that handles projective collapse of SuperposedSiteState components. Issues MeasurementCertificate upon successful collapse with QM_1 verification.
A Resolver that constructs a LiftChain from liftSourceLevel to an arbitrary liftTargetLevel Q_k by iterating IncrementalCompletenessResolver step by step.
A strategy class that defines how a SessionResolver orders pending RelationQuery instances for dispatch. The policy reads the targetSite.freeRank of each pending query and applies an ordering function.
A typed controlled vocabulary for ExecutionPolicy individuals. Follows the SessionBoundaryType pattern: a single class with named individuals rather than a subclass hierarchy.
A resolver that runs the extended ψ-pipeline (ψ_7–ψ_9) to compute the full homotopy type of a CechNerve. Returns HomotopyGroup observables and PostnikovTruncation records.
A resolver that computes the local structure of the moduli space at a given CompleteType: constructs the DeformationComplex, determines the HolonomyStratum, and computes tangent/obstruction dimensions.
The type of input this resolver accepts.
The type of output this resolver produces. For all UOR resolvers, the output is a partition:Partition.
A human-readable description of the resolution strategy this resolver implements.
The current resolution state of this resolver.
Whether this resolution is complete: all sites are pinned and the partition is fully determined.
The number of refinement iterations performed so far.
The site budget showing the remaining unpinned sites. When all sites are pinned, the deficit is zero and resolution is complete.
A refinement suggestion for advancing this resolution.
The metric axis this suggestion recommends exploring.
The constraint class this suggestion recommends applying.
The site coordinates this suggestion targets for pinning.
The rate at which sites are being pinned per iteration. A higher rate indicates faster convergence toward a complete resolution.
The computational complexity class of this resolver. Replaces the string-valued resolver:complexity property.
The constraint nerve associated with this resolution state.
The residual Shannon entropy of the resolution state: S = freeRank × ln 2. Measures remaining uncertainty.
Whether all Betti numbers of the constraint nerve are zero, indicating no topological obstructions to resolution.
The Euler characteristic χ(N(C)) of the active constraint nerve at this resolution state. IT_7d requires this value to equal n (the quantum level) for resolution to be complete. Cached here to avoid recomputing the full ψ pipeline on each iteration check.
The CompletenessCandidate this resolver is certifying.
The quantum level this resolver instance is configured for.
The BindingAccumulator this session resolver maintains across multiple RelationQuery evaluations.
The goal this type synthesis resolver is working to achieve.
Number of constraint combinations evaluated so far during synthesis.
The type candidate currently being evaluated during synthesis.
The WittLift this incremental completeness resolver is evaluating.
The new site position at Q_{n+1} that the lift refinement suggestion targets.
The obstruction class this lift refinement suggestion is designed to kill.
The type whose holonomy this monodromy resolver is computing.
The HolonomyGroup produced by this monodromy resolver run.
The Jacobian observable guiding constraint selection at this resolution state (DC_10).
Whether this resolver used the saturation shortcut (SC_5) to bypass the ψ-pipeline and return a direct coordinate read.
The GeodesicTrace being validated by this GeodesicValidator.
The amplitude of the SuperposedSiteState prior to projective collapse by this MeasurementResolver.
The site index that was collapsed (pinned to a classical value) by the projective measurement.
The classical value obtained from the projective collapse. Either 0 or 1 for a single-site measurement.
The amplitude vector of all branches maintained by this SuperpositionResolver during ψ-pipeline traversal. Encoded as a comma-separated list of decimal amplitudes. Must satisfy Σ|αᵢ|² = 1 (QM_5) after normalization.
The full vector of all branch amplitudes before projective collapse. Recorded by the MeasurementResolver to enable Born rule verification (QM_5): P(outcome k) = |α_k|².
The level to which the tower is being built.
The IncrementalCompletenessResolver used for each single-step lift.
The ordering strategy this resolver applies to pending queries. Defaults to FifoPolicy if unset.
The CechNerve whose homotopy type this resolver computes.
A HomotopyGroup observable produced by this resolver.
The CompleteType whose local moduli structure this resolver computes.
The DeformationComplex constructed by this resolver.
The dispatch table governing resolver selection for this resolver class.
The predicate that selects this specific resolver. When the predicate evaluates to true on an input type, this resolver is chosen.
O(1) complexity — the resolver runs in constant time regardless of ring size.
O(log n) complexity — the resolver runs in logarithmic time in the quantum level.
O(n) complexity — the resolver runs in time linear in the quantum level.
O(2^n) complexity — the resolver runs in time exponential in the quantum level.
Process queries in arrival order. The implicit pre-Amendment 48 behavior.
Process the query with the smallest targetSite.freeRank first. Favors cheapest resolutions, accelerating early grounding gain.
Process the query with the largest targetSite.freeRank first. Favors hardest resolutions, maximizing information gain per step.
Process queries whose targetSite is disjoint from all other pending queries' site sets first. Minimizes contention when operating against a SharedContext.
Runtime type declarations that parameterize the resolution pipeline. Types are declared by Prism applications and resolved to partitions of the ring.
A runtime type declaration. The root class for all UOR types. Each TypeDefinition, when resolved, produces a partition of the ring at the specified quantum level.
A primitive type defined by a fixed bit width. The carrier is the entire ring Z/(2^n)Z at the specified quantum level.
A product (Cartesian) type formed from multiple component types. The carrier is the product of the component carriers.
A sum (disjoint union) type formed from multiple variant types. The carrier is the disjoint union of the variant carriers.
A type formed by constraining a base type with a predicate. The carrier is the subset of the base carrier satisfying the constraint.
A composable predicate that refines a type by pinning one or more site coordinates. Constraints are the parameterization mechanism for ConstrainedType.
A constraint based on residue class membership: x ≡ r (mod m). Pins sites corresponding to the residue pattern.
A constraint based on carry propagation patterns in ring arithmetic. Pins sites corresponding to carry positions.
A constraint on factorization depth: the minimum and maximum number of irreducible factors. Pins sites by bounding the factorization tree depth.
A constraint formed by composing two or more simpler constraints. The composite pins the union of sites pinned by its components.
Pins the Hamming weight of the Datum to at most the bound. The horizontal axis of the tri-metric.
Pins a single site coordinate to 0 or 1. The atomic unit of the site budget.
Pins the Datum to an affine subspace specified by an offset and a set of generators.
A classification axis for constraints by their geometric effect. The three axes — vertical (ring/additive), horizontal (Hamming/bitwise), diagonal (incompatibility) — form the tri-metric coordinate system of UOR.
A TypeDefinition certified to satisfy the UOR completeness criterion (IT_7d): its constraint nerve N(C) has Euler characteristic χ = n and all Betti numbers β_k = 0. A CompleteType guarantees that resolution closes the site budget in O(1) — no iterative refinement is required. Completeness is attested by a cert:CompletenessCertificate linked via cert:certifiedType. This class is not addressable from a type-expr position in the term language; references from term-language positions are rejected by the resolver.
A ConstrainedType actively undergoing the completeness certification pipeline. Links to the resolver:ResolutionState tracking the current iteration and to the resolver:CechNerve being computed. Disjoint from CompleteType (which is already certified). This class is not addressable from a type-expr position in the term language; references from term-language positions are rejected by the resolver.
A record of a single site-closing event: one constraint application that reduced the FreeRank deficit. Carries the applied constraint and the sitesClosed count. Forms the ordered audit trail between ConstrainedType and CompleteType.
A specification of the desired topological properties of a type to be synthesised. Carries a target Euler characteristic (targetEulerCharacteristic) and a target Betti profile (zero or more targetBettiNumber assertions). The minimal goal for O(1) resolution is: targetEulerCharacteristic = n and all targetBettiNumber = 0 — the IT_7d profile.
The output of a TypeSynthesisResolver run. Contains the SynthesizedType, the realised topological signature (as a SynthesisSignature), and the SynthesisTrace recording the construction steps.
A ConstrainedType produced by the TypeSynthesisResolver. Distinguished from a hand-authored ConstrainedType by the presence of a type:synthesisResult link. May or may not be a CompleteType, depending on the synthesis goal. This class is not addressable from a type-expr position in the term language; references from term-language positions are rejected by the resolver.
The minimal set of constraints in the SynthesizedType's constraint set that is sufficient to realise the target topological signature. The minimality criterion is that removing any single member changes the realised signature.
A ConstrainedType T' over R_{n+1} obtained by extending a ConstrainedType T over R_n. Carries a link to the base type (liftBase), the quantum level it lifts to (liftTargetLevel), and the LiftObstruction (if the lift fails to transfer completeness). A WittLift is a CompleteType iff its LiftObstruction is trivial.
The algebraic obstruction to a WittLift inheriting the completeness of its base type. Computed as the image of the spectral sequence differential d_2. If trivial (zero), the base type's completeness lifts. If non-trivial, at least one additional constraint is needed at the new quantum level.
A ConstrainedType whose HolonomyGroup is non-trivial — at least one closed constraint path produces a non-identity dihedral element. A TwistedType may still be a CompleteType (IT_7d is a homological, not holonomic, criterion), but its resolution paths require tracking dihedral accumulation. This class is not addressable from a type-expr position in the term language; references from term-language positions are rejected by the resolver.
A ConstrainedType whose HolonomyGroup is trivial — all closed constraint paths have identity monodromy. The constraint configuration is topologically flat: resolution is path-independent. This class is not addressable from a type-expr position in the term language; references from term-language positions are rejected by the resolver.
A type representing a superposition of site states where sites carry complex amplitudes rather than binary pinned/free assignments. Ontological realisation of RC_5 (Amendment 32). This class is not addressable from a type-expr position in the term language; references from term-language positions are rejected by the resolver.
A topological signature (χ, β_k) that is formally impossible to achieve for any ConstrainedType. Witnessed by an ImpossibilityWitness in proof/.
A site state that has undergone projective collapse from a SuperposedSiteState to a definitive classical value. Topologically equivalent to a classically pinned site (QM_2).
An ordered composition of WittLift steps from liftSourceLevel (Q_j) to liftTargetLevel (Q_k) for any j < k. The canonical object certifying type completeness at arbitrary Q_k.
The complete ordered sequence of LiftObstruction records encountered and resolved along a LiftChain. An empty ObstructionChain means the tower is flat.
The space of all CompleteTypes over R_n at a given quantum level.
A stratum indexed by a conjugacy class of subgroups of D_{2^n}.
A one-parameter family of constraint configurations parameterizing a path.
The versal deformation of a CompleteType T.
The map induced by WittLift from one moduli space to the next.
The adjunction between the type lattice and the site lattice. The upper adjoint is type closure; the lower adjoint is site interior. σ = lower adjoint evaluation; r = complement of upper adjoint image.
A morphism T₁ → T₂ witnessing that T₁ is a subtype of T₂: the constraint set of T₁ is a superset of the constraint set of T₂.
The variance of a structural type position under operad composition. One of Covariant, Contravariant, Invariant, or Bivariant.
The partial order on types induced by TypeInclusion. The top element is PrimitiveType (no constraints); the bottom elements are CompleteTypes (all sites pinned).
The bit width of a primitive type (the quantum level n). The carrier is Z/(2^n)Z.
The base type that a constrained type restricts.
The content-derived address of this type definition, uniquely identifying the type in the UOR address space.
A typed constraint object applied to this constrained type. Replaces the deprecated string-based type:constraint property.
The modulus m of a residue constraint: x ≡ r (mod m).
The residue value r of a residue constraint: x ≡ r (mod m).
The carry propagation pattern of a carry constraint, expressed as a Datum at the appropriate quantum level.
The minimum factorization depth required by a depth constraint.
The maximum factorization depth allowed by a depth constraint.
A component constraint of this composite constraint.
Upper bound on the Hamming weight of the Datum.
Zero-based index of the pinned site coordinate.
The value the pinned site coordinate must equal (a Datum in the set {0, 1}).
Constant offset defining the affine subspace.
A generator of the affine subspace. Non-functional: multiple generators span the subspace.
The metric axis along which this constraint operates: vertical (ring), horizontal (Hamming), or diagonal (incompatibility).
A site coordinate that this constraint pins when applied.
The metric axis that this operation affects. Replaces the string-valued type:axisSignature property with a typed reference to MetricAxis individuals. Non-functional: an operation may affect multiple axes.
The cost of applying this constraint in terms of axis crossings: the number of metric boundaries that must be traversed.
The ConstrainedType being evaluated for completeness by this CompletenessCandidate.
The constraint nerve being computed for this candidate. The CompletenessResolver reads χ(N(C)) from this nerve at each iteration via resolver:nerveEulerCharacteristic.
The constraint applied in this witness step.
Number of sites closed by this witness step.
The target χ(N(C)) value. For O(1) resolution: set equal to n (the quantum level).
Non-functional. Each assertion specifies a target Betti number value for a given homological degree. Multiple assertions permitted, one per degree.
Links a SynthesizedType back to the synthesis run that produced it.
Non-functional. One assertion per constraint in the minimal basis.
The cardinality of the minimal basis. The theoretical lower bound is n (one constraint per site).
The base type being lifted to the next quantum level.
The LiftObstruction for this lift. Trivial (zero class) iff the lift inherits completeness.
True iff the obstruction class is zero — the base type's completeness transfers to the lifted quantum level without additional constraints.
The site at the new quantum level where the obstruction is located. Ranges over the new bit position introduced at Q_{n+1}.
The HolonomyGroup of this type. Computed by the MonodromyResolver.
The MonodromyClass classifying this type as flat or twisted.
The amplitude coefficient for this superposed site state.
Whether the target signature of this TypeSynthesisGoal is a ForbiddenSignature. If true, synthesis is provably impossible.
The SuperposedSiteState from which this CollapsedSiteState was produced by projective measurement.
The amplitude of the surviving branch after projective collapse. |α|² is the probability of this outcome under the Born rule.
Whether the amplitude vector of this SuperposedSiteState satisfies the normalization condition Σ|αᵢ|² = 1 (QM_5). Set by the SuperpositionResolver after verification.
Whether this ConstrainedType has been classified as FlatType or TwistedType by the MonodromyResolver. The MN_8 identity guarantees this is a bivalent classification: holonomyClassified(T) iff isFlatType(T) xor isTwistedType(T).
The quantum level at the base of the chain.
The number of WittLift steps in the chain (k - j).
A WittLift step in this chain. Non-functional: one per step.
The full obstruction history of this chain.
The basis size of the CompleteType at the chain target level.
A non-trivial LiftObstruction in this chain. Non-functional.
Total number of non-trivial LiftObstruction records.
True iff obstructionCount = 0 (flat tower).
The quantum level at which this moduli space is defined.
A CompleteType that is a point of this moduli space.
The MonodromyClass indexing this stratum.
The codimension of this stratum within the moduli space.
The moduli space containing this stratum.
A CompleteType along the deformation path.
Whether every member of this deformation family remains a CompleteType.
The CompleteType at the base of this versal deformation.
The dimension of the versal deformation space.
The source moduli space of this tower map.
The upper adjoint (type closure) of the Galois connection, expressed as a symbolic formula string.
The lower adjoint (site interior) of the Galois connection, expressed as a symbolic formula string.
The fixpoint condition for the Galois connection: when upper(lower(T)) = T, the type is complete.
Description of the refinement direction: ascending in type lattice corresponds to descending in site freedom.
Formula or description of the site count for a structural type individual.
Description of the grounding rule that maps values of this structural type onto the UOR ring.
Description of the constraint characterizing this structural type, if applicable.
The closure property of a Galois connection.
The interior property of a Galois connection.
Reference to the grounding map used for this type.
The algebraic composition law governing this type.
Constraint on the ordering of sites for this type.
The threshold for backbone inclusion in the type lattice.
The permutation group acting on sites of this type.
Witness certifying acyclicity of the type dependency graph.
Witness certifying connectivity of the type graph.
Constraint imposed by the schema on this type.
The size of the alphabet for symbol-based types.
The range specification for quantized types.
Reference to the element type within a composite type.
True iff constraints(source) ⊇ constraints(target). Computed, not asserted.
Maximum chain length from PrimitiveType (top) to any CompleteType (bottom). Equals the site budget n at quantum level Q_k.
The vertical (ring/additive) metric axis. Constraints on this axis operate through ring arithmetic: residue classes, divisibility, and additive structure.
The horizontal (Hamming/bitwise) metric axis. Constraints on this axis operate through bitwise structure: carry patterns, bit positions, and Hamming distance.
The diagonal (incompatibility) metric axis. Constraints on this axis measure the gap between ring and Hamming metrics — the curvature of UOR geometry.
A single value from an ordered domain. siteCount = n (quantization bits).
quantize(value, range, bits) produces ring element where d_R reflects value proximity
A value from a finite unordered set. siteCount = ceil(log2(|alphabet|)).
argmin_{encoding} sum d_delta over observed pairs (CY_5)
An ordered list of elements with backbone constraint. The free monoid on the element type.
backbone ordering: elements indexed by position
free monoid on element type, backbone constraint
site ordering follows CY_6 (optimal site ordering)
Nodes with edge constraints. Constraint nerve = graph topology.
edge constraints: adjacency preserved under grounding
constraint nerve = graph nerve, beta_k equality
Unordered collection. d_delta is permutation-invariant.
permutation invariance: encoding is order-independent
d_delta invariant under element permutation, D_{2n} symmetry
Hierarchical structure. beta_1=0 (acyclic), beta_0=1 (connected).
beta_1=0 (acyclic), beta_0=1 (connected)
parent-child encoding with acyclicity constraint
Collection of tuples sharing a schema = Sequence(Tuple(S)). Functorial decomposition.
shared schema: all rows conform to tuple type S
Sequence(Tuple(S)), functorial decomposition
The structural position preserves TypeInclusion: if T₁ ≤ T₂, then F(T₁) ≤ F(T₂).
The structural position reverses TypeInclusion: if T₁ ≤ T₂, then F(T₂) ≤ F(T₁).
The structural position requires exact type equality: F(T₁) ≤ F(T₂) only if T₁ = T₂.
The structural position ignores the type parameter: F(T₁) ≤ F(T₂) for all T₁, T₂.
The canonical binary disjoint union type whose carrier is L + R.
The canonical A + Unit idiom for optional values.
Irreducibility partitions produced by type resolution. A partition divides the ring into four disjoint components: Irreducible, Reducible, Units, and Exterior.
A four-component partition of R_n produced by resolving a type declaration. The four components — Irreducible, Reducible, Units, Exterior — are mutually disjoint and exhaustive over the carrier.
A single component of a partition: a set of datum values belonging to one of the four categories.
The set of irreducible elements under the active type: elements whose only factorizations involve units or themselves. Analogous to prime elements in a ring.
The set of reducible non-unit elements: elements that can be expressed as a product of two or more non-unit elements.
The set of invertible elements (units) in the carrier: elements with a multiplicative inverse. In Z/(2^n)Z, the units are the odd integers.
Elements of R_n that fall outside the active carrier — i.e., outside the type's domain. These are ring elements that do not participate in the current type resolution.
A single site coordinate in the iterated Z/2Z fibration. Each site represents one binary degree of freedom in the ring's structure. The total number of sites equals the quantum level n.
The site budget for a partition: an accounting of how many sites are pinned (determined by constraints) versus free (still available for further refinement). A closed budget means all sites are pinned and the type is fully resolved.
A record of a single site being pinned by a constraint. Links a specific site coordinate to the constraint that determined its value.
The tensor product of two partitions: partition(A × B) = partition(A) ⊗ partition(B). The four-component structure combines component-wise under the product type construction (PT_2a). Carries leftFactor and rightFactor links to the operand partitions.
The coproduct (disjoint union) of two partitions: partition(A + B) = partition(A) ⊕ partition(B). The four-component structure combines via disjoint union under the sum type construction (PT_2b). Carries leftSummand and rightSummand links to the operand partitions.
The irreducible component of this partition.
The reducible component of this partition.
The exterior component of this partition.
A datum value belonging to this partition component.
The number of elements in this partition component. The cardinalities of the four components must sum to 2^n.
The irreducible density of this partition: |Irr| / |A|, where A is the active carrier.
The type declaration that was resolved to produce this partition.
The Witt level n at which this partition was computed. The ring has 2^n elements at this level.
The zero-based position of this site coordinate within the iterated fibration. Position 0 is the least significant bit; position n-1 is the most significant.
The current state of this site coordinate: 'pinned' if determined by a constraint, 'free' if still available for refinement.
The site budget associated with this partition.
The total number of site coordinates in this budget, equal to the quantum level n.
The number of site coordinates currently pinned by constraints.
The number of site coordinates still free (not yet pinned). Equals totalSites - pinnedCount.
Whether all sites in this budget are pinned. A closed budget means the type is fully resolved and the partition is complete.
A site coordinate belonging to this budget.
The constraint that pins this site coordinate.
The site coordinate that this pinning determines.
An ancilla site coordinate paired with this site for reversible computation (RC_1–RC_4 ancilla model).
True when this site budget uses a reversible computation strategy preserving information through ancilla sites.
The formal membership criterion for this Complement: x ∈ Ext(T) iff x ∉ carrier(T). The Complement is context-dependent on the active type T (FPM_9).
Whether the four components of this partition are exhaustive over R_n: |Irr| + |Red| + |Unit| + |Ext| = 2^n (FPM_8). Set by the kernel after verification.
The left operand partition of this tensor product.
The right operand partition of this tensor product.
The left operand partition of this coproduct.
The right operand partition of this coproduct.
Observable quantities and metrics computed by the UOR kernel. Includes ring-metric, Hamming-metric, curvature, holonomy, and catastrophe-theoretic observables.
A measurable quantity in the UOR Framework. All observables are kernel-computed and user-consumed.
An observable measuring stratum-level properties: position within the ring's layer structure.
An observable measuring geometric distance between ring elements under a specific metric.
An observable measuring properties of paths through the ring: path length, total variation, winding number.
An observable measuring reduction properties: the length and count of operation sequences.
An observable measuring catastrophe-theoretic properties: thresholds at which qualitative changes occur in the partition.
An observable measuring the curvature of the UOR geometry: the gap between ring-isometry and Hamming-isometry for a given transform.
An observable measuring holonomy: the accumulated transformation when traversing a closed path in the ring.
Distance between two ring elements under the ring metric: d_R(x, y) = |x - y| mod 2^n.
Distance between two ring elements under the Hamming metric: the number of bit positions where they differ.
The metric incompatibility between two ring elements: the divergence between their ring-metric and Hamming-metric distances, measuring geometric curvature.
The difference in stratum between two ring elements.
The sequence of strata traversed by a path through the ring.
The length of a path through the ring, measured in operation steps.
The total variation of a path: the sum of metric distances between consecutive elements.
The winding number of a closed path: the number of times the path wraps around the ring.
The number of operation applications in a reduction sequence.
The number of distinct reduction sequences in a computation.
A critical value at which a qualitative change occurs in the partition structure.
The number of catastrophe events (qualitative partition changes) in a computation.
The commutator [f, g](x) = f(g(x)) - g(f(x)) of two operations, measuring their non-commutativity.
The integrated curvature over a region of type space: the total metric incompatibility accumulated.
The monodromy of a closed path: the net transformation accumulated when traversing a loop in the type space.
The parallel transport of a vector along a path: the canonical lift of the path to the tangent bundle of the ring.
An element of the dihedral group D_{2^n} acting on the type space. Each dihedral element induces an isometry of 𝒯_n.
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.
Site-by-site curvature decomposition. J_k measures the discrete derivative of the incompatibility metric at site position k: J_k = |d_R(x, succ(x)) - d_H(x, succ(x))| restricted to position k.
An observable measuring a topological invariant of the resolution space. Topological observables are invariant under continuous deformations of the constraint configuration.
The rank of a homology group of the constraint nerve. β_k = rank(H_k(N(C))) counts the k-dimensional holes in the constraint configuration.
The smallest positive eigenvalue of the constraint nerve Laplacian. Controls the convergence rate of iterative resolution: larger gap = faster convergence.
An observable measuring thermodynamic properties of the resolution process: residual entropy, Landauer cost, and reduction distribution statistics.
S_residual: the residual Shannon entropy of the site distribution after partial resolution. Computed as S = (Σ κ_k − χ(N(C))) × ln 2 (IT_7b). Unit: Nats.
The minimum thermodynamic cost (in units of k_B T ln 2) of erasing one bit of site uncertainty. The UOR ring operates at β* = ln 2 — the Landauer temperature.
The Shannon entropy of the reduction distribution P(j) = 2^{−j}. At the Landauer temperature, this equals ln 2 per reduction step — each step erases exactly one bit of site uncertainty.
A named topological signature: a pair (realised Euler characteristic, realised Betti profile). Linked from TypeSynthesisResult. Allows comparison between the goal signature and the actually achieved signature.
A single page E_r of the quantum level spectral sequence. Carries the page index r and the differential d_r. The sequence converges when all differentials vanish — typically by E_3 for simple constraint configurations.
The cohomology class in H^2(N(C(T))) representing the LiftObstruction for a specific WittLift. The class is zero iff the obstruction is trivial. When non-zero, it indexes the specific site pair at Q_{n+1} that cannot be closed by the lifted constraint set alone.
A classification of a type's holonomy: the subgroup of D_{2^n} generated by all Monodromy observables computed over closed paths in the type's constraint nerve. Trivial iff every closed constraint path returns to its starting site assignment without net dihedral transformation.
The holonomy group of a ConstrainedType: the group of all Monodromy elements achievable by closed paths in the constraint nerve. Always a subgroup of D_{2^n}. Trivial iff the type has trivial monodromy everywhere; equals D_{2^n} iff paths involving both neg and bnot involutions are present.
A sequence of constraint applications forming a closed loop in the constraint nerve — beginning and ending at the same site assignment. The Monodromy of the loop is the net DihedralElement accumulated when traversing it.
A classification of phase boundary in the catastrophe diagram: period boundary (g divides 2^n − 1) or power-of-two boundary (g = 2^k).
The achievability classification of a topological signature in the morphospace. Either Achievable or Forbidden (witnessed by ImpossibilityWitness).
The k-th homotopy group πk(N(C), v) of the constraint nerve based at vertex v.
The image of πk(N(C)) → Aut(sitek) for k > 1. Generalises the MN_6 monodromy homomorphism.
The Whitehead product [α, β] ∈ πp+q−1 for α ∈ πp, β ∈ πq.
A record of the holonomy stratification of the moduli space at a given quantum level: the list of HolonomyStrata, their codimensions, and their relationship to the MorphospaceBoundary.
Superclass for the six universal measurements. Every computation on the ring produces these six quantities: d_Δ, σ, J_k, β_k, χ, r.
The grounding metric σ = pinned sites / total sites. Ranges from 0 (no sites pinned) to 1 (fully grounded).
The Euler characteristic χ = Σ(−1)^k β_k of the constraint nerve. An integer-valued topological invariant.
The numeric value of an observable measurement.
The source object of this measurement (datum, partition, or path start point).
The target object of this measurement (for metrics and path-end measurements).
The measurement unit of this observable. Replaces the string-valued observable:unit property with a typed reference to a MeasurementUnit individual.
The site position k at which this Jacobian entry is measured.
The discrete derivative value at this site position.
The dimension k of the topological observable (e.g., the degree of the Betti number or the dimension of the spectral gap).
The Euler characteristic actually achieved by this synthesis signature.
Non-functional. Realised Betti number values, one assertion per homological degree.
The page r of this spectral sequence page. r=1 is the initial page; convergence is declared when all d_r are zero.
True iff d_r = 0 on this page — no further corrections to the lifted homology.
The page index r at which the spectral sequence converged (all subsequent differentials zero).
The cohomology class in H^2(N(C(T))) representing this obstruction.
The closed path that generates this monodromy value.
The dihedral element g in D_{2^n} accumulated when traversing the loop. The monodromy is trivial iff this element is the group identity.
True iff the monodromyElement is the identity in D_{2^n}.
Non-functional. The generators of the holonomy group: one DihedralElement per generating monodromy.
The order of the holonomy group as a subgroup of D_{2^n}. For a FlatType: 1. For full dihedral holonomy: 2^{n+1}.
The number of constraint application steps in this closed path.
Non-functional. The ordered sequence of constraints traversed. One assertion per step.
Non-functional. One assertion per generator in the normal form of the element — the sequence of neg and/or bnot operations that realises this dihedral element when composed.
True iff this element is the group identity (the trivial monodromy value).
The order of this element in D_{2^n}: the smallest k >= 1 such that g^k = id. For neg and bnot: order 2.
An estimated computational hardness for a ThermoObservable, connecting thermodynamic cost to complexity (TH_9 realisation).
The ring dimension coordinate n in the (n, g) catastrophe phase diagram (PD_1 n-coordinate).
The group-order coordinate g in the (n, g) catastrophe phase diagram (PD_1 g-coordinate).
True when g divides 2^n − 1, placing this observable on a resonance line in the phase diagram (PD_4).
The type of phase boundary at this point in the catastrophe diagram: PeriodBoundary or PowerOfTwoBoundary (PD_2).
The achievability classification of this observable's topological signature in the morphospace.
Whether this signature has been empirically verified as achievable at some quantum level.
Whether this signature has been formally proven impossible by an ImpossibilityWitness.
The proof individual (ImpossibilityWitness or AxiomaticDerivation) that grounds this signature's achievability classification.
The rotation exponent k ∈ \[0, 2^n) of this dihedral element in the standard representation r^k s^s. Together with reflectionBit, uniquely identifies the element within D_\{2^n\}.
The reflection flag s ∈ \{0,1\} of this dihedral element. False = pure rotation (r^k), true = reflection (r^k·s). D_7 defines composition: (r^a s^p)(r^b s^q) = r^(a + (-1)^p b) s^(p XOR q).
The dimension k of this homotopy group πk.
The rank of this homotopy group (number of free generators).
The basepoint vertex v at which this homotopy group is computed.
The dimension k > 1 at which this higher monodromy acts.
True iff this Whitehead product is trivial (zero in πp+q−1).
The Postnikov truncation associated with this spectral sequence page.
The quantum level at which this stratification is computed.
A HolonomyStratum in this stratification record.
The mathematical domain of this base metric.
The mathematical range (codomain) of this base metric.
How this metric composes with others in the measurement tower.
The existing observable class that this base metric references.
The existing identity that defines this base metric.
The count of pinned sites (numerator of σ).
The total site count (denominator of σ).
The alternating sum formula for Euler characteristic.
The unit of measurement for this base metric.
The precision or resolution of this base metric.
Monotonicity property of this metric (e.g., non-decreasing).
The decomposition rule for this metric into sub-metrics.
The position of this metric in the metric tower.
The computational cost of evaluating this metric.
Upper or lower bound on the metric value.
Information-theoretic unit: the measurement is in bits (e.g., Hamming weight, entropy).
Ring-arithmetic unit: the measurement is in ring distance steps (|x - y| mod 2^n).
Dimensionless unit: the measurement is a pure number (e.g., winding number, Betti number, spectral gap).
Natural information unit: entropy measured in nats (using natural logarithm). S_residual is expressed in nats when computed as (Σ κ_k − χ) × ln 2.
A phase boundary where g divides 2^n − 1, meaning g is a period of the multiplicative structure of R_n.
A phase boundary where g = 2^k, meaning g aligns with the binary stratification of R_n.
The signature has been verified as achievable at some quantum level by an AxiomaticDerivation proof.
The signature has been formally proven impossible by an ImpossibilityWitness deriving from MS_1, MS_2, or other impossibility theorems.
d_Δ: the incompatibility metric |d_R − d_H| per site pair.
σ: the grounding metric, pinned sites / total sites.
β_k: per-dimension Betti number of the constraint nerve.
r: count of free (unpinned) sites, the residual entropy.
Carry chain algebra: generate/propagate/kill event classification, carry profiles, encoding configurations, and encoding quality metrics for d_Δ optimization.
The Boolean function chain c_{k+1} = or(and(x_k, y_k), and(xor(x_k, y_k), c_k)). The carry chain is the algebraic mechanism behind the incompatibility metric d_Δ.
A single carry event at site k. Three kinds: Generate (and(x_k, y_k) = 1), Propagate (xor(x_k, y_k) = 1 and c_k = 1), Kill (neither generate nor propagate).
The complete carry pattern for an addition x + y. Aggregates carry events across all sites into counts and position masks.
A mapping from a finite symbol set S to Z/(2^k)Z where 2^k ≥ |S|. Determines how domain values are represented as ring elements.
The d_Δ quality metric for an encoding over observed data. Measures how well an encoding minimizes carry-induced metric incompatibility.
The number of sites in this carry chain.
Bit mask of site positions where carry is generated: and(x_k, y_k) = 1.
Bit mask of site positions where carry propagates: xor(x_k, y_k) = 1.
Bit mask of site positions where carry is killed: neither generated nor propagated.
The kind of carry event: Generate, Propagate, or Kill.
The site index k at which this carry event occurs.
The total number of carry events in this profile.
The longest consecutive propagation run in this profile.
The carry chain that this profile summarizes.
The cardinality of the symbol set S being encoded.
The number of bits k used for encoding (2^k ≥ |S|).
String representation of the mapping from symbols to ring elements.
The mean d_Δ over observed pairs for this encoding.
The ratio of distinguishable pairs to total pairs under this encoding.
Whether this encoding minimizes Σ d_Δ over observed pairs.
Simplicial complexes, chain complexes, boundary operators, and homology groups for structural reasoning.
A k-simplex: a finite set of k+1 vertices drawn from constraint objects.
A simplicial complex: a set of simplices closed under taking faces.
A face map d_i: removes vertex i from a simplex, producing a face.
A free abelian group generated by k-simplices (the k-th chain group C_k).
The boundary operator ∂_k: C_k → C_{k-1}. Satisfies ∂² = 0.
A chain complex: a sequence of chain groups connected by boundary operators.
The k-th homology group H_k = ker(∂_k) / im(∂_{k+1}). Measures k-dimensional holes.
The nerve functor N: maps a set of constraints to a simplicial complex.
The chain functor C: maps a simplicial complex to a chain complex.
A simplicial set satisfying the Kan extension condition. The constraint nerve, when promoted from a SimplicialComplex to a KanComplex, carries a full homotopy type — not just its homology groups.
A witness that a given horn (an incomplete simplex boundary) can be filled, certifying the Kan condition at a specific dimension and position.
The k-th Postnikov truncation τ≤k of the constraint nerve: a KanComplex whose homotopy groups πj vanish for j > k.
The k-invariant κk that classifies the extension from the (k−1)-truncation to the k-truncation of the Postnikov tower. Trivial κk means the truncation splits as a product.
The deformation complex of a CompleteType T: a chain complex whose H⁰ = automorphisms, H¹ = first-order deformations, H² = obstructions to extending deformations.
The dimension k of a simplex (number of vertices minus one).
A vertex of this simplex, drawn from the set of constraint objects.
The number of vertices in this simplex (dimension + 1).
Indicates that this simplex is a face of another simplex.
A site coordinate in the partition whose intersection pins this simplex.
A simplex belonging to this simplicial complex.
The maximum dimension of any simplex in this simplicial complex.
The Euler characteristic of this simplicial complex: the alternating sum of simplex counts by dimension.
The total number of vertices (0-simplices) in this simplicial complex.
The index i of the vertex removed by this face map d_i.
The target face (result simplex) of this face map.
The degree k of this chain group (the dimension of its generating simplices).
The rank of a free abelian group (number of generators).
A simplex that generates this chain group.
The source chain group C_k of this boundary operator.
The target chain group C_{k-1} of this boundary operator.
Whether this boundary operator satisfies the fundamental property ∂² = 0.
A chain group belonging to this chain complex.
A boundary operator belonging to this chain complex.
The degree k of this homology group H_k.
The Betti number β_k = rank(H_k): the rank of this homology group.
A horn filler witnessing the Kan condition for this complex.
The dimension of the horn that this filler completes.
The position (missing face index) of the horn that this filler completes.
The truncation level k of this Postnikov truncation τ≤k.
The KanComplex from which this Postnikov truncation is derived.
The k-invariant classifying the extension at this truncation level.
True iff this k-invariant is trivial, meaning the Postnikov truncation splits as a product.
The CompleteType whose deformation complex this is.
The dimension of the tangent space H¹(Def(T)): the number of first-order deformations.
The dimension of the obstruction space H²(Def(T)): the number of independent obstructions to extending deformations.
The homology group that grounds this Betti number observable.
The chain complex whose Laplacian determines this spectral gap.
The chain complex used for homological analysis of a resolution state.
∂² = 0: the boundary of a boundary is zero.
The nerve functor N: constraints → simplicial complex.
The chain functor C: simplicial complex → chain complex.
ψ_4: HomologyGroups → BettiNumbers (extraction functor).
Index bridge: connects Euler characteristic to alternating Betti sum.
Cochain complexes, sheaf cohomology, and local-to-global obstruction detection.
A cochain group: the dual of a chain group, maps chains to coefficients.
The coboundary operator δ^k: C^k → C^{k+1}. Satisfies δ² = 0.
A cochain complex: a sequence of cochain groups connected by coboundary operators.
The k-th cohomology group H^k = ker(δ^k) / im(δ^{k-1}). Measures k-dimensional obstructions.
A sheaf F over a simplicial complex: assigns data to each simplex with restriction maps.
A stalk F_σ: the local data of a sheaf at a simplex σ.
A global section of a sheaf: a consistent choice of local data across all simplices.
A local section: a consistent choice of data over a subcomplex.
A restriction map ρ_{σ,τ}: maps data from a simplex to a face.
A gluing obstruction: a cohomology class that detects when local sections fail to glue.
The rank (dimension) of this cochain group.
The chain group that this cochain group is dual to.
The source cochain group of this coboundary operator.
The target cochain group of this coboundary operator.
Whether this coboundary operator satisfies δ² = 0.
A cochain group belonging to this cochain complex.
A coboundary operator belonging to this cochain complex.
The degree k of this cohomology group H^k.
The rank (dimension) of this cohomology group.
The simplicial complex that this sheaf is defined over.
The simplex at which this stalk is located.
The source simplex of this restriction map.
The target simplex (face) of this restriction map.
The cohomology class that this gluing obstruction represents.
The refinement suggestion that, if applied, would resolve this gluing obstruction. Computed by the kernel when ψ₆ detects H^1 ≠ 0: the obstruction class indexes the site pair that is incompatible, and the suggestion targets that pair with a new bridging constraint.
The sheaf analysis associated with a resolution state.
δ² = 0: the coboundary of a coboundary is zero.
Discrete de Rham duality: H^k ≅ Hom(H_k, R).
Sheaf cohomology equals simplicial cohomology for constant sheaves.
Local-global principle: H^1(K; F) = 0 implies all local sections glue to global sections.
Kernel-produced verification proofs attesting to algebraic properties of UOR objects and operations.
A kernel-produced attestation that a given algebraic property holds. The root class for all proof types.
A proof of coherence: the type system and ring structure are mutually consistent at a given quantum level.
A proof confirmed by exhaustive execution over R_n at a specific quantum level. The kernel ran the identity against all 2^n inputs and observed that it holds. The proof:atWittLevel property records the level; proof:witness links to the WitnessData. CriticalIdentityProof is a subclass of ComputationCertificate.
A proof that follows from previously established axioms or definitions by equational, structural, or topological reasoning. The proof:derivationWitness property links to a derivation:Derivation individual recording the rewrite chain. All pipeline, constraint, observable, and topological identities are AxiomaticDerivations.
A proof of the critical identity: neg(bnot(x)) = succ(x) for all x in R_n. This is the foundational theorem of the UOR kernel.
Supporting data for a proof: specific examples, counter-examples checked, or intermediate computation results.
A formal witness that a topological signature (χ, β_k) is impossible to achieve for any ConstrainedType. Carries the algebraic reason and the verification domain grounding the impossibility.
A formal record of a morphospace boundary point — either an achievable or forbidden topological signature. Aggregated by MorphospaceBoundary to form the queryable morphospace map.
An aggregate of ImpossibilityWitness instances forming the queryable morphospace map. SPARQL over this structure answers achievability queries in O(1).
A proof by structural induction on the quantum level index k. Carries a base case proof, an inductive step proof, and the minimum k for which the induction holds.
A controlled vocabulary of proof methods. Each proof individual carries exactly one strategy from this vocabulary, enabling compilation to verified theorem provers.
Root AST node for proof construction terms. Distinct from schema:TermExpression which represents mathematical terms; DerivationTerm represents proof constructions (tactic applications, lemma invocations, induction scaffolding).
A proof step applying a named tactic (from ProofStrategy) with arguments. Maps to a Lean4 tactic invocation.
A proof step invoking a previously proved identity as a lemma. References the identity via proof:dependsOn.
A proof step performing structural induction: base case derivation, inductive hypothesis, and step derivation.
A proof step performing exhaustive computation at a specific quantum level as verification witness.
Whether this proof has been verified by the kernel.
The time at which this proof was produced.
Human-readable statement of the critical identity proven. E.g., 'neg(bnot(x)) = succ(x) for all x in R_n'. Annotation only — proof:provesIdentity is the typed reference.
A specific input value used as a witness for the critical identity check.
Whether the identity neg(bnot(x)) = succ(x) holds for this specific witness.
The algebraic identity this proof establishes. Provides a canonical object reference alongside the existing proof:criticalIdentity string property, which remains for human readability.
The quantum level at which this computation certificate was produced. A ComputationCertificate at schema:Q0 confirms the identity holds for all 256 inputs of R_8. A certificate at schema:Q1 confirms it for all 65,536 inputs of R_16.
Human-readable quantum level note, e.g. 'n=8, 256 inputs'. Annotation only — proof:atWittLevel is the typed assertion.
True when this axiomatic derivation holds for all quantum levels by the definition of Z/(2^n)Z. False when the derivation depends on a property specific to a particular ring size. All current AxiomaticDerivation individuals in the spec carry universalScope true.
The derivation chain that witnesses this axiomatic derivation. Links a proof:AxiomaticDerivation to the derivation:Derivation individual recording the rewrite sequence. Optional at the spec level — the conformance suite requires only that the proof individual exists; full derivation chains live in generated artifacts.
The topological signature (χ, β_k) that this ImpossibilityWitness formally forbids, expressed as a symbolic notation string (e.g., 'β₀ = 0').
Human-readable statement of the algebraic reason the signature is impossible (e.g., 'β₀ = 0 violates MS_1').
The verification domain grounding the impossibility (e.g., Pipeline for β₀ = 0, Algebraic for χ > n).
The achievability classification of a proof-linked observable signature: Achievable or Forbidden.
The specific quantum level at which an empirical verification or impossibility witness was established.
Links a MorphospaceBoundary to one of its constituent MorphospaceRecord individuals.
Whether this MorphospaceRecord represents an impossibility boundary (from below) or an achievability boundary (from above).
The proof that the claim holds at the base level k_0.
The proof that if the claim holds at Q_k, it holds at Q_{k+1}.
The minimum k for which the induction is valid.
The proof method from the ProofStrategy controlled vocabulary. Determines the compilation target (e.g., `by ring`, `by simp`, `by induction`).
An identity that this proof depends on as a lemma. Forms the proof dependency DAG. Leaf proofs (provable from definitions alone) have no dependsOn assertions.
The formal proof construction term: a DerivationTerm AST node encoding the tactic script, lemma chain, or induction scaffold that constitutes the proof.
Follows from ZMod ring axioms. Lean4 tactic: `by ring`.
Decidable at Q0 by exhaustive evaluation. Lean4: `by native_decide`.
Induction on bit width n. Lean4: `by induction n`.
From dihedral group presentation. Lean4: `by group`.
By simplification with cited lemmas. Lean4: `by simp [lemmalist]`.
By Chinese Remainder Theorem. Lean4: `by exact ZMod.chineseRemainder ...`.
By Euler-Poincare formula applied to the constraint nerve.
By Ostrowski product formula or derived valuation arguments.
By composing proofs of sub-identities. Lean4: `by exact ...`.
By deriving contradiction for impossibility witnesses. Lean4: `by contradiction`.
By computation at a specified quantum level. Lean4: `by native_decide`.
Computation certificate for the critical identity neg(bnot(x)) = succ(x) at Q0.
Axiomatic derivation of the critical identity neg(bnot(x)) = succ(x). Holds at all quantum levels.
Computation certificate for phi_1 at Q0.
Computation certificate for phi_2 at Q0.
Computation certificate for phi_3 at Q0.
Computation certificate for phi_4 at Q0.
Computation certificate for phi_5 at Q0.
Computation certificate for phi_6 at Q0.
Axiomatic derivation of AD_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AD_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of R_A1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of R_A2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of R_A3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of R_A4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of R_A5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of R_A6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of R_M1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of R_M2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of R_M3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of R_M4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of R_M5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_7. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_8. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_9. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_10. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_11. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_12. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of B_13. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of X_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of X_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of X_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of X_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of X_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of X_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of X_7. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of D_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of D_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of D_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of D_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of U_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of U_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of U_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of U_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of U_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AG_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AG_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AG_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AG_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CA_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CA_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CA_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CA_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CA_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CA_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of C_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of C_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of C_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of C_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of C_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of C_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CDI. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CL_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CL_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CL_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CL_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CL_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CM_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CM_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CM_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CR_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CR_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CR_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CR_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CR_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of F_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of F_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of F_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of F_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FL_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FL_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FL_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FL_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FPM_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FPM_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FPM_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FPM_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FPM_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FPM_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FPM_7. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FS_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FS_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FS_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FS_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FS_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FS_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of FS_7. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of RE_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of IR_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of IR_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of IR_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of IR_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of SF_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of SF_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of RD_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of RD_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of SE_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of SE_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of SE_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of SE_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OO_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OO_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OO_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OO_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OO_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CB_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CB_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CB_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CB_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CB_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CB_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_M1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_M2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_M3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_M4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_M5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_M6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_C1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_C2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_C3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_H1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_H2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_H3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_P1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_P2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of OB_P3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CT_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CT_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CT_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CT_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CF_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CF_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CF_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of CF_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of HG_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of HG_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of HG_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of HG_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of HG_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_C1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_C2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_C3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_C4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_I1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_I2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_I3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_I4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_I5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_E1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_E2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_E3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_E4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_A1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_A2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_A3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of T_A4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AU_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AU_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AU_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AU_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AU_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of EF_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of EF_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of EF_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of EF_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of EF_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of EF_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of EF_7. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AA_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AA_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AA_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AA_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AA_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AA_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AM_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AM_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AM_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AM_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of TH_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of TH_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of TH_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of TH_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of TH_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of TH_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of TH_7. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of TH_8. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of TH_9. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of TH_10. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AR_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AR_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AR_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of AR_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Inductive proof of AR_5: greedy vs adiabatic cost difference is at most 5%. Base case at Q0 by exhaustive evaluation; inductive step by QLS_5 (identity preservation under lift).
Axiomatic derivation of PD_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of PD_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of PD_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of PD_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of PD_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of RC_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of RC_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of RC_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of RC_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of RC_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of DC_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of DC_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of DC_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of DC_4. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of DC_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of DC_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of DC_7. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of DC_8. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of DC_9. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of DC_10. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of DC_11. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of HA_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of HA_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of HA_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of IT_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of IT_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of IT_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of IT_7a. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of IT_7b. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of IT_7c. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of IT_7d. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of psi_1. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of psi_2. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of psi_3. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of psi_5. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of psi_6. Holds at all quantum levels by definition of Z/(2^n)Z.
Axiomatic derivation of homology:boundarySquaredZero. Holds at all quantum levels by topological reasoning.
Axiomatic derivation of homology:psi_4. Holds at all quantum levels by topological reasoning.
Axiomatic derivation of homology:indexBridge. Holds at all quantum levels by topological reasoning.
Axiomatic derivation of cohomology:coboundarySquaredZero. Holds at all quantum levels by topological reasoning.
Axiomatic derivation of cohomology:deRhamDuality. Holds at all quantum levels by topological reasoning.
Axiomatic derivation of cohomology:sheafCohomologyBridge. Holds at all quantum levels by topological reasoning.
Axiomatic derivation of cohomology:localGlobalPrinciple. Holds at all quantum levels by topological reasoning.
Axiomatic derivation of the Surface Symmetry Theorem. Holds at all quantum levels: the composite P∘Π∘G is a well-typed morphism whenever G and P share the same state:Frame. Follows from the definition of the shared-frame condition and the type-equivalence algebra.
Proof that a CompleteType T satisfies: resolution(x, T) terminates in O(1) for all x ∈ R_n. Follows from IT_7d: when χ(N(C)) = n and all β_k = 0, the resolver has no topological obstructions.
Proof that the ψ pipeline is monotone: each constraint application cannot increase the site deficit. Derived from the definition of the partition refinement order.
Proof that a CompletenessCertificate implies CompleteType: the certificate attestation is only issued when IT_7d holds, by construction of the CompletenessResolver.
Proof that the CompletenessAuditTrail witnessCount equals the number of CompletenessWitness records in the trail. Structural invariant of the audit accumulation protocol.
Proof that the CechNerve nerve computation is deterministic: the same constraint set always produces the same nerve topology. Follows from the nerve functor being a functor (functoriality).
Universal proof that neg(bnot(x)) = succ(x) in Z/(2^n)Z for all n ≥ 1. Derived symbolically from ring axioms: bnot is bitwise complement, neg is two's complement negation, succ is modular increment. The critical identity in universal form.
Universal proof that the ring carrier set size is exactly 2^n for all n ≥ 1. Follows from the definition of Z/(2^n)Z.
Universal proof that Landauer erasure cost scales as n × k_B T ln 2 at quantum level n. Follows from the thermodynamic interpretation: each bit erased from an n-bit ring costs k_B T ln 2.
Universal proof that the dihedral group D_{2^n} action on Z/(2^n)Z is faithful for all n ≥ 1. The stabilizer of any element is trivial under the full dihedral action.
Universal proof that canonical form rewriting terminates at all quantum levels. The rewriting system is terminating by lexicographic descent on the term complexity measure.
Universal proof that the completeness criterion χ(N(C)) = n generalizes to all quantum levels. Derived from the definition of the nerve construction and the Euler characteristic formula for simplicial complexes.
Universal proof of the ring topology Euler characteristic identity: χ = 1 − n at quantum level n. Derived from the CW decomposition of the n-dimensional torus formed by the ring's cyclic group action.
Proof of binding monotonicity: freeRank(B_{i+1}) ≤ freeRank(B_i) for all i in a Session. Follows from the definition of the BindingAccumulator: each appended binding either pins sites or is a no-op; it never frees them.
Proof that the empty session is the identity element of the session algebra: freeRank(B_0) = total site space. The empty accumulator has no pinned sites by definition.
Proof of session convergence: a session terminates iff freeRank reaches its minimum (the maximum pinned by the given constraint set). Follows from the compactness of the site space and monotonicity.
Proof that disjoint bindings compose without site conflict: if two bindings address disjoint site sets, their composition is well-defined and their union is also a valid binding.
Proof of contradiction detection correctness: ContradictionBoundary fires iff there exist bindings b, b' in the same Context with the same address, different datum, and same constraint. This is the minimal condition for type contradiction.
Proof of nerve realisability: for any target profile with χ* ≤ n and β₀* = 1, there exists a ConstrainedType whose constraint nerve realises the target. Follows from the constructive synthesis algorithm.
Proof of minimal basis bound: the MinimalConstraintBasis for the IT_7d target has size exactly n. Follows from the site-by-site construction and the minimality criterion.
Proof of synthesis monotonicity: adding a constraint never decreases the Euler characteristic of the constraint nerve. Follows from the nerve inclusion principle.
Proof of synthesis convergence: the TypeSynthesisResolver terminates in at most n steps. Follows from monotonicity (TS_3) and the finite site budget bound.
Proof of synthesis-certification duality: a SynthesizedType achieves IT_7d iff the CompletenessResolver certifies it as CompleteType. The duality follows from the shared topological criterion.
Proof of Jacobian-guided synthesis efficiency: the Jacobian oracle reduces expected steps from O(n²) to O(n log n). Follows from the information content of the Jacobian at each synthesis step.
Proof of unreachable signatures: β₀ = 0 is unreachable by any non-empty ConstrainedType. Follows from the nerve connectedness of non-empty constraint sets.
Proof of lift unobstructedness criterion: WittLift T' is CompleteType iff the spectral sequence collapses at E_2. Follows from the Leray spectral sequence of the quantum level extension.
Proof of obstruction localisation: a non-trivial LiftObstruction is localised to a specific site at bit position n+1. Follows from the local-to-global structure of the constraint nerve.
Proof of monotone lifting: basisSize(T') = basisSize(T) + 1 for trivially obstructed lifts. Follows from the minimal basis construction at Q_{n+1}.
Proof of spectral sequence convergence bound: the spectral sequence converges by page E_{d+2} for depth-d configurations. Follows from the filtration length of the constraint nerve chain complex.
Proof of universal identity preservation under quantum lifts: every universallyValid identity holds in the lifted ring. Follows from the universal validity definition and ring extension properties.
Proof of ψ-pipeline universality for quantum lifts: the ψ-pipeline produces a valid ChainComplex for any WittLift. Follows from the functorial construction of the chain complex.
Base case for QLS_1 at Q0: lift unobstructedness holds trivially for 8-bit rings where the constraint nerve is contractible.
Base case for QLS_2 at Q0: obstruction localisation holds at the 8-bit level where sites are directly inspectable.
Inductive step for QLS_2: if obstruction is localised at Q_k, the local-to-global structure of the constraint nerve preserves localisation at Q_{k+1}.
Base case for QLS_3 at Q0: monotone lifting basis size increment holds trivially for 8-bit to 16-bit extension.
Inductive step for QLS_3: the minimal basis construction at Q_{k+1} adds exactly one element from the trivially obstructed site.
Base case for QLS_4 at Q0: spectral sequence convergence at E_{d+2} holds for 8-bit filtrations by direct computation.
Inductive step for QLS_4: filtration length at Q_{k+1} extends by at most one page from Q_k, preserving the E_{d+2} bound.
Base case for QLS_5 at Q0: universallyValid identities hold in the 8-bit ring by definition of universal validity.
Base case for QLS_6 at Q0: the psi-pipeline produces a valid ChainComplex for 8-bit WittLifts by direct construction.
Inductive step for QLS_6: the functorial construction of the chain complex commutes with quantum level extension.
Base case for QT_3: resolved basis size formula holds for chain length 1 by direct construction.
Base case for QT_5: LiftChainCertificate existence for tower height 1 follows from single-step certificate issuance.
Base case for AR_5 at Q0: greedy vs adiabatic cost difference verified by exhaustive enumeration over Z/256Z.
Inductive step for AR_5: if greedy vs adiabatic bound holds at Q_k, it holds at Q_{k+1} by QLS_5 (universal identity preservation under quantum lift).
Base case for QM_6 at Q0: amplitude index set equals monotone pinning trajectories by exhaustive trajectory enumeration over the 8-bit site lattice.
Inductive step for QM_6: monotone pinning trajectories at Q_{k+1} extend those at Q_k by the site lattice ordering (monotone extension property).
Proof of holonomy group containment: HolonomyGroup(T) ≤ D_{2^n}. Follows from the fact that all constraint applications are dihedral group elements.
Proof of additive flatness: additive constraints (ResidueConstraint, DepthConstraint) generate only the identity in D_{2^n}. Follows from the additive structure of the dihedral action.
Proof of dihedral generation: neg and bnot together generate D_{2^n}. Follows from the standard presentation of the dihedral group by involutions.
Proof of holonomy-Betti implication: non-trivial holonomy implies β₁ ≥ 1. Follows from the fact that a non-trivial monodromy requires a topological loop in the constraint nerve.
Proof of CompleteType holonomy: IT_7d (β₁ = 0) implies trivial holonomy (FlatType). Follows from MN_4 contrapositive: trivial holonomy ← β₁ = 0.
Proof of monodromy composition: the monodromy map is a group homomorphism from the loop space to D_{2^n}. Follows from the composition of dihedral group elements.
Proof of TwistedType obstruction class: a TwistedType always contributes a non-zero class to H²(N(C(T')); ℤ/2ℤ) for any WittLift T'. Follows from MN_4 and the obstruction theory of dihedral torsors.
Proof of PT_1: product type site additivity. siteBudget(A × B) = siteBudget(A) + siteBudget(B). Follows from the definition of ProductType as an independent concatenation of site spaces.
Proof of PT_2: product type partition factorisation. partition(A × B) = partition(A) ⊗ partition(B). Follows from the tensor product structure of constraint nerves over independent site spaces.
Proof of PT_3: product type Euler characteristic additivity. χ(N(C(A × B))) = χ(N(C(A))) + χ(N(C(B))). Follows from the Künneth formula applied to the join of constraint nerves.
Proof of PT_4: product type entropy additivity. S(A × B) = S(A) + S(B). Follows from PT_1 (site additivity) and TH_1 (S = freeRank × ln 2).
Proof of ST_1: sum type site budget maximum. siteBudget(A + B) = max(siteBudget(A), siteBudget(B)). Follows from SumType requiring capacity for the larger variant.
Proof of ST_2: sum type entropy. S(A + B) = ln 2 + max(S(A), S(B)). The ln 2 term accounts for the variant discriminant bit; the max reflects that only one variant is active at a time.
Proof of SC_1: context temperature. T_ctx(C) = freeRank(C) × ln 2 / n. Derived from TH_1 normalized per site.
Proof of SC_2: saturation degree. σ(C) = (n − freeRank(C)) / n. Definitional identity.
Proof of SC_3: saturation monotonicity. Corollary of SR_1 through order-reversing SC_2.
Proof of SC_4: ground state equivalence. Four equivalent conditions for full saturation derived from SC_2, TH_1, SC_1.
Proof of SC_5: O(1) resolution guarantee at saturation. Derived from SR_2 and FreeRank.isClosed at freeRank = 0.
Proof of SC_6: pre-reduction of effective budget. Derived from session-scoped site reduction at partial saturation.
Proof of SC_7: thermodynamic cooling cost. n site-closures at Landauer cost each via SR_1 + TH_4.
Proof of MS_1: connectivity lower bound β₀ ≥ 1. Formalisation of TS_7.
Proof of MS_2: Euler capacity ceiling χ ≤ n. Derived from TS_1 constraint nerve dimension bound.
Proof of MS_3: Betti monotonicity under constraint addition. Formalisation of TS_3.
Proof of MS_4: level-relative achievability. Derived from WittLift construction (Amendment 29).
Proof of MS_5: empirical completeness convergence. Convergence statement for verification accumulation.
Proof of GD_1: geodesic condition. Dual condition from AR_1 ordering + DC_10 selection.
Proof of GD_2: geodesic entropy bound. Each step on a geodesic erases exactly ln 2 nats.
Proof of GD_3: total geodesic cost equals Landauer bound TH_4 with equality.
Proof of GD_4: geodesic uniqueness up to step-order equivalence. Equal-J_k permutations are interchangeable.
Proof of GD_5: subgeodesic detectability via step-by-step J_k check.
Proof of QM_1: von Neumann–Landauer bridge. S_vN equals Landauer erasure cost at the Landauer temperature β* = ln 2.
Proof of QM_2: measurement as site topology change. Projective collapse ≅ classical ResidueConstraint pinning.
Proof of QM_3: superposition entropy bound. 0 ≤ S_vN ≤ ln 2 for single-site superpositions.
Proof of QM_4: collapse idempotence. Re-measurement of a collapsed state is a no-op.
Proof of QM_5: amplitude normalization (Born rule). Σ|αᵢ|² = 1 for well-formed SuperposedSiteState.
Proof of RC_6: amplitude renormalization. Division by norm yields a normalized SuperposedSiteState.
Proof of FPM_8: partition exhaustiveness. The four component cardinalities sum to 2ⁿ.
Proof of FPM_9: exterior membership criterion. x ∈ Ext(T) iff x ∉ carrier(T).
Proof of MN_8: holonomy classification covering. Every ConstrainedType is flat xor twisted.
Proof of QL_8: quantum level chain inverse. wittLevelPredecessor is the left inverse of nextLevel.
Proof of D_7: dihedral composition rule from the semidirect product presentation.
Proof of SP_1: classical embedding. Superposition resolution of a classical datum reduces to classical resolution.
Proof of SP_2: collapse–resolve commutativity. The collapse and resolve operations commute.
Proof of SP_3: amplitude preservation. The SuperpositionResolver preserves the normalized amplitude vector.
Proof of SP_4: Born rule outcome probability. P(collapse to site k) = |α_k|².
Proof of PT_2a: product type partition tensor. Π(A × B) = PartitionProduct(Π(A), Π(B)).
Proof of PT_2b: sum type partition coproduct. Π(A + B) = PartitionCoproduct(Π(A), Π(B)).
Proof of GD_6: geodesic predicate decomposition. isGeodesic = isAR1Ordered ∧ isDC10Selected.
β₀ = 0 violates MS_1: constraint nerve of non-empty set is connected
Impossibility witness for MS_1: β₀ = 0 is forbidden for any non-empty ConstrainedType because the constraint nerve is always connected.
χ > n violates MS_2: Euler characteristic bounded by quantum level
Impossibility witness for MS_2: χ > n is forbidden at quantum level n. The Euler characteristic cannot exceed the quantum level.
Morphospace record: the IT_7d completeness target χ = n is achievable (sits at the ceiling of MS_2).
Morphospace record: the connectivity lower bound β₀ ≥ 1 marks the forbidden region from below.
Proof of tower chain validity by induction on chain length.
Proof of obstruction count bound: direct from QLS_2 localization.
Proof of resolved basis size formula by induction on chain length.
Proof of flat tower characterization: isFlat iff trivial holonomy at every step.
Proof of LiftChainCertificate existence by induction on tower height.
Proof of single-step reduction: QT_3 with chainLength=1 reduces to QLS_3.
Proof of CC_PINS: carry-constraint site-pinning map follows from ring carry propagation rule.
Computation certificate for CC_COST_SITE: exhaustive enumeration at Q0 confirms |pinsSites| = popcount + 1.
Proof of jsat_RR: CRT joint satisfiability follows from the Chinese Remainder Theorem.
Proof of jsat_CR: carry-residue joint satisfiability follows from the carry stopping rule and residue class intersection.
Computation certificate for jsat_CC: bit-pattern exhaustive enumeration at Q0.
Proof of D_8: dihedral inverse formula follows from D_5 group presentation and D_7 composition rule.
Proof of D_9: reflection order 2 follows from D_7 composition: (r^k s)(r^k s) = identity.
Proof of EXP_1: monotone carrier characterization follows from site lattice monotonicity.
Computation certificate for EXP_2: principal filter count verified by exhaustive enumeration at Q0.
Proof of EXP_3: SumType carrier is coproduct by definitional architectural decision.
Proof of ST_3: Euler characteristic additivity for disjoint simplicial complexes.
Proof of ST_4: Betti number additivity via Mayer-Vietoris for disjoint union.
Proof of ST_5: SumType completeness transfer follows from ST_3 + ST_4 + IT_7d.
Inductive proof of TS_8: minimum constraint count for beta_1 = k is 2k + 1. Base case at k=1 requires 3 mutually overlapping constraints.
Inductive proof of TS_9: TypeSynthesisResolver terminates in at most 2^n steps. Base case at n=1 has 2 constraint combinations.
Proof of TS_10: ForbiddenSignature membership follows from exhaustive enumeration bound.
Proof of QT_8: ObstructionChain length bound follows from QLS_2 and spectral sequence convergence.
Proof of QT_9: TowerCompletenessResolver termination follows from finite chain length and QT_8 bound.
Proof of COEFF_1: Z/2Z coefficient ring is definitional, consistent with MN_7.
Proof of GO_1: cohomology killing lemma for GluingObstruction feedback.
Proof of SR_6: saturation re-entry free count follows from SR_1 monotone accumulation and SC_2.
Proof of SR_7: saturation degree degradation follows from SC_2 definition and SR_1 monotonicity.
Inductive proof of QM_6: amplitude index set equals monotone pinning trajectories. Base case at Q0 by exhaustive trajectory enumeration; inductive step by site lattice ordering.
Proof of CIC_1: TransformCertificate issuance coverage.
Proof of CIC_2: IsometryCertificate issuance coverage.
Proof of CIC_3: InvolutionCertificate issuance coverage.
Proof of CIC_4: GroundingCertificate issuance coverage.
Proof of CIC_5: GeodesicCertificate issuance coverage.
Proof of CIC_6: MeasurementCertificate issuance coverage.
Axiomatic derivation of CIC_7: BornRuleVerification issuance coverage. Follows by composition from corrected OA_4 (product formula chain) and QM_5 (amplitude normalization).
Proof of GC_1: GroundingCertificate issuance coverage.
Proof of SR_8: session composition tower consistency.
Proof of SR_9: ContextLease site disjointness.
Proof of SR_10: ExecutionPolicy confluence.
Proof of MC_1: lease partition conserves total budget.
Proof of MC_2: per-lease binding monotonicity.
Proof of MC_3: composition freeRank inclusion-exclusion.
Proof of MC_4: disjoint-lease composition additivity.
Proof of MC_5: policy-invariant final binding set.
Proof of MC_6: full lease coverage implies composed saturation.
Proof of MC_7: distributed O(1) resolution.
Proof of MC_8: parallelism bound on per-session resolution work.
Axiomatic derivation of WC_1: Witt coordinate = bit coordinate at p=2.
Axiomatic derivation of WC_2: Witt sum correction = carry.
Axiomatic derivation of WC_3: carry recurrence = Witt polynomial recurrence.
Axiomatic derivation of WC_4: δ-correction = single-level carry.
Axiomatic derivation of WC_5: LiftObstruction = δ nonvanishing.
Axiomatic derivation of WC_6: metric discrepancy = Witt defect.
Axiomatic derivation of WC_7: D_1 = Witt truncation order.
Axiomatic derivation of WC_8: D_3 = Witt-Burnside conjugation.
Axiomatic derivation of WC_9: D_4 = reflection composition.
Axiomatic derivation of WC_10: Frobenius = identity on W_n(F_2).
Axiomatic derivation of WC_11: Verschiebung = doubling.
Axiomatic derivation of WC_12: δ = squaring defect / 2.
Axiomatic derivation of OA_1: Ostrowski product formula at p=2.
Axiomatic derivation of OA_2: crossing cost = ln 2.
Axiomatic derivation of OA_3: Landauer cost grounding via product formula.
Axiomatic derivation of OA_4: Born rule bridge follows from the product formula chain OA_1 (Ostrowski) -> OA_2 (crossing cost) -> OA_3 (Landauer grounding) -> OA_4.
Axiomatic derivation of OA_5: entropy per δ-level = crossing cost.
Axiomatic derivation of HT_1: the constraint nerve satisfies the Kan extension condition.
Axiomatic derivation of HT_2: path components recover Betti number β₀.
Axiomatic derivation of HT_3: π₁ factors through HolonomyGroup.
Axiomatic derivation of HT_4: higher homotopy groups vanish above dimension.
Axiomatic derivation of HT_5: 1-truncation determines flat/twisted classification.
Axiomatic derivation of HT_6: trivial k-invariants imply spectral collapse.
Axiomatic derivation of HT_7: Whitehead product detects lift obstructions.
Axiomatic derivation of HT_8: Hurewicz isomorphism for first non-vanishing group.
Axiomatic derivation of ψ_7: KanComplex to PostnikovTower functor.
Axiomatic derivation of ψ_8: PostnikovTower to HomotopyGroups extraction.
Axiomatic derivation of ψ_9: HomotopyGroups to KInvariants computation.
Axiomatic derivation of HP_1: pipeline composition ψ_7 ∘ ψ_1.
Axiomatic derivation of HP_2: homotopy extraction agrees with homology on truncation.
Axiomatic derivation of HP_3: ψ_9 detects QLS_4 convergence.
Axiomatic derivation of HP_4: HomotopyResolver complexity bound.
Axiomatic derivation of MD_1: moduli dimension equals basis cardinality.
Axiomatic derivation of MD_2: automorphism group is subgroup of D_{2^n}.
Axiomatic derivation of MD_3: first-order deformations parameterize tangent space.
Axiomatic derivation of MD_4: obstruction space equals LiftObstruction.
Axiomatic derivation of MD_5: FlatType stratum is open (codimension 0).
Axiomatic derivation of MD_6: TwistedType strata have codimension at least 1.
Axiomatic derivation of MD_7: versal deformation exists when unobstructed.
Axiomatic derivation of MD_8: completeness-preserving iff obstruction vanishes along path.
Axiomatic derivation of MD_9: tower map site dimension is 1 when unobstructed.
Axiomatic derivation of MD_10: tower map site empty iff twisted at every level.
Axiomatic derivation of MR_1: moduli resolver agrees with MorphospaceBoundary.
Axiomatic derivation of MR_2: stratification record is complete.
Axiomatic derivation of MR_3: moduli resolver complexity bound.
Axiomatic derivation of MR_4: moduli-morphospace consistency.
Axiomatic derivation of CY_1: carry generation condition.
Axiomatic derivation of CY_2: carry propagation condition.
Axiomatic derivation of CY_3: carry kill condition.
Axiomatic derivation of CY_4: d_Δ as carry–Hamming discrepancy.
Axiomatic derivation of CY_5: optimal encoding theorem.
Axiomatic derivation of CY_6: site ordering theorem.
Axiomatic derivation of CY_7: carry lookahead via prefix computation.
Axiomatic derivation of BM_1: saturation metric definition.
Axiomatic derivation of BM_2: Euler characteristic formula.
Axiomatic derivation of BM_3: index theorem linking all six metrics.
Axiomatic derivation of BM_4: Jacobian vanishes on pinned sites.
Axiomatic derivation of BM_5: d_delta equals Witt defect.
Axiomatic derivation of BM_6: metric composition tower.
Axiomatic derivation of GL_1: σ as lower adjoint.
Axiomatic derivation of GL_2: r as complement of upper adjoint.
Axiomatic derivation of GL_3: completeness as Galois fixpoint.
Axiomatic derivation of GL_4: Galois order reversal.
Axiomatic derivation of NV_1: nerve additivity for disjoint domains.
Axiomatic derivation of NV_2: Mayer–Vietoris for constraint nerves.
Axiomatic derivation of NV_3: Betti number bounded change.
Axiomatic derivation of NV_4: accumulation monotonicity.
Axiomatic derivation of SD_1: scalar grounding identity.
Axiomatic derivation of SD_2: symbol grounding identity.
Axiomatic derivation of SD_3: sequence free monoid identity.
Axiomatic derivation of SD_4: tuple site additivity.
Axiomatic derivation of SD_5: graph nerve equality.
Axiomatic derivation of SD_6: set permutation invariance.
Axiomatic derivation of SD_7: tree acyclicity constraint.
Axiomatic derivation of SD_8: table functorial decomposition.
Axiomatic derivation of DD_1: dispatch determinism.
Axiomatic derivation of DD_2: dispatch coverage.
Axiomatic derivation of PI_1: inference idempotence.
Axiomatic derivation of PI_2: inference soundness.
Axiomatic derivation of PI_3: inference composition.
Axiomatic derivation of PI_4: inference complexity.
Axiomatic derivation of PI_5: inference coherence.
Axiomatic derivation of PA_1: accumulation permutation invariance.
Axiomatic derivation of PA_2: accumulation monotonicity.
Axiomatic derivation of PA_3: accumulation soundness.
Axiomatic derivation of PA_4: accumulation base preservation.
Axiomatic derivation of PA_5: accumulation identity element.
Axiomatic derivation of PL_1: lease disjointness.
Axiomatic derivation of PL_2: lease conservation.
Axiomatic derivation of PL_3: lease coverage.
Axiomatic derivation of PK_1: composition validity.
Axiomatic derivation of PK_2: distributed resolution.
Axiomatic derivation of PP_1: pipeline unification.
Axiomatic derivation of PE_1: state initialization.
Axiomatic derivation of PE_2: resolver dispatch.
Axiomatic derivation of PE_3: ring address grounding.
Axiomatic derivation of PE_4: constraint resolution.
Axiomatic derivation of PE_5: consistent accumulation.
Axiomatic derivation of PE_6: coherent extraction.
Axiomatic derivation of PE_7: full pipeline composition.
Axiomatic derivation of PM_1: phase rotation.
Axiomatic derivation of PM_2: phase gate check.
Axiomatic derivation of PM_3: conjugate rollback.
Axiomatic derivation of PM_4: rollback involution.
Axiomatic derivation of PM_5: epoch saturation preservation.
Axiomatic derivation of PM_6: service window context.
Axiomatic derivation of PM_7: machine determinism.
Axiomatic derivation of ER_1: guard satisfaction.
Axiomatic derivation of ER_2: effect atomicity.
Axiomatic derivation of ER_3: guard purity.
Axiomatic derivation of ER_4: intra-stage commutativity.
Axiomatic derivation of EA_1: epoch boundary reset.
Axiomatic derivation of EA_2: saturation monotonicity.
Axiomatic derivation of EA_3: service window bound.
Axiomatic derivation of EA_4: epoch admission exclusivity.
Axiomatic derivation of OE_1: stage fusion.
Axiomatic derivation of OE_2: effect commutativity.
Axiomatic derivation of OE_3: lease parallelism.
Axiomatic derivation of OE_4a: fusion semantics preservation.
Axiomatic derivation of OE_4b: commutation outcome preservation.
Axiomatic derivation of OE_4c: parallelism coverage preservation.
Axiomatic derivation of CS_1: bounded stage cost.
Axiomatic derivation of CS_2: additive pipeline cost.
Axiomatic derivation of CS_3: bounded rollback cost.
Axiomatic derivation of CS_4: constant preflight cost.
Axiomatic derivation of CS_5: total reduction cost bound.
Axiomatic derivation of FA_1: query liveness.
Axiomatic derivation of FA_2: no starvation.
Axiomatic derivation of FA_3: fair lease allocation.
Axiomatic derivation of SW_1: memory boundedness.
Axiomatic derivation of SW_2: saturation invariance.
Axiomatic derivation of SW_3: eviction releases resources.
Axiomatic derivation of SW_4: non-empty window.
Axiomatic derivation of LS_1: suspension preserves pinned state.
Axiomatic derivation of LS_2: expiry releases resources.
Axiomatic derivation of LS_3: checkpoint restore idempotence.
Axiomatic derivation of LS_4: suspend-resume round-trip.
Axiomatic derivation of TJ_1: AllOrNothing rollback.
Axiomatic derivation of TJ_2: BestEffort partial commit.
Axiomatic derivation of TJ_3: epoch-scoped atomicity.
Axiomatic derivation of AP_1: saturation monotonicity.
Axiomatic derivation of AP_2: quality improvement.
Axiomatic derivation of AP_3: deferred query liveness.
Axiomatic derivation of EC_1: phase half-turn convergence.
Axiomatic derivation of EC_2: conjugate involution.
Axiomatic derivation of EC_3: pairwise commutator convergence.
Axiomatic derivation of EC_4: triple associator convergence.
Axiomatic derivation of EC_4a: associator monotonicity.
Axiomatic derivation of EC_4b: associator finiteness.
Axiomatic derivation of EC_4c: vanishing implies associativity.
Axiomatic derivation of EC_5: Adams termination.
Axiomatic derivation of DA_1: Cayley-Dickson R→C.
Axiomatic derivation of DA_2: Cayley-Dickson C→H.
Axiomatic derivation of DA_3: Cayley-Dickson H→O.
Axiomatic derivation of DA_4: Adams dimension restriction.
Axiomatic derivation of DA_5: convergence-level algebra correspondence.
Axiomatic derivation of DA_6: commutator-commutativity equivalence.
Axiomatic derivation of DA_7: associator-associativity equivalence.
Axiomatic derivation of IN_1: interaction cost.
Axiomatic derivation of IN_2: disjoint leases commute.
Axiomatic derivation of IN_3: shared sites nonzero commutator.
Axiomatic derivation of IN_4: negotiation convergence.
Axiomatic derivation of IN_5: commutative subspace selection.
Axiomatic derivation of IN_6: pairwise outcome space.
Axiomatic derivation of IN_7: associative subalgebra selection.
Axiomatic derivation of IN_8: nerve Betti coupling bound.
Axiomatic derivation of IN_9: Betti-disagreement associator bound.
Axiomatic derivation of AS_1: δ-ι-κ non-associativity.
Axiomatic derivation of AS_2: ι-α-λ non-associativity.
Axiomatic derivation of AS_3: λ-κ-δ non-associativity.
Axiomatic derivation of AS_4: non-associativity root cause.
Axiomatic derivation of MO_1: monoidal unit law.
Axiomatic derivation of MO_2: monoidal associativity.
Axiomatic derivation of MO_3: certificate composition.
Axiomatic derivation of MO_4: saturation monotonicity.
Axiomatic derivation of MO_5: residual monotonicity.
Axiomatic derivation of OP_1: site additivity.
Axiomatic derivation of OP_2: grounding distributivity.
Axiomatic derivation of OP_3: d_Δ decomposition.
Axiomatic derivation of OP_4: tabular data decomposition.
Axiomatic derivation of OP_5: hierarchical data structure.
Axiomatic derivation of FX_1: pinning site budget decrement.
Axiomatic derivation of FX_2: unbinding site budget increment.
Axiomatic derivation of FX_3: phase budget invariance.
Axiomatic derivation of FX_4: disjoint commutativity.
Axiomatic derivation of FX_5: composite delta additivity.
Axiomatic derivation of FX_6: reversible inverse.
Axiomatic derivation of FX_7: external shape compliance.
Axiomatic derivation of PR_1: predicate totality.
Axiomatic derivation of PR_2: predicate purity.
Axiomatic derivation of PR_3: deterministic dispatch.
Axiomatic derivation of PR_4: deterministic match.
Axiomatic derivation of PR_5: typed guard transition.
Axiomatic derivation of CG_1: typed entry guard.
Axiomatic derivation of CG_2: typed exit guard with effect.
Axiomatic derivation of DIS_1: exhaustive exclusive table.
Axiomatic derivation of DIS_2: deterministic resolver selection.
Axiomatic derivation of PAR_1: disjoint commutativity.
Axiomatic derivation of PAR_2: delta additivity.
Axiomatic derivation of PAR_3: exhaustive partitioning.
Axiomatic derivation of PAR_4: interleaving invariance.
Axiomatic derivation of PAR_5: certificate conjunction.
Axiomatic derivation of HO_1: content-addressed certification.
Axiomatic derivation of HO_2: application certification.
Axiomatic derivation of HO_3: composition certification.
Axiomatic derivation of HO_4: saturation equivalence.
Axiomatic derivation of STR_1: epoch termination.
Axiomatic derivation of STR_2: saturation preservation.
Axiomatic derivation of STR_3: finite prefix computability.
Axiomatic derivation of STR_4: unfold seed initialization.
Axiomatic derivation of STR_5: continuation chaining.
Axiomatic derivation of STR_6: lease expiry budget return.
Axiomatic derivation of FLR_1: coproduct exhaustiveness.
Axiomatic derivation of FLR_2: total computation guarantee.
Axiomatic derivation of FLR_3: sequential propagation.
Axiomatic derivation of FLR_4: parallel independence.
Axiomatic derivation of FLR_5: recovery result.
Axiomatic derivation of FLR_6: conjugate rollback.
Axiomatic derivation of LN_1: exact coverage.
Axiomatic derivation of LN_2: pinning effect.
Axiomatic derivation of LN_3: consumption linearity.
Axiomatic derivation of LN_4: lease budget decrement.
Axiomatic derivation of LN_5: lease expiry return.
Axiomatic derivation of LN_6: geodesic linearity.
Axiomatic derivation of SB_1: constraint superset.
Axiomatic derivation of SB_2: resolution subset.
Axiomatic derivation of SB_3: nerve sub-complex.
Axiomatic derivation of SB_4: covariance.
Axiomatic derivation of SB_5: contravariance.
Axiomatic derivation of SB_6: lattice depth.
Axiomatic derivation of BR_1: strict descent.
Axiomatic derivation of BR_2: depth bound.
Axiomatic derivation of BR_3: termination guarantee.
Axiomatic derivation of BR_4: structural measure.
Axiomatic derivation of BR_5: base predicate zero.
Axiomatic derivation of RG_1: nerve-determined working set.
Axiomatic derivation of RG_2: diameter bound.
Axiomatic derivation of RG_3: addressable space bound.
Axiomatic derivation of RG_4: working set containment.
Axiomatic derivation of IO_1: ingest type conformance.
Axiomatic derivation of IO_2: emit type conformance.
Axiomatic derivation of IO_3: grounding validity.
Axiomatic derivation of IO_4: projection validity.
Axiomatic derivation of IO_5: non-vacuous crossing.
Axiomatic derivation of CS_6: budget solvency rejection.
Axiomatic derivation of CS_7: unit address computation.
Computation witnesses recording term rewriting sequences from original terms to their canonical forms.
A complete term rewriting witness: the full sequence of rewrite steps transforming an original term into its canonical form.
An abstract step in a derivation. Concrete subclasses are RewriteStep (term-level rewriting) and RefinementStep (type-level refinement).
A single rewrite step in a derivation: the application of one rewrite rule to transform a term.
A type-level refinement step: the application of a constraint to narrow a type, pinning additional site coordinates. Complements RewriteStep (term-level) in the derivation hierarchy.
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.
Metrics describing the size and complexity of a term.
A single step in the construction of a SynthesizedType: one constraint added to the synthesis candidate and the resulting change in the constraint nerve's topological signature. Ordered by derivation:stepIndex. Analogous to derivation:RewriteStep in the forward pipeline.
A persistent snapshot of a ConstraintSearchState at a specific SynthesisStep, allowing a TypeSynthesisResolver to resume exploration after interruption. Essential at Q1+ scale where exhaustive synthesis is computationally significant.
The term at the start of the derivation, before any rewriting.
The canonical form produced at the end of the derivation.
The datum value obtained by evaluating the canonical term.
Metrics for the canonical term produced by this derivation.
The typed rewrite rule applied in this step. Provides a structured reference to a named RewriteRule individual, complementing the string-valued derivation:rule property.
The algebraic identity that grounds this rewrite rule. Links a RewriteRule to the op:Identity individual that justifies its application.
The total number of rewrite steps in this derivation.
The number of nodes in the canonical term's syntax tree.
The type before this refinement step was applied.
The constraint that was applied in this refinement step.
The type after this refinement step was applied.
The number of site coordinates pinned by this refinement step.
Zero-based sequential index of this step within the synthesis derivation.
The constraint added in this synthesis step.
The constraint nerve signature before this synthesis step.
The constraint nerve signature after this synthesis step.
The SynthesisStep at which this checkpoint was taken.
The ConstraintSearchState snapshot captured by this checkpoint.
Links a TowerCompletenessResolver to a SynthesisCheckpoint issued at each completed step. Cross-namespace bridge property: domain is resolver:TowerCompletenessResolver.
The rewrite rule applying the critical identity: neg(bnot(x)) → succ(x). Grounded in op:criticalIdentity.
The rewrite rule applying involution cancellation: f(f(x)) → x for any involution f.
The rewrite rule applying associativity to re-bracket nested binary operations.
The rewrite rule applying commutativity to reorder operands of commutative operations.
The rewrite rule eliminating identity elements: add(x, 0) → x, mul(x, 1) → x, xor(x, 0) → x.
The rewrite rule normalizing compound expressions to canonical ordering (e.g., sorting operands by address).
Execution traces recording the sequence of kernel operations, intermediate results, and accumulated metrics for a computation.
A complete record of a kernel computation: the input, output, every operation step, and accumulated metrics.
A single step in a computation trace: one operation applied to produce one output from one or more inputs.
Summary metrics for a computation trace: total steps, accumulated ring distance, and accumulated Hamming distance.
A computation trace that satisfies the dual geodesic condition (GD_1): AR_1-ordered and DC_10-selected. The path of least dissipation through the resolution landscape.
A record of a geodesic condition violation at a specific step of a computation trace. Produced by GeodesicValidator when J_k(step_i) < max_\{free\} J_k(state_i).
A specialized computation step recording a single projective collapse of a SuperposedSiteState. Carries pre-collapse entropy and post-collapse Landauer cost (QM_1).
A single outcome of a projective measurement on a SuperposedSiteState, recording the classical site index (outcomeValue) and its Born-rule probability |α_k|² (outcomeProbability). Multiple outcomes form the probability distribution of a measurement.
The monodromy accumulated by this computation: the net dihedral group element produced by the full operation sequence.
The input datum of this computation step.
The output datum of this computation step.
The operation applied in this computation step.
The zero-based sequential index of this step within its trace.
Total number of computation steps in this trace.
Total ring-metric distance accumulated across all steps.
Total Hamming-metric distance accumulated across all steps.
The certificate that attests to the correctness of this computation trace.
The residual entropy observable remaining after this computation trace, linking to the ThermoObservable taxonomy (TH_9 connection).
Whether this computation trace satisfies the dual geodesic condition (GD_1): AR_1-ordered and DC_10-selected.
The GeodesicCertificate attesting that this trace satisfied both GD_1 conditions.
A GeodesicViolation record indicating where the trace deviated from the geodesic condition.
The entropy cost of a single computation step. On a geodesic, this equals ln 2 for every step (GD_2).
The total entropy cost accumulated across all steps of a trace. On a geodesic, equals freeRank_initial × ln 2 (GD_3).
The Jacobian value J_k at this step, used by the GeodesicValidator to check DC_10 maximality.
Whether the step sequence of this trace follows the AR_1 adiabatic ordering (decreasing freeRank × cost-per-site).
Human-readable description of why a geodesic violation occurred, citing the step index and the unused higher-J_k option.
A MeasurementEvent step within this computation trace.
The von Neumann entropy S_vN of the SuperposedSiteState before projective collapse.
The Landauer cost incurred by the projective collapse. Equals preCollapseEntropy at β* = ln 2 (QM_1).
The step index within the enclosing ComputationTrace at which this projective collapse occurred.
The full pre-collapse amplitude vector of all branches at the time of measurement. Enables Born rule verification (QM_5): P(outcome k) = |α_k|² / Σ|αᵢ|².
Whether this computation trace has steps ordered by the AR_1 adiabatic metric (decreasing freeRank × cost-per-site). One of the two sub-predicates of isGeodesic (GD_6).
Whether each step of this computation trace was selected by the DC_10 Jacobian criterion (maximal J_k among free sites). One of the two sub-predicates of isGeodesic (GD_6).
The classical site index selected by projective collapse in this measurement outcome.
The Born-rule probability of this measurement outcome: |α_k|² where α_k is the amplitude of the collapsed site.
Canonical geodesic trace at quantum level Q0 (n=8). Demonstrates GD_1 through GD_3 at the base level.
Canonical geodesic trace at quantum level Q1 (n=16). Demonstrates geodesic scaling from Q0 to Q1.
Canonical geodesic trace at quantum level Q2 (n=32). Demonstrates geodesic scaling from Q1 to Q2.
Canonical geodesic trace at quantum level Q3 (n=64). Demonstrates geodesic scaling from Q2 to Q3.
Canonical measurement event: collapse of an equal superposition (|α|² = 0.5). Maximum von Neumann entropy S_vN = ln 2. Maximum Landauer cost per QM_1.
Canonical measurement event: collapse of a biased superposition (|α|² = 0.9). Lower entropy than equal superposition. Demonstrates QM_3 bound.
Canonical measurement event: collapse of a classical state (|α|² = 1). Zero entropy, zero Landauer cost. Demonstrates QM_4 idempotence.
Kernel-produced attestation certificates for transforms, isometries, and involutions. Each certificate verifies that a specific structural property holds.
A kernel-produced attestation. The root class for all certificate types.
A certificate attesting to the properties of a morphism:Transform. Certifies that the transform maps source to target correctly.
A certificate attesting that a morphism:Isometry preserves metric distances. Certifies the transform is a metric isometry with respect to the specified metric.
A certificate attesting that an operation is an involution: f(f(x)) = x for all x in R_n.
A certificate attesting that a type:CompleteType satisfies IT_7d: its constraint nerve has χ = n and all Betti numbers β_k = 0. Issued by the kernel after running the full ψ pipeline on the type's constraint set.
An ordered collection of CompletenessWitness records belonging to a CompletenessCertificate. Provides full provenance of the certification process: every constraint applied, every site closed, in sequence.
A certificate attesting that a state:GroundedContext has reached full saturation (σ = 1, freeRank = 0, S = 0, T_ctx = 0) per SC_4. The session-layer dual of CompletenessCertificate.
A certificate attesting that a trace:GeodesicTrace satisfies both GD_1 conditions: AR_1-ordered and DC_10-selected. Transforms ComputationTrace from descriptive to normative.
A certificate attesting that a trace:MeasurementEvent respected the von Neumann–Landauer bridge (QM_1): preCollapseEntropy = postCollapseLandauerCost at β* = ln 2.
A structured evidence bundle attesting that each sub-predicate of the geodesic condition (GD_6) holds independently: isAR1Ordered and isDC10Selected. Linked from GeodesicCertificate via evidenceBundle.
A certificate attesting that a MeasurementEvent outcome probability matches the Born rule: P(outcome k) = |α_k|² (QM_5). Linked from MeasurementCertificate to provide probability distribution verification.
A kernel-issued certificate attesting that a LiftChain from liftSourceLevel to liftTargetLevel is complete.
An ordered collection of per-step evidence records for a LiftChainCertificate.
The type of transform this certificate attests to (e.g., 'isometry', 'embedding', 'action').
The verification method used to produce this certificate (e.g., 'exhaustive_check', 'symbolic_proof', 'sampling').
The operation this certificate applies to.
Whether this certificate has been verified by the kernel.
The Witt level at which this certificate was produced.
The time at which this certificate was issued.
The resource this certificate attests to. Links a certificate to the observable, transform, or other entity it covers.
The TypeDefinition whose completeness this certificate attests. The kernel issues this certificate after running the ψ pipeline on the type's constraint set and confirming IT_7d.
The audit trail attesting the certification provenance. Links a CompletenessCertificate to its ordered sequence of CompletenessWitness records.
Total number of witness steps in this audit trail.
The GroundedContext whose full saturation this certificate attests. Uses IRI string (cert cannot import state).
The GroundingWitness providing step-by-step evidence of the saturation process.
The GeodesicTrace whose geodesic status this certificate attests. Uses IRI string (cert cannot import trace).
The computation trace that this GeodesicCertificate covers. Redundant with certifiedGeodesic but expresses the inverse direction for queryability.
The MeasurementEvent whose QM_1 compliance this certificate attests. Uses IRI string (cert cannot import trace).
The von Neumann entropy S_vN of the pre-measurement SuperposedSiteState, recorded by this certificate.
The Landauer cost incurred by the projective collapse, recorded by this certificate. Equals vonNeumannEntropy at β* = ln 2 per QM_1.
The GeodesicEvidenceBundle attesting to the decomposed sub-predicates (isAR1Ordered, isDC10Selected) of this GeodesicCertificate's geodesic claim.
Whether this BornRuleVerification certificate confirms that all outcome probabilities match the Born rule (QM_5): P(k) = |α_k|² for every site k.
The LiftChain this certificate attests to.
The ordered per-step evidence for this certificate.
The quantum level Q_k at which the certificate was issued.
The quantum level Q_j from which the tower was started.
Number of lift steps in this ChainAuditTrail. Must equal chainLength of the certified LiftChain. Distinct from witnessCount (domain-locked to CompletenessAuditTrail).
True iff the linked GeodesicTrace is ordered by the AR_1 canonical rewriting rule (smallest lexicographic representative first).
True iff each constraint in the trace was selected by the DC_10 Jacobian oracle at the step where it was applied.
Runtime abstractions for maps between UOR objects: transforms, isometries, embeddings, and group actions. The foundation provides the vocabulary; Prism writes the sentences.
A map between UOR objects. The root abstraction: source, target, and optionally what structure (if any) is preserved. This is what cert:TransformCertificate certifies.
A transform that preserves metric structure with respect to a specified metric. In UOR, isometry is metric-relative: neg is a ring isometry, bnot is a Hamming isometry. A transform can be an isometry with respect to one metric but not the other. This is what cert:IsometryCertificate certifies.
An injective, structure-preserving transform across quantum levels. The canonical instance is the level embedding ι : R_n → R_{n'} (n < n'), which preserves addition, multiplication, and content addressing.
The mechanism by which a group applies transforms systematically to a set. Each group element induces a transform of the set. The dihedral action on type space is an action by isometries — every element of D_{2^n} produces an isometric transform of 𝒯_n.
A transform formed by composing two or more transforms sequentially. The categorical composition operation that turns transforms into a category.
The identity transform on a type: maps every element to itself. The categorical identity morphism.
A law governing how operations compose. Records whether the composition is associative, commutative, and what the result operation is. The critical composition law (neg ∘ bnot = succ) is the foundational instance.
A Transform mapping a surface symbol (any schema:Literal) to its ring datum (a schema:Datum) via the content-addressing bijection. Typed, derivation-witnessed, constraint-preserving map from surface to coordinate. Applies identically across NLP tokens, ARC-AGI grid cells, MIDI notes, pixels, sensor readings, and logical propositions.
A Transform mapping a resolved partition:Partition (address neighbourhood) to an ordered sequence of surface symbols. Output ordering determined by the active state:Frame — the same constraint frame that decomposed the input symbol sequence.
A certificate attesting that a specific grounding round-trip (P∘Π∘G) satisfied the shared-frame condition and landed in the type-equivalent neighbourhood of the source symbol. Witnesses the Surface Symmetry Theorem (op:surfaceSymmetry) for one specific symbol instance.
A topological delta: records changes in topological invariants (Betti numbers, Euler characteristic, nerve structure) before and after a morphism.
A datum whose ring value is the content address of a cert:TransformCertificate. Represents a certified computation as a first-class value within the ring.
A transform that applies a ComputationDatum to an input datum, producing an output datum. The output inherits the certificate of the ComputationDatum.
A ComputationDatum formed by fixing some but not all inputs of a multi-argument transform.
A ComputationDatum representing the composition f ∘ g of two ComputationDatums. Certified iff both components are certified and range(g) = domain(f).
Abstract supertype for one specific input/output pair witnessing a Transform.
One specific surface symbol mapped to one specific grounded address by some GroundingMap.
One specific input partition mapped to one specific surface symbol sequence by some ProjectionMap.
An ordered sequence of surface symbols. Elements are reified as SequenceElement individuals with explicit position indices.
One position in a SymbolSequence: a reified (value, index) pair.
The structure preserved by this transform (if any). E.g., a ring homomorphism preserves addition and multiplication.
The specific metric this isometry preserves. Points to observable:RingMetric or observable:HammingMetric. A transform that preserves both is an isometry of the full UOR geometry. A transform that preserves one but not the other has nontrivial curvature — observable:CurvatureObservable measures this gap.
The quantum level n of the source ring for an embedding.
The quantum level n' of the target ring for an embedding. Must satisfy n' > n (embeddings go to larger rings).
The set being acted upon by this group action.
Whether every transform induced by this action is an isometry. True for the dihedral action on 𝒯_n (Frame Theorem).
The computation trace that realized this transform at runtime. A Transform is an abstraction; a trace is the kernel's record of how it was executed via concrete operations.
A transform that this transform can be composed with. The target of this transform must match the source of the composed transform.
The transform that results from this composition.
A component transform of this composition.
The type on which this identity transform acts.
The number of component transforms in a composition.
Whether this composition law is associative.
Whether this composition law is commutative.
An operation that is a component of this composition law.
The operation that results from this composition law.
The identity preserved by this transform (reference to the op:Identity that the transform commutes with).
Certificate that this embedding's addressing diagram commutes: glyph ∘ ι ∘ addresses is well-defined and injective.
Euler characteristic before the morphism.
Euler characteristic after the morphism.
Constraint nerve (simplicial complex) before the morphism.
Constraint nerve (simplicial complex) after the morphism.
The surface symbol that is the source of this grounding witness.
The resolved ring address that is the target of this grounding witness.
The derivation witnessing the content-addressing computation that produced the grounded address from the surface symbol.
A typed attribute preserved by this grounding. Non-functional: one assertion per active constraint axis (vertical, horizontal, diagonal).
The active frame — shared with the grounding that produced the query. The shared-frame condition (Surface Symmetry Theorem) requires G and P to reference the same frame.
The resolved partition (address neighbourhood) that this projection witness projects back to surface symbols.
Ordering constraint determining the output symbol sequence. Domain-specific: syntactic position (NLP), row-major scan (ARC), temporal sequence (music).
Completeness criterion: does projecting the grounded source address recover a symbol in the same type class as the input? True iff the shared-frame condition holds.
The GroundingMap used in this certified round-trip.
The ProjectionMap used in this certified round-trip.
The surface symbol that entered the grounding boundary.
The ring address the symbol was grounded to.
The certificate this computation datum encodes.
The content address of the referenced certificate.
The base computation being partially applied.
The OWL class of inputs this transform accepts. Uses OWL2 punning so the value is a class IRI treated as an individual at this position.
The OWL class of outputs this transform produces. Uses OWL2 punning.
When outputClass is a sequence type, the OWL class of individual sequence elements. Uses OWL2 punning.
Zero or more witness pairs documenting specific input/output bindings of this transform.
Membership of a SymbolSequence. The sequence is reconstructed by sorting elements by elementIndex.
The surface symbol value of this sequence element.
The zero-based position of this element in the sequence.
The single SymbolSequence produced by this projection witness.
The critical composition law: neg ∘ bnot = succ. This is the operational form of the critical identity theorem. The composition of the two involutions (neg, bnot) yields the successor operation. Non-associative and non-commutative.
Grounds integer surface symbols to ring addresses.
Grounds UTF-8 host strings to ring addresses.
Grounds JSON host strings to ring addresses.
Projects partitions to integer symbol sequences.
Projects partitions to UTF-8 symbol sequences.
Projects partitions to JSON symbol sequences.
Parameterized address spaces, context management, binding lifecycle, and state transitions. The user-space overlay onto the kernel's read-only ring substrate.
A bounded set of populated UOR addresses. The parameter space for a resolution cycle. Contexts hold bindings that map addresses to datum values.
The association of a datum value with an address in a context. The write primitive: creating a binding populates an address.
The visibility boundary determining which bindings are in scope for a given resolution. A frame is a view into a context: it selects which bindings the resolver sees.
A state change: the transformation of one context into another through binding or unbinding. The sequence of transitions is the application's computation history.
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.
A bounded sequence of RelationQuery/response pairs sharing a common state:Context. Sessions are the unit of coherent multi-turn reasoning in Prism.
The mutable accumulator that appends state:Binding instances to a state:Context as each RelationQuery resolves. Tracks monotonic reduction of aggregate free site space.
Marks a context-reset event within a session stream. Records why the context was reset and provides a clean state:Context for subsequent queries.
A context that has reached full saturation: σ = 1, freeRank = 0, S = 0, T_ctx = 0 (SC_4). The ground state of the type system. All subsequent queries resolve in O(1) via SC_5.
Step-by-step evidence of the saturation process: records which bindings were applied, in what order, to reach full saturation.
An informational/monitoring record tracking the saturation progress of a specific domain within a context. Carries no formal authority — purely observational.
A typed controlled vocabulary for the three phases of context saturation: Open (σ = 0), PartialGrounding (0 < σ < 1), and FullGrounding (σ = 1).
A Context visible to more than one Session simultaneously. Holds a set of ContextLease instances that partition its site coordinates among active sessions. Lease disjointness (SR_9) prevents concurrent write conflicts.
A bounded, exclusive claim on a set of site coordinates within a SharedContext, held by exactly one Session. When the session closes or hits a SessionBoundary, the lease is released and its sites become available for re-leasing.
Records that a Session was formed by merging the binding sets of two or more predecessor sessions. Valid only if all predecessor binding sets pass the cross-session consistency check (SR_8). An invalid composition attempt produces a ContradictionBoundary on the target session.
The UOR address being bound in this binding.
The datum value bound to the address in this binding.
The type under which this binding's datum is resolved.
The time at which this binding was created.
The maximum number of bindings this context can hold.
The content-derived address of this context, uniquely identifying its current state in the UOR address space.
The Witt level of this context's address space.
The bindings currently in scope for this frame.
The type:Constraint determining which bindings from the context are visible in this frame. The resolver applies this constraint to filter the context's binding set, producing the frame's active bindings. An absent constraint means all bindings are visible.
Bindings added to the context in this transition.
Bindings removed from the context in this transition.
The computation trace recording the kernel operations that effected this state transition.
A snapshot of topological invariants at this transition point.
The shared context holding all bindings accumulated across the queries in this session.
The number of RelationQuery evaluations completed in this session.
The aggregate FreeRank deficit across all accumulated bindings: the total remaining free sites that have not yet been closed by resolution. Decreases monotonically as the session progresses.
A binding accumulated by this accumulator from a resolved RelationQuery.
A human-readable description of why this session boundary was triggered.
The typed reason category for this session boundary.
The state:Context that was active before this boundary reset.
The clean state:Context produced after this boundary reset, ready for subsequent queries.
The saturation degree σ ∈ \[0, 1\] of this context. Defined by SC_2: σ = (n − freeRank) / n.
The context temperature T_ctx ∈ \[0, ln 2\]. Defined by SC_1: T_ctx = freeRank × ln 2 / n. At σ = 1, T_ctx = 0.
Whether this context has reached full saturation (σ = 1). Equivalent to freeRank = 0, S = 0, T_ctx = 0 per SC_4.
The current saturation phase of this context: Open, PartialGrounding, or FullGrounding.
The GroundingCertificate attesting that this context has reached full saturation.
A binding that contributed to the saturation process, recorded in this GroundingWitness.
The step index at which a particular binding was applied during the saturation process.
The number of free (unbound) sites remaining in this context. At saturation, residualFreeCount = 0.
The GroundedContext that this DomainGroundingRecord monitors.
The domain within the context being tracked by this DomainGroundingRecord.
The number of free sites remaining in the specific domain tracked by this DomainGroundingRecord.
The subset of sites claimed by this lease. Must be disjoint from all other active leases on the same SharedContext (SR_9).
A currently active ContextLease on this SharedContext.
A predecessor session contributing bindings to this composition. Non-functional: one composition may merge two or more sessions.
Whether all predecessor binding sets passed the SR_8 consistency check. If false, the composition is invalid and must not be used as a session context.
The merged Context produced by a valid composition. Only present when compositionCompatible = true.
Whether the LiftChain tower consistency check (SR_8 parametric extension) was performed across all Q_0 through Q_k levels. Required for compositions involving sessions at Q_1 or higher.
The caller explicitly requested a context reset. All accumulated bindings are discarded.
The session resolver determined that no further queries can reduce the aggregate site deficit.
A new query produced a type contradiction with an accumulated binding. Context must reset before resolution can continue.
The context has σ = 0: no bindings accumulated, all sites are free. The initial phase of every session.
The context has 0 < σ < 1: some sites are pinned by accumulated bindings, but free sites remain. The accumulation phase.
The context has σ = 1: all sites are pinned, freeRank = 0. The ground state. All subsequent queries resolve in O(1) via SC_5.
The canonical ground-state witness: a GroundedContext at σ = 1, freeRank = 0, T_ctx = 0, S = 0 (SC_4). Demonstrates that full saturation is achievable and O(1) resolution (SC_5) is realized.
Sequential composition of ψ-maps into a parameterized reduction ψ = ψ_9 ∘ … ∘ ψ_1. Defines stages, phase gates, rollback, and epochs.
The composite endofunctor ψ = ψ_9 ∘ … ∘ ψ_1, parameterized by Ω = e^{iπ/6}.
Schedule Ω⁰, Ω¹, …, Ω⁵ assigning a phase angle to each stage of the reduction.
The angle at which the reduction terminates (default: π).
Validation at each stage boundary checking that the accumulated phase angle matches the expected Ω^k.
Recovery operation when a phase gate fails: z → z̄. Involutory: applying twice yields the original value.
A named stage of the reduction. The standard reduction has six stages (Initialization through Convergence).
State of reduction execution at a specific point, including the current stage, phase angle, and pinned mask.
Guard-effect pair governing stage transitions in the reduction. The guard must be satisfied before the effect is applied.
Temporal segment of reduction execution. Each epoch represents one complete pass through the reduction stages.
Transition between epochs. Carries metadata about the epoch boundary crossing.
A Boolean expression over the reduction state. The atomic guard unit.
A conjunction of PredicateExpressions that must hold for a transition to fire.
State changes applied when a transition fires. Contains PropertyBind steps.
A single site pinning: target site + value.
Advancement from one ReductionStep to the next.
A sliding window over recent epochs providing BaseContext.
An atomic group of state changes within the reduction.
Typed failure: DispatchMiss, GroundingFailure, ConvergenceStall, etc.
A pre-execution validation: feasibility, dispatch coverage, coherence.
Result of a preflight check: feasibility witness or infeasibility witness.
Lifecycle of a partitioned context lease: Pending → Active → Released/Expired/Suspended.
A context lease with lifecycle tracking.
Snapshot of lease state at a point in time.
Flow control when reduction produces faster than downstream can consume.
Transfer of a lease from one computation to another.
Predicate comparing a state field against a value.
Conjunction (AND) of multiple predicates.
Disjunction (OR) of multiple predicates.
Predicate testing membership of an element in a set.
Predicate testing whether grounding exceeds a threshold.
Predicate testing whether a site coverage target is met.
Predicate testing equality of two expressions.
Predicate testing that a field is non-null.
Predicate testing whether a query is a subtype of a given type.
The typed input graph submitted to the reduction pipeline. Packages a root Term, target quantum level, verification domains, and thermodynamic budget. Stage 0 accepts exactly one CompileUnit and initializes the reduction state vector from it.
The base phase parameter Ω for this reduction (e.g., e^{iπ/6}).
The cumulative phase angle at which the reduction converges.
The ordered list of ψ-maps that compose this reduction.
String representation of the rotation schedule Ω⁰, Ω¹, …, Ω⁵.
The base angle π/6 from which the schedule is derived.
The target convergence angle (default: π).
The reduction stage at which this gate is applied.
The expected phase angle Ω^k at this gate.
Whether the phase gate check passed or failed.
The reduction stage to which execution rolls back on gate failure.
Zero-based index of this stage in the reduction.
Human-readable name of this reduction stage.
The expected phase angle Ω^k at this stage.
A typed predicate evaluated on the current ReductionState. Must be satisfied to enter this stage.
A typed predicate that must be satisfied before the reduction advances past this stage.
The effect applied by this stage upon successful exit.
The reduction stage at which execution is currently positioned.
The accumulated phase angle at the current point.
Bit mask of sites that are pinned (resolved) at this point.
The number of free (unresolved) sites at this point.
A typed GuardedTransition from predicate/ governing the stage transition.
The effect applied when this transition fires.
Whether this transition advances to the next stage.
Zero-based index of this epoch in the reduction execution.
Metadata or summary datum for this epoch.
The type of epoch boundary crossing (e.g., normal, forced, timeout).
The comparison operator (e.g., '=', '<', '>=').
The value against which the field is compared.
The predicate expressions that compose this guard.
The property bind steps applied by this effect.
The target site identifier for this binding.
The number of recent epochs in this service window.
The starting epoch offset of this service window.
The execution policy for this transaction (e.g., AllOrNothing, BestEffort).
The outcome of this transaction (e.g., committed, rolled back).
The kind of pipeline failure (e.g., DispatchMiss, ConvergenceStall).
The kind of preflight check (e.g., feasibility, dispatch coverage).
The result of the preflight check (e.g., pass, fail).
The kind of feasibility result (e.g., Feasible, Infeasible).
The witness justifying the feasibility or infeasibility result.
The lifecycle phase of a lease (e.g., Pending, Active, Released).
Unique identifier for this managed lease.
The current lifecycle state of this managed lease.
The epoch index at which this checkpoint was taken.
The reduction state captured at this checkpoint.
The current back-pressure level (e.g., Low, Medium, High).
The threshold at which back-pressure activates.
The number of queries in this deferred set.
The epoch in which these queries were deferred.
The site budget transferred between leases.
Whether the sublease transfer has been completed.
The state field tested by this comparison predicate.
The value against which the comparison is made.
The set against which membership is tested.
The element being tested for set membership.
The grounding threshold above which the predicate holds.
The right-hand side of an equality test.
The query type reference for subtype testing.
The site state descriptor within a reduction state.
The scope of sites affected by this transaction.
Current status of this transaction (e.g., pending, committed).
Reference to the base context provided by this service window.
The remaining site budget at this checkpoint.
The epoch at which this managed lease expires.
The total site budget allocated to this managed lease.
The source stage emitting back-pressure.
The target stage receiving back-pressure.
The reduction stage at which the pipeline failure occurred.
The final grounding level achieved on pipeline success.
Whether grounding was preserved across the epoch boundary.
The root term expression of a CompileUnit — the top-level syntactic node from which all sub-expressions descend.
The quantum level at which this CompileUnit operates.
The Landauer-bounded energy budget for this CompileUnit's resolution, measured in k_B T ln 2 units.
The verification domain(s) targeted by this CompileUnit.
Content-addressable identifier computed as the u:Element of the root term’s transitive closure. Computed by stage_initialization, not declared by the submitter. Excludes budget, domains, and quantum level to enable memoization.
Zero-based execution order for preflight checks. Lower indices execute first. BudgetSolvencyCheck (order 0) must precede all others.
Stage 0: initialize state vector to identity.
Stage 2: produce valid ring address (G grounds).
Stage 3: resolve constraints (Π terminates).
Stage 4: accumulate without contradiction (α consistent).
Stage 5: extract coherent output (P projects).
Terminal stage: reduction has reached the convergence angle π.
Phase gate at stage 0 boundary: checks Ω⁰ = 1.
Phase gate at stage 1 boundary: checks Ω¹.
Phase gate at stage 2 boundary: checks Ω².
Phase gate at stage 3 boundary: checks Ω³.
Phase gate at stage 4 boundary: checks Ω⁴.
Phase gate at stage 5 boundary: checks Ω⁵.
The canonical Euler reduction instance with Ω = e^{iπ/6} and 6 stages.
The canonical phase rotation schedule for the 6-stage reduction.
The canonical complex conjugate rollback operation: z → z̄.
Failure: no resolver matched the dispatch query.
Failure: grounding to a valid ring address failed.
Failure: reduction stalled before reaching convergence angle.
Failure: accumulation detected a logical contradiction.
Failure: coherence constraint violated during extraction.
Successful termination: all sites saturated.
Preflight: checks that the reduction can reach convergence.
Preflight: checks that every dispatch query has a resolver.
Preflight: checks package-level coherence constraints.
The default service window: 3 epochs, zero offset.
Advancement from Initialization to Declare.
An all-or-nothing atomic reduction transaction.
A trivially satisfied guard with no predicates.
A predicate that always evaluates to true.
A no-op property binding that changes nothing.
Lease is active and resources are allocated.
Preflight result: reduction is feasible.
Preflight result: reduction is infeasible.
Preflight: verifies thermodynamicBudget ≥ bitsWidth(unitWittLevel) × ln 2. Rejects the CompileUnit if the budget is absent or insufficient. Must execute before all other preflights (preflightOrder 0). Cost is O(1) per CS_4.
Default back-pressure signal with medium threshold.
Hopf convergence tower: four levels R, C, H, O corresponding to the four normed division algebras of dimensions 1, 2, 4, 8. Each level carries a Hopf fibration fiber and Betti signature.
A level in the convergence tower. Four instances: R (dim 1), C (dim 2), H (dim 4), O (dim 8).
The fiber of the Hopf fibration at a convergence level. Four instances: S⁰, S¹, S³, S⁷.
The unresolved structure at a convergence level. The β_{2^k−1} = 1 Betti number that persists.
The subspace U(1) ⊂ SU(2) selected when pairwise interaction converges.
The subspace H ⊂ O selected when triple interaction converges.
The dimension of the division algebra at this level (1, 2, 4, or 8).
The Betti number signature at this convergence level.
The Hopf fiber associated with this convergence level.
The characteristic identity at this convergence level (existence, feedback, choice, self-reference).
Human-readable name of this convergence level.
The fiber sphere designation (e.g. S⁰, S¹).
The persistent Betti number at this residual.
The dimension at which the residual persists.
The commutative subspace selected by pairwise convergence.
The associative subalgebra selected by triple convergence.
Reference to the commutator pair for this convergence.
Reference to the associator triple for this convergence.
Level 0: R (reals), dimension 1, existence.
Level 1: C (complex), dimension 2, feedback.
Level 2: H (quaternions), dimension 4, choice.
Level 3: O (octonions), dimension 8, self-reference.
Hopf fiber S⁰: dimension 0, total space S¹, base pt.
Hopf fiber S¹: dimension 1, total space S³, base S².
Hopf fiber S³: dimension 3, total space S⁷, base S⁴.
Hopf fiber S⁷: dimension 7, total space S¹⁵, base S⁸.
The four normed division algebras R, C, H, O and the Cayley-Dickson construction.
An algebra over R that is a division ring with multiplicative norm. Exactly four exist (Hurwitz theorem): R, C, H, O.
The doubling construction that builds each division algebra from the previous: R → C → H → O.
The explicit product rules for a division algebra’s basis elements.
The commutator [a,b] = ab − ba. Zero for R and C; non-zero for H and O.
The associator [a,b,c] = (ab)c − a(bc). Zero for R, C, H; non-zero for O.
The dimension of this division algebra (1, 2, 4, or 8).
Whether multiplication in this algebra is commutative.
Whether multiplication in this algebra is associative.
The basis elements of this division algebra.
The multiplication table for this algebra.
The source algebra of the Cayley-Dickson doubling.
The target algebra of the Cayley-Dickson doubling.
The new basis element adjoined by this doubling step.
The conjugation and multiplication rule for the adjoined element.
The real numbers R: dimension 1, commutative, associative.
The complex numbers C: dimension 2, commutative, associative.
The quaternions H: dimension 4, non-commutative, associative.
The octonions O: dimension 8, non-commutative, non-associative.
Cayley-Dickson doubling R → C: adjoin i with i² = −1.
Cayley-Dickson doubling C → H: adjoin j with j² = −1, ij = k, ji = −k.
Cayley-Dickson doubling H → O: adjoin l, non-associative Fano plane products.
Multi-entity interaction: commutator states, associator triples, negotiation convergence.
Two entities sharing sites through composed operations. Properties: entityA, entityB, sharedSiteMask, commutatorNorm.
The norm ‖[δ_A, ι_B]‖ on shared sites. Zero iff operators commute on the shared domain.
The norm of the three-way associator on shared sites.
Three entities whose interaction exhibits non-associativity due to read-write interleaving.
A site shared by all three entities in an AssociatorTriple.
Sequence of CommutatorStates across interaction steps.
Sequence of AssociatorStates across interaction steps.
Simplicial complex of N-entity coupling.
IC(A,B) = κ(session(A,B)). Combined interaction-composition operator.
First entity in the interaction context.
Second entity in the interaction context.
Bitmask identifying which sites are shared between the two entities.
The norm of the commutator on shared sites. Zero iff the operators commute.
First component datum in the associator triple.
Second component datum in the associator triple.
Third component datum in the associator triple.
Value under left-associative grouping (AB)C.
Value under right-associative grouping A(BC).
Whether this site is pinned by a lease constraint.
Identifier of the entity pair that pins this site.
Number of steps in the negotiation trace.
Whether the trace converges to zero commutator or zero associator.
Whether the mutual model trace converges.
Maximum dimension of the interaction nerve simplicial complex.
Betti number sequence of the interaction nerve.
Depth of the interaction composition reification.
The number of steps in a negotiation trace.
The rate at which the negotiation trace converges.
The terminal value of the negotiation trace.
Reference to the observable describing the associativity profile.
The maximum norm of the associator for this triple.
Sequential composition of computations via monoidal product A ⊗ B.
A ⊗ B: the sequential composition of two computations. Output of A feeds input of B.
The identity computation I: passes input through unchanged. I ⊗ A ≅ A ≅ A ⊗ I.
The witness that (A⊗B)⊗C ≅ A⊗(B⊗C). The associativity isomorphism.
The left operand in the monoidal product A ⊗ B.
The right operand in the monoidal product A ⊗ B.
The result datum of the composed computation A ⊗ B.
σ(A⊗B) relationship: saturation of the sequential composition.
Certificate witnessing I ⊗ A ≅ A ≅ A ⊗ I.
Certificate witnessing the associativity isomorphism (A⊗B)⊗C ≅ A⊗(B⊗C).
Structural type nesting via operad composition. Governs how types compose: Table(Tuple(Sequence(Symbol(...)))).
The composition structure on the eight structural types. Governs how types nest.
A specific nesting: outer type F applied to inner type G.
The structural operad defining this composition.
Typed endomorphisms on state:Context classified by site target. Formalizes what reduction guard-effect pairs do to the site budget.
A typed endomorphism on state:Context. Maps one site-budget configuration to another. The atomic unit of state mutation in the kernel.
An effect that has a well-defined inverse. PinningEffect and PhaseEffect are reversible; ExternalEffect and CompositeEffect are not in general.
Pins a single free site to a definite value. Decrements freeRank by exactly 1. The effect produced by constraint resolution.
Releases a pinned site back to free state. Increments freeRank by exactly 1. The effect produced by session boundary reset.
Rotates the reduction phase angle by Ω^k. Does not alter the site budget. The effect produced by reduction step transitions.
An ordered sequence of effects applied atomically. The composition E₁ ; E₂ applies E₁ then E₂.
An opaque effect declared by a Prism implementation. The kernel treats it as a site-budget transformation satisfying the declared commutation contract. Must carry an effect:externalEffectShape linking to a conformance:EffectShape.
The set of site coordinates that an effect reads or writes. Determines commutation.
A certificate that two EffectTargets have empty intersection, enabling commutative reordering.
The site coordinates this effect touches.
The individual site coordinates in this target set.
The first effect in the composite sequence.
Subsequent effects in the composite sequence (ordered by effect:compositeIndex).
The left target in the disjointness claim.
The right target in the disjointness claim.
The conformance shape that this external effect satisfies.
Change in freeRank: −1 for PinningEffect, +1 for UnbindingEffect, 0 for PhaseEffect.
The phase rotation applied, expressed as Ω^k.
Position within a CompositeEffect sequence.
Computed: true iff effectTargets are disjoint with the compared effect. Derived from DisjointnessWitness existence.
Number of site coordinates in this target set.
Boolean-valued functions on kernel objects. Formalizes resolver dispatch, reduction guard evaluation, and conditional resolution paths.
A total, pure, boolean-valued function on a kernel object. Evaluation terminates for all inputs and produces no side effects.
A predicate over type:TypeDefinition. Used for resolver dispatch.
A predicate over state:Context or reduction:ReductionState. Used for reduction step guards.
A predicate over partition:SiteIndex. Used for site-level selection in geodesic resolution.
A pair (Predicate, Target) where Target is a resolver:Resolver class. The kernel evaluates the predicate; if true, the target resolver is selected.
An ordered set of DispatchRules for a single dispatch point. Must satisfy exhaustiveness and mutual exclusion.
A triple (StatePredicate, effect:Effect, reduction:ReductionStep). The guard is a StatePredicate; if true, the effect is applied and the reduction advances to the target step.
A single case in a pattern match: a Predicate and a result Term. The match evaluates predicates in order and returns the result of the first matching arm.
A term formed by evaluating a sequence of MatchArms. Extends the term language with deterministic conditional evaluation.
The OWL class of objects this predicate accepts as input.
The predicate that triggers this dispatch rule.
The resolver selected when the predicate is satisfied.
The guard predicate for this transition.
The effect applied when the guard is satisfied.
The ordered arms of this match expression.
A termination witness for user-declared predicates. Kernel predicates are total by construction; user-declared predicates must carry a descent measure certifying termination.
Position in the dispatch table (evaluation order).
True iff the disjunction of all dispatch predicates is a tautology over the input class.
True iff no two dispatch predicates can be simultaneously true for any input.
Position in the match expression (evaluation order).
True on every Datum. Match-arm default catch-all.
False on every Datum. Disabled-arm marker.
True iff the Datum is the additive identity of its ring.
True iff the Datum is the multiplicative identity.
True iff op(op(x)) = x for the bound op.
True iff the named site coordinate is currently pinned.
True iff the named site coordinate is currently free.
True iff the resolver has entered a ContradictionBoundary.
True iff the reduction fixpoint has been reached.
Independent computations over provably disjoint site budgets. Formalizes when execution order is irrelevant.
A ∥ B: two computations with provably disjoint site targets. Execution order does not affect the result.
A kernel-produced certificate attesting that the site targets of two computations are disjoint.
A point where two parallel computations must agree on shared state before proceeding. Only applicable when parallelism is partial.
A computation trace recording interleaved steps from two parallel computations. Valid iff every interleaving produces the same final context.
A partition of the total site budget into disjoint subsets, one per parallel component. The sum of subset cardinalities equals the total site budget.
The left parallel component (itself a sequential computation).
The certificate proving site disjointness.
The site target of the left computation.
The site target of the right computation.
The shared sites requiring synchronization.
The disjoint subsets composing the full site budget.
True iff site targets have zero overlap (no SynchronizationPoints required).
Declares whether this parallel product commutes with disjoint effects per FX_4.
Coinductive sequences of reduction epochs. Each epoch terminates independently; the stream is the unbounded composition of terminating epochs.
An unbounded sequence of reduction epochs where each epoch terminates and produces a well-typed output. The coinductive dual of a finite computation.
A single bounded iteration within a productive stream. Each epoch is a complete reduction execution from Initialization through Convergence.
The transition point between consecutive epochs. Carries the continuation context and the epoch output.
A finite prefix of a productive stream: the first k epochs and their outputs. Every finite prefix is computable in finite time.
A transform between productive streams: maps each epoch of the source to an epoch of the target while preserving the productive property.
The coinductive constructor: given an initial context and a step function (a morphism:ComputationDatum), produces a ProductiveStream. The step function must be certified to always reach reduction convergence.
The output datum produced by this epoch.
The context carried across the boundary.
The epochs in this prefix (ordered by stream:epochIndex).
The certified step function producing each epoch.
Zero-based index of this epoch in the stream.
Always true by construction: every epoch terminates. Invariant, not computed.
Partial computations, typed failure propagation, and recovery. Formalizes how computations that cannot reach convergence are represented, composed, and recovered from within the ring substrate.
The outcome of a computation that may fail: either a Success carrying a datum, or a Failure carrying a typed reason. The coproduct of the success and failure cases.
A computation that reached convergence and produced a valid datum. Carries the output datum and the computation certificate.
A computation that could not reach convergence. Carries a typed FailureReason and the reduction state at the point of failure.
A typed classification of why a computation failed.
A reduction step guard evaluated to false and no alternative transition exists.
Two constraints in the type’s constraint set are jointly unsatisfiable.
The linear budget was exhausted before resolution completed.
A WittLift encountered a non-trivial obstruction that could not be resolved.
A computation that produces a ComputationResult rather than a guaranteed datum. The general case of all computations.
A computation where the FailureReason type is empty — failure is structurally impossible.
A strategy for converting a Failure into a Success by modifying the computation path.
The rule for how failures compose under monoidal and parallel products.
The output datum of a successful computation.
The certificate attesting the computation’s correctness.
The reduction state at the point of failure.
The reduction step where failure occurred.
Available recovery strategies for this failure.
The effect applied to recover from failure.
The reduction step to retry after recovery.
Which failure reasons propagate through this composition.
True iff the computation is a TotalComputation (no possible failure path).
The reduction step index at which failure occurred.
Linear discipline on site consumption. Formalizes that each site in a complete resolution path is targeted by exactly one effect.
A site index annotated with a linearity constraint: must be pinned exactly once in any complete resolution path.
A PinningEffect that consumes its target LinearSite. After application, the site is no longer available for pinning by any subsequent effect.
A computation trace where every site in the budget is targeted by exactly one LinearEffect.
The multiset of LinearSites available at a given point in resolution. Starts as the full site budget; each LinearEffect removes exactly one element.
A binding between a state:ContextLease and a subset of LinearSites. Formalizes what resources a lease claims.
A site that may be pinned at most once (but need not be pinned). Relaxation of LinearSite for incomplete resolution paths.
The single site consumed by this effect.
The context associated with this budget state.
The ContextLease individual that owns this allocation.
Links a state:ContextLease to its LinearSite allocation.
Number of unconsumed sites. Equals freeRank on the associated context.
Self-referential computations with well-founded descent measures guaranteeing termination.
A self-referential computation parameterized by a descent measure. Each recursive step strictly decreases the measure; the computation terminates when the base case predicate is satisfied.
A well-founded function from computation state to xsd:nonNegativeInteger. Strictly decreases on every recursive step.
The match arm selected when the descent measure reaches zero or the base predicate is satisfied. Produces a direct result without further recursion.
The match arm selected when the descent measure is positive. Applies a decomposition step, decreases the measure, and invokes the recursion.
A single step in a bounded recursion: the decomposition applied before the recursive invocation. Must strictly decrease the DescentMeasure.
A computation trace recording the sequence of recursive steps, measure values, and the base case result. The trace length is bounded by the initial measure value.
A bounded recursion where the descent measure is the structural size of the input type (site count, constraint count, or operad nesting depth).
The descent measure guaranteeing termination.
The transform applied to decompose the input before recursion.
The predicate that identifies the base case.
The computation applied at each recursive step (may reference itself via its content address).
The measure value at the start of recursion. Bounds the maximum recursion depth.
The current value of the descent measure.
Spatial locality of content-addressed ring elements. Defines computable working sets for resolver stages, independent of physical memory layout.
A contiguous range of u:Element values accessible during a single reduction step. Defines the resolver’s working set.
The boundary of an AddressRegion: a pair (lowerAddress, upperAddress) in the content-address ordering.
A metric on u:Element values determining which addresses are near each other for resolution purposes.
The set of AddressRegions needed by a resolver at a specific reduction step for a specific type. Computable from the type’s constraint nerve.
An assignment of AddressRegions to reduction steps for a given computation. Enables Prism to pre-compute memory layout.
The metric defining contiguity for this region.
The address regions composing this working set.
The reduction step this working set applies to.
The working sets assigned to each stage.
Total addresses across all regions in the working set.
Typed interface between kernel computation and the external world. Formalizes how data enters and exits the ring substrate.
A typed interface point between the kernel and the external world. Every data flow into or out of the ring crosses exactly one IOBoundary.
A typed source of external data entering the ring. Carries an expected TypeDefinition describing the shape of incoming data.
A typed destination for data leaving the ring. Carries an expected TypeDefinition describing the shape of outgoing data.
An effect that crosses the kernel/external boundary. Specializes effect:ExternalEffect with explicit source or sink binding.
A BoundaryEffect that reads from a Source and produces a datum in the ring.
A BoundaryEffect that writes a ring datum to a Sink.
A specification of the data shape, ordering, and framing constraints for data crossing a boundary.
A Session that includes BoundaryEffects. Extends the session model to track which boundaries were crossed.
The expected type of data arriving from this source.
The expected type of data departing through this sink.
The grounding map that transforms incoming surface data to ring datums.
The projection map that transforms ring datums to outgoing surface data.
The type specification for boundary data.
Sequencing constraints on boundary data.
The boundaries crossed during this session.
True iff applying the boundary effect twice produces the same result as applying it once.
Total number of boundary crossings in this session.
SHACL-equivalent constraint shapes defining what a Prism implementation must provide at each extension point. Machine-verifiable contracts.
A constraint shape that a Prism-declared extension must satisfy. Analogous to sh:NodeShape in SHACL.
A single required property within a shape: the property URI, its expected range, minimum and maximum cardinality.
Shape for declaring a new WittLevel beyond Q3.
Shape for declaring a ProductiveStream (targets stream:Unfold, the coinductive constructor).
Shape for declaring a new DispatchRule in a DispatchTable.
Shape for declaring a Lease with LinearSite allocation.
Shape for declaring a GroundingMap from surface data to the ring.
The result of validating an extension against a shape: conforms (boolean), and violation details if non-conformant.
Shape for user-declared predicates. Requires a bounded evaluator (termination witness) and input type declaration.
Opaque ring element witness. Cannot be constructed outside the foundation crate — only produced by reduction evaluation or the two-phase minting boundary.
Boundary crossing intermediate for a single grounded coordinate value. Not a WitnessDatum — must be validated and minted by the foundation.
Boundary crossing intermediate for a fixed-size array of GroundedCoordinate values. Stack-resident, no heap allocation.
Sealed marker trait class. Implemented only for GroundedCoordinate and GroundedTuple. Prevents downstream crates from substituting arbitrary types.
Generic validation-proof wrapper. Proves that the inner value was produced by the conformance checker, not fabricated by Prism code.
Opaque derivation trace that can only be extended by the rewrite engine. Records rewrite step count and root term content address.
Opaque site budget that can only be decremented by PinningEffect and incremented by UnbindingEffect — never by direct mutation.
Structured violation diagnostic carrying the shape IRI, constraint IRI, property IRI, expected range, cardinality bounds, and violation kind.
The kind of shape violation: Missing, TypeMismatch, CardinalityViolation, ValueCheck, or LevelMismatch.
Builder for CompileUnit admission. Collects rootTerm, quantumLevelCeiling, thermodynamicBudget, and targetDomains. Validates against CompileUnitShape.
Builder for EffectShape. Collects effect name, target sites, budget delta, and commutation flag.
Builder for GroundingShape. Collects source type, ring mapping, and invertibility contract.
Builder for DispatchShape. Collects predicate, target resolver, and dispatch priority.
Builder for LeaseShape. Collects linear site and lease scope.
Builder for StreamShape. Collects unfold seed, step term, and productivity witness.
Builder for PredicateShape. Collects input type, evaluator term, and termination witness.
Builder for ParallelShape. Collects site partition and disjointness witness.
Builder for WittLevelShape. Collects declared bit width, cycle size, and predecessor level.
Boundary session state tracker. Records crossing count and idempotency flag for the two-phase minting boundary.
The OWL class that instances of this shape must belong to.
The expected range of the required property.
Minimum cardinality of the required property.
True iff the target satisfies all constraints of the shape.
The quantum level at which this witness datum was minted.
The raw byte representation of this witness datum.
The quantum level tag of this grounded coordinate.
The validated inner value wrapped by this proof.
IRI of the conformance:Shape that was validated against.
IRI of the specific PropertyConstraint that failed.
IRI of the property that was missing or invalid.
The expected range class IRI for the violated property.
The minimum cardinality from the violated constraint.
The maximum cardinality from the violated constraint (0 = unbounded).
The root term expression for the CompileUnit.
The widest quantum level the computation may reference.
Landauer-bounded energy budget in kBT ln 2 units.
Verification domains targeted by the CompileUnit.
Site coordinates this effect reads or writes.
The site budget delta (positive = increment, negative = decrement).
Whether this effect commutes with effects on disjoint sites.
The source type of incoming external data.
Description of the mapping from surface data to ring.
Whether the grounding map is invertible.
The predicate expression guarding this dispatch rule.
The resolver to dispatch to when the predicate holds.
Priority ordering for this dispatch rule (lower = first).
The site coordinate allocated linearly by this lease.
The scope within which this lease is valid.
The seed term for the stream unfold constructor.
The step function term for the stream unfold.
Evidence that the stream is productive (always produces a next element).
The input type for the declared predicate.
The evaluator term for the declared predicate.
Evidence that the predicate evaluator terminates on all inputs.
The site partition for the parallel composition.
Evidence that the site partition components are pairwise disjoint.
The declared bit width for this quantum level.
The declared number of ring states at this level.
The predecessor quantum level in the chain.
Total boundary crossings in this minting session.
Whether applying this session's boundary effect twice equals applying it once.
Shape validating that a CompileUnit carries all required properties before reduction admission. The unitAddress property is NOT required — it is computed by stage_initialization after shape validation passes.
Exactly one root term is required. Range is schema:Term.
Exactly one quantum level is required. Range is schema:WittLevel.
Exactly one thermodynamic budget is required. Shape validates presence and type; the BudgetSolvencyCheck preflight validates the value against the Landauer bound.
At least one target verification domain is required. maxCount 0 means unbounded.
Required property was not set on the builder.
Property was set but its value is not an instance of the constraintRange.
Cardinality violated: too few or too many values provided.
Value-dependent check failed (Tier 2). For example, thermodynamic budget insufficient for Landauer bound.
A term's quantum level annotation exceeds the CompileUnit ceiling, or binary operation operands are at different levels without an intervening lift or project.