UOR Operations

IRI
https://uor.foundation/op/
Prefix
op:
Space
kernel
Comment
Ring operations, involutions, algebraic identities, and the dihedral symmetry group D_{2^n} generated by neg and bnot.

View documentation reference

This is a kernel-space namespace in the Define stage of the PRISM pipeline. It provides the immutable algebraic substrate — ring structure, schema vocabulary, and operation algebra.

Learn more: Pipeline Overview · Witt Levels

Class hierarchy
Class hierarchy for UOR Operations namespace Operation UnaryOp BinaryOp Involution Identity Group DihedralGroup VerificationDo GeometricChara WittLevelBindi QuantumThermod ValidityScopeK ComposedOperat DispatchOperat InferenceOpera AccumulationOp LeasePartition SessionComposi GroupPresentat

Imports

Classes

NameSubclass OfDisjoint WithComment
OperationThingAn operation on the ring Z/(2^n)Z. The root class for all UOR kernel operations.
UnaryOpOperationA unary operation on the ring: takes one datum and produces one datum.
BinaryOpOperationA binary operation on the ring: takes two datums and produces one datum.
InvolutionUnaryOpA 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).
IdentityThingAn 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.
GroupThingA group: a set with an associative binary operation, an identity element, and inverses for every element.
DihedralGroupGroupThe 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.
VerificationDomainThingA 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/.
GeometricCharacterThingThe 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}.
WittLevelBindingThingA 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.
QuantumThermodynamicDomainThingA verification domain at the intersection of quantum superposition and classical thermodynamics. Identities in this domain require both SuperpositionDomain and Thermodynamic reasoning simultaneously.
ValidityScopeKindThingRoot class for validity scope individuals. Instances are the four named scope kinds: Universal, ParametricLower, ParametricRange, and LevelSpecific.
ComposedOperationOperation, CompositionAn operation formed by composing ring operations, witnessed by op:composedOf and morphism/CompositionLaw.
DispatchOperationComposedOperationδ: Query × ResolverRegistry → Resolver. Non-commutative, non-associative, arity 2.
InferenceOperationComposedOperationι = P ∘ Π ∘ G (the φ-pipeline composed). Non-commutative, non-associative, arity 2.
AccumulationOperationComposedOperationα: Binding × Context → Context. Non-commutative, associative at convergence (SR_10), arity 2.
LeasePartitionOperationComposedOperationλ: SharedContext × ℕ → ContextLease^k. Non-commutative, non-associative, arity 2.
SessionCompositionOperationComposedOperationκ: Session × Session → Session. Commutative (disjoint leases), associative (SR_8), arity 2.
GroupPresentationThingA structured group presentation: generators and relations as typed data rather than prose strings.

Properties

NameKindFunctionalDomainRangeComment
arityDatatypetrueOperationnonNegativeIntegerThe number of arguments this operation takes. 1 for unary operations, 2 for binary operations.
hasGeometricCharacterObjecttrueOperationGeometricCharacterThe geometric role of this operation in the UOR ring and hypercube geometry. Functional: each operation has exactly one geometric character.
commutativeDatatypetrueBinaryOpbooleanWhether this binary operation satisfies op(x,y) = op(y,x) for all x, y in R_n.
associativeDatatypetrueBinaryOpbooleanWhether this binary operation satisfies op(op(x,y),z) = op(x,op(y,z)) for all x, y, z in R_n.
identityDatatypetrueBinaryOpintegerThe identity element of this binary operation: the value e such that op(x, e) = op(e, x) = x for all x in R_n.
inverseObjecttrueOperationOperationThe inverse operation: the operation inv_op such that op(x, inv_op(x)) = e for all x, where e is the identity.
composedOfObjecttrueOperationListOrdered 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.
lhsObjecttrueIdentityTermExpressionThe left-hand side of an algebraic identity as a typed AST node (schema:TermExpression).
rhsObjecttrueIdentityTermExpressionThe right-hand side of an algebraic identity as a typed AST node (schema:TermExpression).
forAllObjecttrueIdentityForAllDeclarationThe quantifier scope: a typed declaration of the variable(s) over which this identity holds.
generatedByObjectfalseGroupOperationAn operation that generates this group. The dihedral group D_{2^n} is generated by op:neg and op:bnot.
orderDatatypetrueGrouppositiveIntegerThe number of elements in the group. For D_{2^n}, the order is 2^(n+1).
presentationAnnotationtrueGroupstringThe group presentation (generators and relations). Example: ⟨r, s | r^{2^n} = s² = e, srs = r⁻¹⟩
verificationDomainObjectfalseIdentityVerificationDomainThe 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.
verifiedAtLevelObjectfalseIdentityWittLevelBindingLinks an Identity individual to a WittLevelBinding attesting verification at a specific quantum level. Non-functional: one binding per (Identity, WittLevel) pair.
bindingLevelObjecttrueWittLevelBindingWittLevelThe quantum level at which this WittLevelBinding was verified.
universallyValidDatatypetrueIdentitybooleanTrue 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.
enumVariantObjecttrueVerificationDomainVerificationDomainThe canonical Rust enum variant name corresponding to this VerificationDomain individual. Provides formal alignment between the OWL individual and the generated Rust enum.
validityKindObjecttrueIdentityValidityScopeKindThe structured validity scope of this identity, replacing the binary universallyValid flag. Required on all new Identity individuals.
validKMinDatatypetrueIdentitynonNegativeIntegerMinimum quantum level index k for ParametricLower and ParametricRange scopes.
validKMaxDatatypetrueIdentitynonNegativeIntegerMaximum quantum level index k (inclusive) for ParametricRange scope.
composedOfOpsObjectfalseComposedOperationOperationReferences a constituent operation of a ComposedOperation. Non-functional: a composed operation may reference multiple constituent operations.
operatorSignatureAnnotationtrueComposedOperationstringHuman-readable type signature describing the domain and codomain of a composed operation (e.g., 'Query × Registry → Resolver').
dispatchSourceObjecttrueDispatchOperationOperationThe source selector for a dispatch operation.
dispatchTargetObjecttrueDispatchOperationOperationThe target resolver for a dispatch operation.
inferenceSourceObjecttrueInferenceOperationOperationThe source data for an inference operation.
inferenceTargetObjecttrueInferenceOperationOperationThe target type for an inference operation.
inferencePipelineObjecttrueInferenceOperationOperationThe pipeline through which inference is performed.
accumulationBaseObjecttrueAccumulationOperationTermExpressionThe base value for an accumulation operation.
accumulationBindingObjecttrueAccumulationOperationTermExpressionThe binding accumulator for an accumulation operation.
leaseSourceObjecttrueLeasePartitionOperationOperationThe source context for a lease partition operation.
leaseFactorObjecttrueLeasePartitionOperationOperationThe partition factor for a lease partition operation.
leasePartitionCountDatatypetrueLeasePartitionOperationnonNegativeIntegerThe number of partitions in a lease partition operation.
compositionLeftSessionObjecttrueSessionCompositionOperationOperationThe left session in a session composition operation.
compositionRightSessionObjecttrueSessionCompositionOperationOperationThe right session in a session composition operation.
operatorDomainTypeObjecttrueComposedOperationTypeDefinitionThe domain type of a composed operation.
operatorRangeTypeObjecttrueComposedOperationTypeDefinitionThe range type of a composed operation.
operatorComplexityDatatypetrueComposedOperationstringThe computational complexity class of a composed operation.
operatorIdempotentDatatypetrueComposedOperationbooleanWhether this composed operation is idempotent.
composedOperatorCountDatatypetrueComposedOperationnonNegativeIntegerThe number of constituent operations in a composed operation.
isInvolutoryDatatypetrueComposedOperationbooleanWhether applying this operation twice yields the identity.
convergenceGuaranteeObjecttrueComposedOperationTermExpressionDescription of the convergence guarantee for this operation.

Named Individuals

NameTypeComment
EnumerativeVerificationDomainEstablished by exhaustive traversal of R_n. Valid for all identities where the ring is finite.
  • enumVariant: Enumerative
AlgebraicVerificationDomainEstablished by equational reasoning from ring or group axioms. Covers derivations via associativity, commutativity, inverse laws, and group presentations.
  • enumVariant: Algebraic
GeometricVerificationDomainEstablished by isometry, symmetry, or GeometricCharacter arguments. Covers dihedral actions, fixed-point analysis, automorphism groups, and affine embeddings.
  • enumVariant: Geometric
AnalyticalVerificationDomainEstablished via discrete differential calculus or metric analysis. Covers ring/Hamming derivatives (DC_), metric divergence (AM_), and adiabatic scheduling (AR_).
  • enumVariant: Analytical
ThermodynamicVerificationDomainEstablished via entropy, Landauer bounds, or Boltzmann distributions. Covers site entropy (TH_), reversible computation (RC_), and phase transitions.
  • enumVariant: Thermodynamic
TopologicalVerificationDomainEstablished via simplicial homology, cohomology, or constraint nerve analysis. Covers homological algebra (HA_) and ψ-pipeline identities.
  • enumVariant: Topological
PipelineVerificationDomainEstablished by the inter-algebra map structure of the resolution pipeline. Covers φ-maps (phi_1–phi_6) and ψ-maps (psi_1–psi_6).
  • enumVariant: Pipeline
IndexTheoreticVerificationDomainEstablished 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).
  • enumVariant: IndexTheoretic
SuperpositionDomainVerificationDomainEstablished by superposition analysis of site states. Covers identities involving superposed (non-classical) site assignments where sites carry complex amplitudes.
  • enumVariant: SuperpositionDomain
QuantumThermodynamicVerificationDomainEstablished 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_).
  • enumVariant: QuantumThermodynamic
ArithmeticValuationVerificationDomainEstablished 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.
  • enumVariant: ArithmeticValuation
ComposedAlgebraicVerificationDomainVerification domain for composed operation identities — algebraic properties of operator compositions including dispatch, inference, accumulation, lease, and session composition operations.
  • enumVariant: ComposedAlgebraic
UniversalValidityScopeKindHolds for all k in N. No minimum k constraint.
  • enumVariant: Universal
ParametricLowerValidityScopeKindHolds for all k >= k_min, where k_min is given by validKMin.
  • enumVariant: ParametricLower
ParametricRangeValidityScopeKindHolds for k_min <= k <= k_max. Both validKMin and validKMax required.
  • enumVariant: ParametricRange
LevelSpecificValidityScopeKindHolds only at exactly one level, given by a WittLevelBinding.
  • enumVariant: LevelSpecific
RingReflectionGeometricCharacterReflection through the origin of the additive ring: neg(x) = -x mod 2^n. One of the two generators of D_{2^n}.
HypercubeReflectionGeometricCharacterReflection through the centre of the hypercube: bnot(x) = (2^n-1) ⊕ x. The second generator of D_{2^n}.
RotationGeometricCharacterRotation by one step: succ(x) = (x+1) mod 2^n. The composition of the two reflections.
RotationInverseGeometricCharacterRotation by one step in the reverse direction: pred(x) = (x-1) mod 2^n.
TranslationGeometricCharacterTranslation along the ring axis: add(x,y), sub(x,y). Preserves Hamming distance locally.
ScalingGeometricCharacterScaling along the ring axis: mul(x,y) = (x×y) mod 2^n.
HypercubeTranslationGeometricCharacterTranslation along the hypercube axis: xor(x,y) = x ⊕ y. Preserves ring distance locally.
HypercubeProjectionGeometricCharacterProjection onto a hypercube face: and(x,y) = x ∧ y. Idempotent; collapses dimensions.
HypercubeJoinGeometricCharacterJoin on the hypercube lattice: or(x,y) = x ∨ y. Idempotent; dual to projection.
ConstraintSelectionGeometricCharacterGeometric character of dispatch: constraint-guided selection over the resolver registry lattice.
ResolutionTraversalGeometricCharacterGeometric character of inference: traversal through the φ-pipeline resolution graph P ∘ Π ∘ G.
SiteBindingGeometricCharacterGeometric character of accumulation: progressive pinning of site states in the context lattice.
SitePartitionGeometricCharacterGeometric character of lease partition: splitting a shared context into disjoint site-set leases.
SessionMergeGeometricCharacterGeometric character of session composition: merging disjoint lease sessions into a unified resolution context.
negInvolutionRing 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).
  • arity: 1
  • hasGeometricCharacter: RingReflection
bnotInvolutionHypercube reflection: bnot(x) = (2^n - 1) ⊕ x (bitwise complement). The second generator of D_{2^n}. bnot(bnot(x)) = x.
  • arity: 1
  • hasGeometricCharacter: HypercubeReflection
succUnaryOpSuccessor: succ(x) = neg(bnot(x)) = (x + 1) mod 2^n. The critical identity: succ is the composition neg ∘ bnot.
  • arity: 1
  • hasGeometricCharacter: Rotation
  • composedOf: [neg, bnot]
  • inverse: pred
predUnaryOpPredecessor: pred(x) = bnot(neg(x)) = (x - 1) mod 2^n. The inverse of succ. pred is the composition bnot ∘ neg.
  • arity: 1
  • hasGeometricCharacter: RotationInverse
  • composedOf: [bnot, neg]
  • inverse: succ
addBinaryOpRing addition: add(x, y) = (x + y) mod 2^n. Commutative, associative; identity element is 0.
  • arity: 2
  • hasGeometricCharacter: Translation
  • commutative: true
  • associative: true
  • identity: 0
  • inverse: sub
subBinaryOpRing subtraction: sub(x, y) = (x - y) mod 2^n. Not commutative, not associative.
  • arity: 2
  • hasGeometricCharacter: Translation
  • commutative: false
  • associative: false
mulBinaryOpRing multiplication: mul(x, y) = (x × y) mod 2^n. Commutative, associative; identity element is 1.
  • arity: 2
  • hasGeometricCharacter: Scaling
  • commutative: true
  • associative: true
  • identity: 1
xorBinaryOpBitwise exclusive or: xor(x, y) = x ⊕ y. Commutative, associative; identity element is 0.
  • arity: 2
  • hasGeometricCharacter: HypercubeTranslation
  • commutative: true
  • associative: true
  • identity: 0
andBinaryOpBitwise and: and(x, y) = x ∧ y. Commutative, associative.
  • arity: 2
  • hasGeometricCharacter: HypercubeProjection
  • commutative: true
  • associative: true
orBinaryOpBitwise or: or(x, y) = x ∨ y. Commutative, associative.
  • arity: 2
  • hasGeometricCharacter: HypercubeJoin
  • commutative: true
  • associative: true
dispatchDispatchOperationδ(q, R) = R(q): dispatches a query to the matching resolver in the registry. Non-commutative, non-associative.
  • arity: 2
  • hasGeometricCharacter: ConstraintSelection
  • commutative: false
  • associative: false
  • operatorSignature: Query × ResolverRegistry → Resolver
inferInferenceOperationι(s, C) = P(Π(G(s, C))): the φ-pipeline composed into a single inference step. Non-commutative, non-associative.
  • arity: 2
  • hasGeometricCharacter: ResolutionTraversal
  • commutative: false
  • associative: false
  • operatorSignature: Symbol × Context → ResolvedType
accumulateAccumulationOperationα(b, C) = C': accumulates a binding into a resolution context, pinning a site. Non-commutative, associative at convergence (SR_10).
  • arity: 2
  • hasGeometricCharacter: SiteBinding
  • commutative: false
  • associative: true
  • operatorSignature: Binding × Context → Context
partition_opLeasePartitionOperationλ(S, k) = (L₁, …, Lₖ): partitions a shared context into k disjoint leases. Non-commutative, non-associative.
  • arity: 2
  • hasGeometricCharacter: SitePartition
  • commutative: false
  • associative: false
  • operatorSignature: SharedContext × ℕ → ContextLease^k
compose_opSessionCompositionOperationκ(S₁, S₂) = S₁ ∪ S₂: composes two sessions with disjoint leases into one. Commutative, associative (SR_8).
  • arity: 2
  • hasGeometricCharacter: SessionMerge
  • commutative: true
  • associative: true
  • operatorSignature: Session × Session → Session
Critical IdentityIdentityThe 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.
  • lhs: succ
  • rhs: [neg, bnot]
  • forAll: term_criticalIdentity_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
AD_1IdentityAddressing bijection: addresses(glyph(d)) = d. Round-trip from datum through glyph and back is identity.
  • lhs: term_AD_1_lhs
  • rhs: term_AD_1_rhs
  • forAll: term_AD_1_forAll
  • verificationDomain: Analytical
AD_2IdentityEmbedding coherence: glyph(ι(addresses(a))) = ι_addr(a). The addressing diagram commutes through embeddings.
  • lhs: term_AD_2_lhs
  • rhs: term_AD_2_rhs
  • forAll: term_AD_2_forAll
  • verificationDomain: Analytical
R_A1IdentityAdditive associativity: add(x, add(y, z)) = add(add(x, y), z).
  • lhs: term_R_A1_lhs
  • rhs: term_R_A1_rhs
  • forAll: term_R_A1_forAll
  • verificationDomain: Algebraic
R_A2IdentityAdditive identity: add(x, 0) = x.
  • lhs: term_R_A2_lhs
  • rhs: term_R_A2_rhs
  • forAll: term_R_A2_forAll
  • verificationDomain: Algebraic
R_A3IdentityAdditive inverse: add(x, neg(x)) = 0.
  • lhs: term_R_A3_lhs
  • rhs: term_R_A3_rhs
  • forAll: term_R_A3_forAll
  • verificationDomain: Algebraic
R_A4IdentityAdditive commutativity: add(x, y) = add(y, x).
  • lhs: term_R_A4_lhs
  • rhs: term_R_A4_rhs
  • forAll: term_R_A4_forAll
  • verificationDomain: Algebraic
R_A5IdentitySubtraction definition: sub(x, y) = add(x, neg(y)).
  • lhs: term_R_A5_lhs
  • rhs: term_R_A5_rhs
  • forAll: term_R_A5_forAll
  • verificationDomain: Algebraic
R_A6IdentityNegation involution: neg(neg(x)) = x.
  • lhs: term_R_A6_lhs
  • rhs: term_R_A6_rhs
  • forAll: term_R_A6_forAll
  • verificationDomain: Algebraic
R_M1IdentityMultiplicative associativity: mul(x, mul(y, z)) = mul(mul(x, y), z).
  • lhs: term_R_M1_lhs
  • rhs: term_R_M1_rhs
  • forAll: term_R_M1_forAll
  • verificationDomain: Algebraic
R_M2IdentityMultiplicative identity: mul(x, 1) = x.
  • lhs: term_R_M2_lhs
  • rhs: term_R_M2_rhs
  • forAll: term_R_M2_forAll
  • verificationDomain: Algebraic
R_M3IdentityMultiplicative commutativity: mul(x, y) = mul(y, x).
  • lhs: term_R_M3_lhs
  • rhs: term_R_M3_rhs
  • forAll: term_R_M3_forAll
  • verificationDomain: Algebraic
R_M4IdentityDistributivity: mul(x, add(y, z)) = add(mul(x, y), mul(x, z)).
  • lhs: term_R_M4_lhs
  • rhs: term_R_M4_rhs
  • forAll: term_R_M4_forAll
  • verificationDomain: Algebraic
R_M5IdentityAnnihilation: mul(x, 0) = 0.
  • lhs: term_R_M5_lhs
  • rhs: term_R_M5_rhs
  • forAll: term_R_M5_forAll
  • verificationDomain: Algebraic
B_1IdentityXOR associativity: xor(x, xor(y, z)) = xor(xor(x, y), z).
  • lhs: term_B_1_lhs
  • rhs: term_B_1_rhs
  • forAll: term_B_1_forAll
  • verificationDomain: Algebraic
B_2IdentityXOR identity: xor(x, 0) = x.
  • lhs: term_B_2_lhs
  • rhs: term_B_2_rhs
  • forAll: term_B_2_forAll
  • verificationDomain: Algebraic
B_3IdentityXOR self-inverse: xor(x, x) = 0.
  • lhs: term_B_3_lhs
  • rhs: term_B_3_rhs
  • forAll: term_B_3_forAll
  • verificationDomain: Algebraic
B_4IdentityAND associativity: and(x, and(y, z)) = and(and(x, y), z).
  • lhs: term_B_4_lhs
  • rhs: term_B_4_rhs
  • forAll: term_B_4_forAll
  • verificationDomain: Algebraic
B_5IdentityAND identity: and(x, 2^n - 1) = x.
  • lhs: term_B_5_lhs
  • rhs: term_B_5_rhs
  • forAll: term_B_5_forAll
  • verificationDomain: Algebraic
B_6IdentityAND annihilation: and(x, 0) = 0.
  • lhs: term_B_6_lhs
  • rhs: term_B_6_rhs
  • forAll: term_B_6_forAll
  • verificationDomain: Algebraic
B_7IdentityOR associativity: or(x, or(y, z)) = or(or(x, y), z).
  • lhs: term_B_7_lhs
  • rhs: term_B_7_rhs
  • forAll: term_B_7_forAll
  • verificationDomain: Algebraic
B_8IdentityOR identity: or(x, 0) = x.
  • lhs: term_B_8_lhs
  • rhs: term_B_8_rhs
  • forAll: term_B_8_forAll
  • verificationDomain: Algebraic
B_9IdentityAbsorption: and(x, or(x, y)) = x.
  • lhs: term_B_9_lhs
  • rhs: term_B_9_rhs
  • forAll: term_B_9_forAll
  • verificationDomain: Algebraic
B_10IdentityAND distributes over OR: and(x, or(y, z)) = or(and(x, y), and(x, z)).
  • lhs: term_B_10_lhs
  • rhs: term_B_10_rhs
  • forAll: term_B_10_forAll
  • verificationDomain: Algebraic
B_11IdentityDe Morgan 1: bnot(and(x, y)) = or(bnot(x), bnot(y)).
  • lhs: term_B_11_lhs
  • rhs: term_B_11_rhs
  • forAll: term_B_11_forAll
  • verificationDomain: Algebraic
B_12IdentityDe Morgan 2: bnot(or(x, y)) = and(bnot(x), bnot(y)).
  • lhs: term_B_12_lhs
  • rhs: term_B_12_rhs
  • forAll: term_B_12_forAll
  • verificationDomain: Algebraic
B_13IdentityBnot involution: bnot(bnot(x)) = x.
  • lhs: term_B_13_lhs
  • rhs: term_B_13_rhs
  • forAll: term_B_13_forAll
  • verificationDomain: Algebraic
X_1IdentityNeg via subtraction: neg(x) = sub(0, x).
  • lhs: term_X_1_lhs
  • rhs: term_X_1_rhs
  • forAll: term_X_1_forAll
  • verificationDomain: Algebraic
X_2IdentityComplement via XOR: bnot(x) = xor(x, 2^n - 1).
  • lhs: term_X_2_lhs
  • rhs: term_X_2_rhs
  • forAll: term_X_2_forAll
  • verificationDomain: Algebraic
X_3IdentitySucc via addition: succ(x) = add(x, 1).
  • lhs: term_X_3_lhs
  • rhs: term_X_3_rhs
  • forAll: term_X_3_forAll
  • verificationDomain: Algebraic
X_4IdentityPred via subtraction: pred(x) = sub(x, 1).
  • lhs: term_X_4_lhs
  • rhs: term_X_4_rhs
  • forAll: term_X_4_forAll
  • verificationDomain: Algebraic
X_5IdentityNeg-bnot bridge: neg(x) = add(bnot(x), 1).
  • lhs: term_X_5_lhs
  • rhs: term_X_5_rhs
  • forAll: term_X_5_forAll
  • verificationDomain: Algebraic
X_6IdentityComplement predecessor: bnot(x) = pred(neg(x)).
  • lhs: term_X_6_lhs
  • rhs: term_X_6_rhs
  • forAll: term_X_6_forAll
  • verificationDomain: Algebraic
X_7IdentityXOR-add bridge: xor(x, y) = add(x, y) - 2 * and(x, y) (in Z before mod).
  • lhs: term_X_7_lhs
  • rhs: term_X_7_rhs
  • forAll: term_X_7_forAll
  • verificationDomain: Algebraic
D_1IdentityRotation order: succ^[2^n](x) = x.
  • lhs: term_D_1_lhs
  • rhs: term_D_1_rhs
  • forAll: term_D_1_forAll
  • verificationDomain: Algebraic
D_3IdentityConjugation: neg(succ(neg(x))) = pred(x).
  • lhs: term_D_3_lhs
  • rhs: term_D_3_rhs
  • forAll: term_D_3_forAll
  • verificationDomain: Algebraic
D_4IdentityReverse composition: bnot(neg(x)) = pred(x).
  • lhs: term_D_4_lhs
  • rhs: term_D_4_rhs
  • forAll: term_D_4_forAll
  • verificationDomain: Algebraic
D_5IdentityGroup closure: D_[2^n] = [succ^k, neg ∘ succ^k : 0 ≤ k < 2^n].
  • lhs: term_D_5_lhs
  • rhs: term_D_5_rhs
  • forAll: term_D_5_forAll
  • verificationDomain: Algebraic
U_1IdentityUnit group decomposition: R_n× ≅ Z/2 × Z/2^[n-2] for n ≥ 3.
  • lhs: term_U_1_lhs
  • rhs: term_U_1_rhs
  • forAll: term_U_1_forAll
  • verificationDomain: Algebraic
U_2IdentityUnit group special cases: R_1× ≅ [1]; R_2× ≅ Z/2.
  • lhs: term_U_2_lhs
  • rhs: term_U_2_rhs
  • forAll: term_U_2_forAll
  • verificationDomain: Algebraic
U_3IdentityMultiplicative order: ord(u) = lcm(ord((-1)^a), ord(3^b)).
  • lhs: term_U_3_lhs
  • rhs: term_U_3_rhs
  • forAll: term_U_3_forAll
  • verificationDomain: Algebraic
U_4IdentityResonance period: ord_g(2) divides φ(g).
  • lhs: term_U_4_lhs
  • rhs: term_U_4_rhs
  • forAll: term_U_4_forAll
  • verificationDomain: Algebraic
U_5IdentityStep formula derivation: step_g = 2 * ((g - (2^n mod g)) mod g) + 1.
  • lhs: term_U_5_lhs
  • rhs: term_U_5_rhs
  • forAll: term_U_5_forAll
  • verificationDomain: Algebraic
AG_1IdentityScaling not dihedral: μ_u ∉ D_[2^n] for u ≠ ±1.
  • lhs: term_AG_1_lhs
  • rhs: term_AG_1_rhs
  • forAll: term_AG_1_forAll
  • verificationDomain: Algebraic
AG_2IdentityAffine group: Aff(R_n) = R_n× ⋉ R_n.
  • lhs: term_AG_2_lhs
  • rhs: term_AG_2_rhs
  • forAll: term_AG_2_forAll
  • verificationDomain: Algebraic
AG_3IdentityAffine group order: |Aff(R_n)| = 2^[2n-1].
  • lhs: term_AG_3_lhs
  • rhs: term_AG_3_rhs
  • forAll: term_AG_3_forAll
  • verificationDomain: Algebraic
AG_4IdentitySubgroup inclusion: D_[2^n] ⊂ Aff(R_n) with u ∈ [±1].
  • lhs: term_AG_4_lhs
  • rhs: term_AG_4_rhs
  • forAll: term_AG_4_forAll
  • verificationDomain: Algebraic
CA_1IdentityAddition decomposition: add(x,y)_k = xor(x_k, xor(y_k, c_k(x,y))).
  • lhs: term_CA_1_lhs
  • rhs: term_CA_1_rhs
  • forAll: term_CA_1_forAll
  • verificationDomain: Algebraic
CA_2IdentityCarry recurrence: c_[k+1](x,y) = or(and(x_k,y_k), and(xor(x_k,y_k), c_k)).
  • lhs: term_CA_2_lhs
  • rhs: term_CA_2_rhs
  • forAll: term_CA_2_forAll
  • verificationDomain: Algebraic
CA_3IdentityCarry commutativity: c(x, y) = c(y, x).
  • lhs: term_CA_3_lhs
  • rhs: term_CA_3_rhs
  • forAll: term_CA_3_forAll
  • verificationDomain: Algebraic
CA_4IdentityZero carry: c(x, 0) = 0 at all positions.
  • lhs: term_CA_4_lhs
  • rhs: term_CA_4_rhs
  • forAll: term_CA_4_forAll
  • verificationDomain: Algebraic
CA_5IdentityNegation carry: c(x, neg(x))_k = 1 for k > v_2(x).
  • lhs: term_CA_5_lhs
  • rhs: term_CA_5_rhs
  • forAll: term_CA_5_forAll
  • verificationDomain: Algebraic
CA_6IdentityCarry-incompatibility link: d_Δ(x, y) > 0 iff ∃ k : c_k(x,y) = 1.
  • lhs: term_CA_6_lhs
  • rhs: term_CA_6_rhs
  • forAll: term_CA_6_forAll
  • verificationDomain: Algebraic
C_1IdentityConstraint pin union: pins of a composite constraint equal the union of component pins.
  • lhs: term_C_1_lhs
  • rhs: term_C_1_rhs
  • forAll: term_C_1_forAll
  • verificationDomain: Algebraic
C_2IdentityConstraint composition commutativity.
  • lhs: term_C_2_lhs
  • rhs: term_C_2_rhs
  • forAll: term_C_2_forAll
  • verificationDomain: Algebraic
C_3IdentityConstraint composition associativity.
  • lhs: term_C_3_lhs
  • rhs: term_C_3_rhs
  • forAll: term_C_3_forAll
  • verificationDomain: Algebraic
C_4IdentityConstraint composition idempotence.
  • lhs: term_C_4_lhs
  • rhs: term_C_4_rhs
  • forAll: term_C_4_forAll
  • verificationDomain: Algebraic
C_5IdentityConstraint composition identity element.
  • lhs: term_C_5_lhs
  • rhs: term_C_5_rhs
  • forAll: term_C_5_forAll
  • verificationDomain: Algebraic
C_6IdentityConstraint composition annihilator.
  • lhs: term_C_6_lhs
  • rhs: term_C_6_rhs
  • forAll: term_C_6_forAll
  • verificationDomain: Algebraic
CDIIdentityConstraint-depth invariant: carry complexity of the residue representation equals the type depth.
  • lhs: term_CDI_lhs
  • rhs: term_CDI_rhs
  • forAll: term_CDI_forAll
  • verificationDomain: Algebraic
CL_1IdentityConstraint quotient lattice isomorphism to power set.
  • lhs: term_CL_1_lhs
  • rhs: term_CL_1_rhs
  • forAll: term_CL_1_forAll
  • verificationDomain: Algebraic
CL_2IdentityLattice join equals constraint composition.
  • lhs: term_CL_2_lhs
  • rhs: term_CL_2_rhs
  • forAll: term_CL_2_forAll
  • verificationDomain: Algebraic
CL_3IdentityLattice meet pins the intersection of component pins.
  • lhs: term_CL_3_lhs
  • rhs: term_CL_3_rhs
  • forAll: term_CL_3_forAll
  • verificationDomain: Algebraic
CL_4IdentityConstraint lattice distributivity.
  • lhs: term_CL_4_lhs
  • rhs: term_CL_4_rhs
  • forAll: term_CL_4_forAll
  • verificationDomain: Algebraic
CL_5IdentityConstraint lattice complement existence.
  • lhs: term_CL_5_lhs
  • rhs: term_CL_5_rhs
  • forAll: term_CL_5_forAll
  • verificationDomain: Algebraic
CM_1IdentityConstraint redundancy criterion.
  • lhs: term_CM_1_lhs
  • rhs: term_CM_1_rhs
  • forAll: term_CM_1_forAll
  • verificationDomain: Algebraic
CM_2IdentityMinimal cover via greedy irredundant removal.
  • lhs: term_CM_2_lhs
  • rhs: term_CM_2_rhs
  • forAll: term_CM_2_forAll
  • verificationDomain: Algebraic
CM_3IdentityMinimum constraint count to cover n sites.
  • lhs: term_CM_3_lhs
  • rhs: term_CM_3_rhs
  • forAll: term_CM_3_forAll
  • verificationDomain: Algebraic
CR_1IdentityResidue constraint cost is the step formula.
  • lhs: term_CR_1_lhs
  • rhs: term_CR_1_rhs
  • forAll: term_CR_1_forAll
  • verificationDomain: Algebraic
CR_2IdentityCarry constraint cost is the popcount of the pattern.
  • lhs: term_CR_2_lhs
  • rhs: term_CR_2_rhs
  • forAll: term_CR_2_forAll
  • verificationDomain: Algebraic
CR_3IdentityDepth constraint cost is sum of residue and carry costs.
  • lhs: term_CR_3_lhs
  • rhs: term_CR_3_rhs
  • forAll: term_CR_3_forAll
  • verificationDomain: Algebraic
CR_4IdentityComposite constraint cost is subadditive.
  • lhs: term_CR_4_lhs
  • rhs: term_CR_4_rhs
  • forAll: term_CR_4_forAll
  • verificationDomain: Algebraic
CR_5IdentityOptimal resolution order is increasing cost.
  • lhs: term_CR_5_lhs
  • rhs: term_CR_5_rhs
  • forAll: term_CR_5_forAll
  • verificationDomain: Algebraic
F_1IdentitySite monotonicity: a pinned site cannot be unpinned.
  • lhs: term_F_1_lhs
  • rhs: term_F_1_rhs
  • forAll: term_F_1_forAll
  • verificationDomain: Algebraic
F_2IdentitySite budget upper bound: at most n pin operations to close.
  • lhs: term_F_2_lhs
  • rhs: term_F_2_rhs
  • forAll: term_F_2_forAll
  • verificationDomain: Algebraic
F_3IdentitySite budget conservation: pinned + free = total sites.
  • lhs: term_F_3_lhs
  • rhs: term_F_3_rhs
  • forAll: term_F_3_forAll
  • verificationDomain: Algebraic
F_4IdentitySite budget closure: closed iff all sites pinned.
  • lhs: term_F_4_lhs
  • rhs: term_F_4_rhs
  • forAll: term_F_4_forAll
  • verificationDomain: Algebraic
FL_1IdentitySite lattice bottom: all sites free.
  • lhs: term_FL_1_lhs
  • rhs: term_FL_1_rhs
  • forAll: term_FL_1_forAll
  • verificationDomain: Algebraic
FL_2IdentitySite lattice top: all sites pinned.
  • lhs: term_FL_2_lhs
  • rhs: term_FL_2_rhs
  • forAll: term_FL_2_forAll
  • verificationDomain: Algebraic
FL_3IdentitySite lattice join is union of pinnings.
  • lhs: term_FL_3_lhs
  • rhs: term_FL_3_rhs
  • forAll: term_FL_3_forAll
  • verificationDomain: Algebraic
FL_4IdentitySite lattice height equals n.
  • lhs: term_FL_4_lhs
  • rhs: term_FL_4_rhs
  • forAll: term_FL_4_forAll
  • verificationDomain: Algebraic
FPM_1IdentityUnit partition membership: x is a unit iff site_0(x) = 1 (x is odd).
  • lhs: term_FPM_1_lhs
  • rhs: term_FPM_1_rhs
  • forAll: term_FPM_1_forAll
  • verificationDomain: Algebraic
FPM_2IdentityExterior partition membership: x is exterior iff x is not in the carrier of T.
  • lhs: term_FPM_2_lhs
  • rhs: term_FPM_2_rhs
  • forAll: term_FPM_2_forAll
  • verificationDomain: Algebraic
FPM_3IdentityIrreducible partition membership: x is irreducible iff x is not a unit, exterior, or reducible.
  • lhs: term_FPM_3_lhs
  • rhs: term_FPM_3_rhs
  • forAll: term_FPM_3_forAll
  • verificationDomain: Algebraic
FPM_4IdentityReducible partition membership: x is reducible iff x is not a unit, exterior, or irreducible.
  • lhs: term_FPM_4_lhs
  • rhs: term_FPM_4_rhs
  • forAll: term_FPM_4_forAll
  • verificationDomain: Algebraic
FPM_5Identity2-adic decomposition: every element factors as 2^{v(x)} times an odd unit.
  • lhs: term_FPM_5_lhs
  • rhs: term_FPM_5_rhs
  • forAll: term_FPM_5_forAll
  • verificationDomain: Algebraic
FPM_6IdentityStratum size formula.
  • lhs: term_FPM_6_lhs
  • rhs: term_FPM_6_rhs
  • forAll: term_FPM_6_forAll
  • verificationDomain: Algebraic
FPM_7IdentityBase type partition cardinalities.
  • lhs: term_FPM_7_lhs
  • rhs: term_FPM_7_rhs
  • forAll: term_FPM_7_forAll
  • verificationDomain: Algebraic
FS_1IdentitySite extraction: site_k(x) is the k-th bit of x.
  • lhs: term_FS_1_lhs
  • rhs: term_FS_1_rhs
  • forAll: term_FS_1_forAll
  • verificationDomain: Algebraic
FS_2IdentitySite 0 is parity.
  • lhs: term_FS_2_lhs
  • rhs: term_FS_2_rhs
  • forAll: term_FS_2_forAll
  • verificationDomain: Algebraic
FS_3IdentityProgressive site determination: site_k given lower sites determines x mod 2^{k+1}.
  • lhs: term_FS_3_lhs
  • rhs: term_FS_3_rhs
  • forAll: term_FS_3_forAll
  • verificationDomain: Algebraic
FS_4IdentityCumulative site determination: sites 0..k together determine x mod 2^{k+1}.
  • lhs: term_FS_4_lhs
  • rhs: term_FS_4_rhs
  • forAll: term_FS_4_forAll
  • verificationDomain: Algebraic
FS_5IdentityComplete site determination: all n sites determine x uniquely.
  • lhs: term_FS_5_lhs
  • rhs: term_FS_5_rhs
  • forAll: term_FS_5_forAll
  • verificationDomain: Algebraic
FS_6IdentityStratum from sites: v_2(x) is the minimum k where site_k(x) = 1.
  • lhs: term_FS_6_lhs
  • rhs: term_FS_6_rhs
  • forAll: term_FS_6_forAll
  • verificationDomain: Algebraic
FS_7IdentityDepth bound: depth(x) ≤ v_2(x) for irreducible elements.
  • lhs: term_FS_7_lhs
  • rhs: term_FS_7_rhs
  • forAll: term_FS_7_forAll
  • verificationDomain: Algebraic
RE_1IdentityResolution strategy equivalence: dihedral, canonical-form, and evaluation resolvers all compute the same partition.
  • lhs: term_RE_1_lhs
  • rhs: term_RE_1_rhs
  • forAll: term_RE_1_forAll
  • verificationDomain: Pipeline
IR_1IdentityResolution monotonicity: pinned count never decreases.
  • lhs: term_IR_1_lhs
  • rhs: term_IR_1_rhs
  • forAll: term_IR_1_forAll
  • verificationDomain: Pipeline
IR_2IdentityResolution convergence bound: at most n iterations.
  • lhs: term_IR_2_lhs
  • rhs: term_IR_2_rhs
  • forAll: term_IR_2_forAll
  • verificationDomain: Pipeline
IR_3IdentityConvergence rate definition.
  • lhs: term_IR_3_lhs
  • rhs: term_IR_3_rhs
  • forAll: term_IR_3_forAll
  • verificationDomain: Pipeline
IR_4IdentityResolution termination: loop terminates if constraint set spans all sites.
  • lhs: term_IR_4_lhs
  • rhs: term_IR_4_rhs
  • forAll: term_IR_4_forAll
  • verificationDomain: Pipeline
SF_1IdentityOptimal resolution level for a factor: n ≡ 0 (mod ord_g(2)).
  • lhs: term_SF_1_lhs
  • rhs: term_SF_1_rhs
  • forAll: term_SF_1_forAll
  • verificationDomain: Pipeline
SF_2IdentityConstraint ordering by step cost: smaller step_g first.
  • lhs: term_SF_2_lhs
  • rhs: term_SF_2_rhs
  • forAll: term_SF_2_forAll
  • verificationDomain: Pipeline
RD_1IdentityResolution determinism: same type and constraint sequence yield unique partition.
  • lhs: term_RD_1_lhs
  • rhs: term_RD_1_rhs
  • forAll: term_RD_1_forAll
  • verificationDomain: Pipeline
RD_2IdentityOrder independence: complete constraint sets yield the same partition regardless of order.
  • lhs: term_RD_2_lhs
  • rhs: term_RD_2_rhs
  • forAll: term_RD_2_forAll
  • verificationDomain: Pipeline
SE_1IdentityEvaluation resolver directly computes the set-theoretic partition.
  • lhs: term_SE_1_lhs
  • rhs: term_SE_1_rhs
  • forAll: term_SE_1_forAll
  • verificationDomain: Pipeline
SE_2IdentityDihedral factorization resolver yields the same partition via orbit decomposition.
  • lhs: term_SE_2_lhs
  • rhs: term_SE_2_rhs
  • forAll: term_SE_2_forAll
  • verificationDomain: Pipeline
SE_3IdentityCanonical form resolver yields the same partition via confluent rewrite.
  • lhs: term_SE_3_lhs
  • rhs: term_SE_3_rhs
  • forAll: term_SE_3_forAll
  • verificationDomain: Pipeline
SE_4IdentityAll three strategies compute the same set-theoretic partition.
  • lhs: term_SE_4_lhs
  • rhs: term_SE_4_rhs
  • forAll: term_SE_4_forAll
  • verificationDomain: Pipeline
OO_1IdentityBenefit of a constraint is the number of new pins it provides.
  • lhs: term_OO_1_lhs
  • rhs: term_OO_1_rhs
  • forAll: term_OO_1_forAll
  • verificationDomain: Pipeline
OO_2IdentityConstraint cost is step or popcount depending on type.
  • lhs: term_OO_2_lhs
  • rhs: term_OO_2_rhs
  • forAll: term_OO_2_forAll
  • verificationDomain: Pipeline
OO_3IdentityGreedy selection maximizes benefit-to-cost ratio.
  • lhs: term_OO_3_lhs
  • rhs: term_OO_3_rhs
  • forAll: term_OO_3_forAll
  • verificationDomain: Pipeline
OO_4IdentityGreedy approximation achieves (1 − 1/e) ≈ 63% of optimal.
  • lhs: term_OO_4_lhs
  • rhs: term_OO_4_rhs
  • forAll: term_OO_4_forAll
  • verificationDomain: Pipeline
OO_5IdentityTiebreaker: prefer vertical (residue) before horizontal (carry).
  • lhs: term_OO_5_lhs
  • rhs: term_OO_5_rhs
  • forAll: term_OO_5_forAll
  • verificationDomain: Pipeline
CB_1IdentityMinimum convergence rate: 1 site per iteration (worst case).
  • lhs: term_CB_1_lhs
  • rhs: term_CB_1_rhs
  • forAll: term_CB_1_forAll
  • verificationDomain: Pipeline
CB_2IdentityMaximum convergence rate: n sites in 1 iteration (best case).
  • lhs: term_CB_2_lhs
  • rhs: term_CB_2_rhs
  • forAll: term_CB_2_forAll
  • verificationDomain: Pipeline
CB_3IdentityExpected residue constraint rate: ⌊log_2(m)⌋ sites per constraint.
  • lhs: term_CB_3_lhs
  • rhs: term_CB_3_rhs
  • forAll: term_CB_3_forAll
  • verificationDomain: Pipeline
CB_4IdentityStall detection: convergenceRate < 1 for 2 iterations suggests insufficiency.
  • lhs: term_CB_4_lhs
  • rhs: term_CB_4_rhs
  • forAll: term_CB_4_forAll
  • verificationDomain: Pipeline
CB_5IdentitySufficiency criterion: pin union covers all site positions.
  • lhs: term_CB_5_lhs
  • rhs: term_CB_5_rhs
  • forAll: term_CB_5_forAll
  • verificationDomain: Pipeline
CB_6IdentityIteration bound for k constraints: at most min(k, n) iterations.
  • lhs: term_CB_6_lhs
  • rhs: term_CB_6_rhs
  • forAll: term_CB_6_forAll
  • verificationDomain: Pipeline
OB_M1IdentityRing metric triangle inequality.
  • lhs: term_OB_M1_lhs
  • rhs: term_OB_M1_rhs
  • forAll: term_OB_M1_forAll
  • verificationDomain: Analytical
OB_M2IdentityHamming metric triangle inequality.
  • lhs: term_OB_M2_lhs
  • rhs: term_OB_M2_rhs
  • forAll: term_OB_M2_forAll
  • verificationDomain: Analytical
OB_M3IdentityIncompatibility metric is the absolute difference of ring and Hamming metrics.
  • lhs: term_OB_M3_lhs
  • rhs: term_OB_M3_rhs
  • forAll: term_OB_M3_forAll
  • verificationDomain: Analytical
OB_M4IdentityNegation preserves ring metric.
  • lhs: term_OB_M4_lhs
  • rhs: term_OB_M4_rhs
  • forAll: term_OB_M4_forAll
  • verificationDomain: Analytical
OB_M5IdentityBitwise complement preserves Hamming metric.
  • lhs: term_OB_M5_lhs
  • rhs: term_OB_M5_rhs
  • forAll: term_OB_M5_forAll
  • verificationDomain: Analytical
OB_M6IdentitySuccessor preserves ring metric but may change Hamming metric.
  • lhs: term_OB_M6_lhs
  • rhs: term_OB_M6_rhs
  • forAll: term_OB_M6_forAll
  • verificationDomain: Analytical
OB_C1IdentityNegation-complement commutator is constant 2.
  • lhs: term_OB_C1_lhs
  • rhs: term_OB_C1_rhs
  • forAll: term_OB_C1_forAll
  • verificationDomain: Analytical
OB_C2IdentityNegation-translation commutator.
  • lhs: term_OB_C2_lhs
  • rhs: term_OB_C2_rhs
  • forAll: term_OB_C2_forAll
  • verificationDomain: Analytical
OB_C3IdentityComplement-XOR commutator is trivial.
  • lhs: term_OB_C3_lhs
  • rhs: term_OB_C3_rhs
  • forAll: term_OB_C3_forAll
  • verificationDomain: Analytical
OB_H1IdentityAdditive paths have trivial monodromy (abelian ⇒ path-independent).
  • lhs: term_OB_H1_lhs
  • rhs: term_OB_H1_rhs
  • forAll: term_OB_H1_forAll
  • verificationDomain: Analytical
OB_H2IdentityDihedral generator paths have monodromy in D_{2^n}.
  • lhs: term_OB_H2_lhs
  • rhs: term_OB_H2_rhs
  • forAll: term_OB_H2_forAll
  • verificationDomain: Analytical
OB_H3IdentitySuccessor-only closed path winding number.
  • lhs: term_OB_H3_lhs
  • rhs: term_OB_H3_rhs
  • forAll: term_OB_H3_forAll
  • verificationDomain: Analytical
OB_P1IdentityPath length is additive under concatenation.
  • lhs: term_OB_P1_lhs
  • rhs: term_OB_P1_rhs
  • forAll: term_OB_P1_forAll
  • verificationDomain: Analytical
OB_P2IdentityTotal variation is subadditive under concatenation.
  • lhs: term_OB_P2_lhs
  • rhs: term_OB_P2_rhs
  • forAll: term_OB_P2_forAll
  • verificationDomain: Analytical
OB_P3IdentityReduction length is additive under sequential composition.
  • lhs: term_OB_P3_lhs
  • rhs: term_OB_P3_rhs
  • forAll: term_OB_P3_forAll
  • verificationDomain: Analytical
CT_1IdentityCatastrophe boundaries are powers of 2.
  • lhs: term_CT_1_lhs
  • rhs: term_CT_1_rhs
  • forAll: term_CT_1_forAll
  • verificationDomain: Analytical
CT_2IdentityOdd prime catastrophe transitions visibility via residue constraints.
  • lhs: term_CT_2_lhs
  • rhs: term_CT_2_rhs
  • forAll: term_CT_2_forAll
  • verificationDomain: Analytical
CT_3IdentityCatastrophe threshold is normalized step cost.
  • lhs: term_CT_3_lhs
  • rhs: term_CT_3_rhs
  • forAll: term_CT_3_forAll
  • verificationDomain: Analytical
CT_4IdentityComposite catastrophe threshold is max of component thresholds.
  • lhs: term_CT_4_lhs
  • rhs: term_CT_4_rhs
  • forAll: term_CT_4_forAll
  • verificationDomain: Analytical
CF_1IdentityCurvature flux is the sum of incompatibility along a path.
  • lhs: term_CF_1_lhs
  • rhs: term_CF_1_rhs
  • forAll: term_CF_1_forAll
  • verificationDomain: Analytical
CF_2IdentityResolution cost is bounded below by curvature flux of optimal path.
  • lhs: term_CF_2_lhs
  • rhs: term_CF_2_rhs
  • forAll: term_CF_2_forAll
  • verificationDomain: Analytical
CF_3IdentitySuccessor curvature flux: trailing_ones(x) for most x, n−1 at maximum.
  • lhs: term_CF_3_lhs
  • rhs: term_CF_3_rhs
  • forAll: term_CF_3_forAll
  • verificationDomain: Analytical
CF_4IdentityTotal successor curvature flux over R_n equals 2^n − 2.
  • lhs: term_CF_4_lhs
  • rhs: term_CF_4_rhs
  • forAll: term_CF_4_forAll
  • verificationDomain: Analytical
HG_1IdentityAdditive holonomy is trivial (abelian group).
  • lhs: term_HG_1_lhs
  • rhs: term_HG_1_rhs
  • forAll: term_HG_1_forAll
  • verificationDomain: Analytical
HG_2IdentityDihedral generator holonomy group is D_{2^n}.
  • lhs: term_HG_2_lhs
  • rhs: term_HG_2_rhs
  • forAll: term_HG_2_forAll
  • verificationDomain: Analytical
HG_3IdentityUnit multiplication holonomy equals the unit group.
  • lhs: term_HG_3_lhs
  • rhs: term_HG_3_rhs
  • forAll: term_HG_3_forAll
  • verificationDomain: Analytical
HG_4IdentityFull holonomy group is the affine group.
  • lhs: term_HG_4_lhs
  • rhs: term_HG_4_rhs
  • forAll: term_HG_4_forAll
  • verificationDomain: Analytical
HG_5IdentityHolonomy group decomposition into dihedral and non-trivial units.
  • lhs: term_HG_5_lhs
  • rhs: term_HG_5_rhs
  • forAll: term_HG_5_forAll
  • verificationDomain: Analytical
T_C1IdentityCategory left identity: compose(id, f) = f.
  • lhs: term_T_C1_lhs
  • rhs: term_T_C1_rhs
  • forAll: term_T_C1_forAll
  • verificationDomain: Geometric
T_C2IdentityCategory right identity: compose(f, id) = f.
  • lhs: term_T_C2_lhs
  • rhs: term_T_C2_rhs
  • forAll: term_T_C2_forAll
  • verificationDomain: Geometric
T_C3IdentityCategory associativity of transform composition.
  • lhs: term_T_C3_lhs
  • rhs: term_T_C3_rhs
  • forAll: term_T_C3_forAll
  • verificationDomain: Geometric
T_C4IdentityComposability condition: f composesWith g iff target(f) = source(g).
  • lhs: term_T_C4_lhs
  • rhs: term_T_C4_rhs
  • forAll: term_T_C4_forAll
  • verificationDomain: Geometric
T_I1IdentityNegation is a ring-metric isometry.
  • lhs: term_T_I1_lhs
  • rhs: term_T_I1_rhs
  • forAll: term_T_I1_forAll
  • verificationDomain: Geometric
T_I2IdentityBitwise complement is a Hamming-metric isometry.
  • lhs: term_T_I2_lhs
  • rhs: term_T_I2_rhs
  • forAll: term_T_I2_forAll
  • verificationDomain: Geometric
T_I3IdentitySuccessor as composed isometries: succ = neg ∘ bnot preserves d_R but not d_H.
  • lhs: term_T_I3_lhs
  • rhs: term_T_I3_rhs
  • forAll: term_T_I3_forAll
  • verificationDomain: Geometric
T_I4IdentityRing isometries form a group under composition.
  • lhs: term_T_I4_lhs
  • rhs: term_T_I4_rhs
  • forAll: term_T_I4_forAll
  • verificationDomain: Geometric
T_I5IdentityCurvatureObservable measures failure of ring isometry to be Hamming isometry.
  • lhs: term_T_I5_lhs
  • rhs: term_T_I5_rhs
  • forAll: term_T_I5_forAll
  • verificationDomain: Geometric
T_E1IdentityEmbedding injectivity.
  • lhs: term_T_E1_lhs
  • rhs: term_T_E1_rhs
  • forAll: term_T_E1_forAll
  • verificationDomain: Geometric
T_E2IdentityEmbedding is a ring homomorphism.
  • lhs: term_T_E2_lhs
  • rhs: term_T_E2_rhs
  • forAll: term_T_E2_forAll
  • verificationDomain: Geometric
T_E3IdentityEmbedding transitivity: composition of embeddings is an embedding.
  • lhs: term_T_E3_lhs
  • rhs: term_T_E3_rhs
  • forAll: term_T_E3_forAll
  • verificationDomain: Geometric
T_E4IdentityEmbedding address coherence: glyph ∘ ι ∘ addresses is well-defined.
  • lhs: term_T_E4_lhs
  • rhs: term_T_E4_rhs
  • forAll: term_T_E4_forAll
  • verificationDomain: Geometric
T_A1IdentityDihedral group acts on constraints by transforming them.
  • lhs: term_T_A1_lhs
  • rhs: term_T_A1_rhs
  • forAll: term_T_A1_forAll
  • verificationDomain: Geometric
T_A2IdentityDihedral group action on partitions permutes components.
  • lhs: term_T_A2_lhs
  • rhs: term_T_A2_rhs
  • forAll: term_T_A2_forAll
  • verificationDomain: Geometric
T_A3IdentityDihedral orbits determine irreducibility boundaries.
  • lhs: term_T_A3_lhs
  • rhs: term_T_A3_rhs
  • forAll: term_T_A3_forAll
  • verificationDomain: Geometric
T_A4IdentityFixed points of negation are {0, 2^{n−1}}; bnot has no fixed points.
  • lhs: term_T_A4_lhs
  • rhs: term_T_A4_rhs
  • forAll: term_T_A4_forAll
  • verificationDomain: Geometric
AU_1IdentityAutomorphism group consists of unit multiplications.
  • lhs: term_AU_1_lhs
  • rhs: term_AU_1_rhs
  • forAll: term_AU_1_forAll
  • verificationDomain: Geometric
AU_2IdentityAutomorphism group is isomorphic to the unit group.
  • lhs: term_AU_2_lhs
  • rhs: term_AU_2_rhs
  • forAll: term_AU_2_forAll
  • verificationDomain: Geometric
AU_3IdentityAutomorphism group order is 2^{n−1}.
  • lhs: term_AU_3_lhs
  • rhs: term_AU_3_rhs
  • forAll: term_AU_3_forAll
  • verificationDomain: Geometric
AU_4IdentityIntersection of automorphism group with dihedral group is {id, neg}.
  • lhs: term_AU_4_lhs
  • rhs: term_AU_4_rhs
  • forAll: term_AU_4_forAll
  • verificationDomain: Geometric
AU_5IdentityAffine group is generated by D_{2^n} and μ_3.
  • lhs: term_AU_5_lhs
  • rhs: term_AU_5_rhs
  • forAll: term_AU_5_forAll
  • verificationDomain: Geometric
EF_1IdentityEmbedding functor action on morphisms.
  • lhs: term_EF_1_lhs
  • rhs: term_EF_1_rhs
  • forAll: term_EF_1_forAll
  • verificationDomain: Geometric
EF_2IdentityEmbedding functor preserves composition.
  • lhs: term_EF_2_lhs
  • rhs: term_EF_2_rhs
  • forAll: term_EF_2_forAll
  • verificationDomain: Geometric
EF_3IdentityEmbedding functor preserves identities.
  • lhs: term_EF_3_lhs
  • rhs: term_EF_3_rhs
  • forAll: term_EF_3_forAll
  • verificationDomain: Geometric
EF_4IdentityEmbedding functor composition is functorial.
  • lhs: term_EF_4_lhs
  • rhs: term_EF_4_rhs
  • forAll: term_EF_4_forAll
  • verificationDomain: Geometric
EF_5IdentityEmbedding functor preserves ring isometries.
  • lhs: term_EF_5_lhs
  • rhs: term_EF_5_rhs
  • forAll: term_EF_5_forAll
  • verificationDomain: Geometric
EF_6IdentityEmbedding functor maps dihedral subgroup into target dihedral group.
  • lhs: term_EF_6_lhs
  • rhs: term_EF_6_rhs
  • forAll: term_EF_6_forAll
  • verificationDomain: Geometric
EF_7IdentityEmbedding functor maps unit group into target unit group.
  • lhs: term_EF_7_lhs
  • rhs: term_EF_7_rhs
  • forAll: term_EF_7_forAll
  • verificationDomain: Geometric
AA_1IdentityBraille glyph encoding: 6-bit blocks to Braille characters.
  • lhs: term_AA_1_lhs
  • rhs: term_AA_1_rhs
  • forAll: term_AA_1_forAll
  • verificationDomain: Analytical
AA_2IdentityBraille XOR homomorphism: Braille encoding commutes with XOR.
  • lhs: term_AA_2_lhs
  • rhs: term_AA_2_rhs
  • forAll: term_AA_2_forAll
  • verificationDomain: Analytical
AA_3IdentityBraille complement: glyph of bnot(x) is character-wise complement of glyph(x).
  • lhs: term_AA_3_lhs
  • rhs: term_AA_3_rhs
  • forAll: term_AA_3_forAll
  • verificationDomain: Analytical
AA_4IdentityAddition does not lift to address space: no glyph homomorphism for add.
  • lhs: term_AA_4_lhs
  • rhs: term_AA_4_rhs
  • forAll: term_AA_4_forAll
  • verificationDomain: Analytical
AA_5IdentityLiftable operations are exactly the Boolean operations.
  • lhs: term_AA_5_lhs
  • rhs: term_AA_5_rhs
  • forAll: term_AA_5_forAll
  • verificationDomain: Analytical
AA_6IdentityNegation decomposes into liftable bnot and non-liftable succ.
  • lhs: term_AA_6_lhs
  • rhs: term_AA_6_rhs
  • forAll: term_AA_6_forAll
  • verificationDomain: Analytical
AM_1IdentityAddress metric is sum of per-character Hamming distances.
  • lhs: term_AM_1_lhs
  • rhs: term_AM_1_rhs
  • forAll: term_AM_1_forAll
  • verificationDomain: Analytical
AM_2IdentityAddress metric equals Hamming metric on ring elements.
  • lhs: term_AM_2_lhs
  • rhs: term_AM_2_rhs
  • forAll: term_AM_2_forAll
  • verificationDomain: Analytical
AM_3IdentityAddress metric does not preserve ring metric in general.
  • lhs: term_AM_3_lhs
  • rhs: term_AM_3_rhs
  • forAll: term_AM_3_forAll
  • verificationDomain: Analytical
AM_4IdentityAddress incompatibility metric.
  • lhs: term_AM_4_lhs
  • rhs: term_AM_4_rhs
  • forAll: term_AM_4_forAll
  • verificationDomain: Analytical
TH_1IdentityEntropy of a site budget state.
  • lhs: term_TH_1_lhs
  • rhs: term_TH_1_rhs
  • forAll: term_TH_1_forAll
  • verificationDomain: Thermodynamic
TH_2IdentityMaximum entropy: unconstrained state has S = n × ln 2.
  • lhs: term_TH_2_lhs
  • rhs: term_TH_2_rhs
  • forAll: term_TH_2_forAll
  • verificationDomain: Thermodynamic
TH_3IdentityZero entropy: fully resolved state has S = 0.
  • lhs: term_TH_3_lhs
  • rhs: term_TH_3_rhs
  • forAll: term_TH_3_forAll
  • verificationDomain: Thermodynamic
TH_4IdentityLandauer bound on total resolution cost.
  • lhs: term_TH_4_lhs
  • rhs: term_TH_4_rhs
  • forAll: term_TH_4_forAll
  • verificationDomain: Thermodynamic
TH_5IdentityCritical inverse temperature for UOR site system.
  • lhs: term_TH_5_lhs
  • rhs: term_TH_5_rhs
  • forAll: term_TH_5_forAll
  • verificationDomain: Thermodynamic
TH_6IdentityConstraint application removes entropy; convergence rate equals cooling rate.
  • lhs: term_TH_6_lhs
  • rhs: term_TH_6_rhs
  • forAll: term_TH_6_forAll
  • verificationDomain: Thermodynamic
TH_7IdentityCatastropheThreshold is the temperature of a partition phase transition.
  • lhs: term_TH_7_lhs
  • rhs: term_TH_7_rhs
  • forAll: term_TH_7_forAll
  • verificationDomain: Thermodynamic
TH_8IdentityStep formula as free-energy cost of a constraint boundary.
  • lhs: term_TH_8_lhs
  • rhs: term_TH_8_rhs
  • forAll: term_TH_8_forAll
  • verificationDomain: Thermodynamic
TH_9IdentityComputational hardness maps to type incompleteness (high temperature).
  • lhs: term_TH_9_lhs
  • rhs: term_TH_9_rhs
  • forAll: term_TH_9_forAll
  • verificationDomain: Thermodynamic
TH_10IdentityType resolution is measurement; cost ≥ entropy removed.
  • lhs: term_TH_10_lhs
  • rhs: term_TH_10_rhs
  • forAll: term_TH_10_forAll
  • verificationDomain: Thermodynamic
AR_1IdentityAdiabatic schedule: decreasing freeRank, cost-per-site ordering.
  • lhs: term_AR_1_lhs
  • rhs: term_AR_1_rhs
  • forAll: term_AR_1_forAll
  • verificationDomain: Analytical
AR_2IdentityAdiabatic cost is sum of constraint costs in optimal order.
  • lhs: term_AR_2_lhs
  • rhs: term_AR_2_rhs
  • forAll: term_AR_2_forAll
  • verificationDomain: Analytical
AR_3IdentityAdiabatic cost satisfies Landauer bound.
  • lhs: term_AR_3_lhs
  • rhs: term_AR_3_rhs
  • forAll: term_AR_3_forAll
  • verificationDomain: Analytical
AR_4IdentityAdiabatic efficiency η ≤ 1.
  • lhs: term_AR_4_lhs
  • rhs: term_AR_4_rhs
  • forAll: term_AR_4_forAll
  • verificationDomain: Analytical
AR_5IdentityGreedy vs adiabatic cost difference: ≤ 5% for n ≤ 16.
  • lhs: term_AR_5_lhs
  • rhs: term_AR_5_rhs
  • forAll: term_AR_5_forAll
  • verificationDomain: Analytical
PD_1IdentityPhase space definition.
  • lhs: term_PD_1_lhs
  • rhs: term_PD_1_rhs
  • forAll: term_PD_1_forAll
  • verificationDomain: Thermodynamic
PD_2IdentityPhase boundaries occur where g divides 2^n − 1 or g is a power of 2.
  • lhs: term_PD_2_lhs
  • rhs: term_PD_2_rhs
  • forAll: term_PD_2_forAll
  • verificationDomain: Thermodynamic
PD_3IdentityParity boundary divides R_n into equal halves.
  • lhs: term_PD_3_lhs
  • rhs: term_PD_3_rhs
  • forAll: term_PD_3_forAll
  • verificationDomain: Thermodynamic
PD_4IdentityResonance lines in the phase diagram.
  • lhs: term_PD_4_lhs
  • rhs: term_PD_4_rhs
  • forAll: term_PD_4_forAll
  • verificationDomain: Thermodynamic
PD_5IdentityPhase count at level n is at most 2^n (typically O(n)).
  • lhs: term_PD_5_lhs
  • rhs: term_PD_5_rhs
  • forAll: term_PD_5_forAll
  • verificationDomain: Thermodynamic
RC_1IdentityReversible pinning stores prior state in ancilla site.
  • lhs: term_RC_1_lhs
  • rhs: term_RC_1_rhs
  • forAll: term_RC_1_forAll
  • verificationDomain: Thermodynamic
RC_2IdentityReversible pinning has zero total entropy change.
  • lhs: term_RC_2_lhs
  • rhs: term_RC_2_rhs
  • forAll: term_RC_2_forAll
  • verificationDomain: Thermodynamic
RC_3IdentityDeferred Landauer cost at ancilla erasure.
  • lhs: term_RC_3_lhs
  • rhs: term_RC_3_rhs
  • forAll: term_RC_3_forAll
  • verificationDomain: Thermodynamic
RC_4IdentityReversible total cost equals irreversible total cost (redistributed).
  • lhs: term_RC_4_lhs
  • rhs: term_RC_4_rhs
  • forAll: term_RC_4_forAll
  • verificationDomain: Thermodynamic
RC_5IdentityQuantum UOR: superposed sites, cost proportional to winning path.
  • lhs: term_RC_5_lhs
  • rhs: term_RC_5_rhs
  • forAll: term_RC_5_forAll
  • verificationDomain: Thermodynamic
DC_1IdentityRing derivative: ∂_R f(x) = f(succ(x)) - f(x).
  • lhs: term_DC_1_lhs
  • rhs: term_DC_1_rhs
  • forAll: term_DC_1_forAll
  • verificationDomain: Analytical
DC_2IdentityHamming derivative: ∂_H f(x) = f(bnot(x)) - f(x).
  • lhs: term_DC_2_lhs
  • rhs: term_DC_2_rhs
  • forAll: term_DC_2_forAll
  • verificationDomain: Analytical
DC_3IdentityHamming derivative of identity: ∂_H id(x) = -(2x + 1) mod 2^n.
  • lhs: term_DC_3_lhs
  • rhs: term_DC_3_rhs
  • forAll: term_DC_3_forAll
  • verificationDomain: Analytical
DC_4IdentityCommutator from derivatives: [neg, bnot](x) = ∂_R neg(x) - ∂_H neg(x).
  • lhs: term_DC_4_lhs
  • rhs: term_DC_4_rhs
  • forAll: term_DC_4_forAll
  • verificationDomain: Analytical
DC_5IdentityCarry dependence: the difference ∂_R f - ∂_H f decomposes into carry contributions.
  • lhs: term_DC_5_lhs
  • rhs: term_DC_5_rhs
  • forAll: term_DC_5_forAll
  • verificationDomain: Analytical
DC_6IdentityJacobian definition: J_k(x) = ∂_R f_k(x) where f_k = site_k.
  • lhs: term_DC_6_lhs
  • rhs: term_DC_6_rhs
  • forAll: term_DC_6_forAll
  • verificationDomain: Analytical
DC_7IdentityTop-site anomaly: J_{n-1}(x) may differ from lower sites.
  • lhs: term_DC_7_lhs
  • rhs: term_DC_7_rhs
  • forAll: term_DC_7_forAll
  • verificationDomain: Analytical
DC_8IdentityRank-curvature identity: rank(J(x)) = d_H(x, succ(x)) - 1 for generic x.
  • lhs: term_DC_8_lhs
  • rhs: term_DC_8_rhs
  • forAll: term_DC_8_forAll
  • verificationDomain: Analytical
DC_9IdentityTotal curvature from Jacobian: κ(x) = Σ_k J_k(x).
  • lhs: term_DC_9_lhs
  • rhs: term_DC_9_rhs
  • forAll: term_DC_9_forAll
  • verificationDomain: Analytical
DC_10IdentityCurvature-weighted ordering: optimal next constraint maximizes J_k over free sites.
  • lhs: term_DC_10_lhs
  • rhs: term_DC_10_rhs
  • forAll: term_DC_10_forAll
  • verificationDomain: Analytical
DC_11IdentityCurvature equipartition: Σ_{x} J_k(x) ≈ (2^n - 2)/n for each k.
  • lhs: term_DC_11_lhs
  • rhs: term_DC_11_rhs
  • forAll: term_DC_11_forAll
  • verificationDomain: Analytical
HA_1IdentityConstraint nerve: N(C) is the simplicial complex on constraints.
  • lhs: term_HA_1_lhs
  • rhs: term_HA_1_rhs
  • forAll: term_HA_1_forAll
  • verificationDomain: Topological
HA_2IdentityStall iff non-trivial homology: resolution stalls ⟺ H_k(N(C)) ≠ 0 for some k > 0.
  • lhs: term_HA_2_lhs
  • rhs: term_HA_2_rhs
  • forAll: term_HA_2_forAll
  • verificationDomain: Topological
HA_3IdentityBetti-entropy theorem: S_residual ≥ Σ_k β_k × ln 2.
  • lhs: term_HA_3_lhs
  • rhs: term_HA_3_rhs
  • forAll: term_HA_3_forAll
  • verificationDomain: Topological
IT_2IdentityEuler-Poincaré formula for constraint nerve.
  • lhs: term_IT_2_lhs
  • rhs: term_IT_2_rhs
  • forAll: term_IT_2_forAll
  • verificationDomain: Topological
IT_3IdentitySpectral Euler characteristic.
  • lhs: term_IT_3_lhs
  • rhs: term_IT_3_rhs
  • forAll: term_IT_3_forAll
  • verificationDomain: Topological
IT_6IdentitySpectral gap bounds convergence rate from below.
  • lhs: term_IT_6_lhs
  • rhs: term_IT_6_rhs
  • forAll: term_IT_6_forAll
  • verificationDomain: Topological
IT_7aIdentityUOR index theorem (topological form): total curvature minus Euler characteristic equals residual entropy in bits.
  • lhs: term_IT_7a_lhs
  • rhs: term_IT_7a_rhs
  • forAll: term_IT_7a_forAll
  • verificationDomain: IndexTheoretic
  • verificationDomain: Analytical
  • verificationDomain: Topological
IT_7bIdentityUOR index theorem (entropy-topology duality).
  • lhs: term_IT_7b_lhs
  • rhs: term_IT_7b_rhs
  • forAll: term_IT_7b_forAll
  • verificationDomain: IndexTheoretic
  • verificationDomain: Analytical
  • verificationDomain: Topological
IT_7cIdentityUOR index theorem (spectral cost bound): resolution cost ≥ n - χ(N(C)).
  • lhs: term_IT_7c_lhs
  • rhs: term_IT_7c_rhs
  • forAll: term_IT_7c_forAll
  • verificationDomain: IndexTheoretic
  • verificationDomain: Analytical
  • verificationDomain: Topological
IT_7dIdentityUOR index theorem (completeness criterion): resolution is complete iff χ(N(C)) = n and all Betti numbers vanish.
  • lhs: term_IT_7d_lhs
  • rhs: term_IT_7d_rhs
  • forAll: term_IT_7d_forAll
  • verificationDomain: IndexTheoretic
  • verificationDomain: Analytical
  • verificationDomain: Topological
phi_1IdentityRing → Constraints map: negation transforms a residue constraint.
  • lhs: term_phi_1_lhs
  • rhs: term_phi_1_rhs
  • forAll: term_phi_1_forAll
  • verificationDomain: Pipeline
phi_2IdentityConstraints → Sites map: composition maps to union of site pinnings.
  • lhs: term_phi_2_lhs
  • rhs: term_phi_2_rhs
  • forAll: term_phi_2_forAll
  • verificationDomain: Pipeline
phi_3IdentitySites → Partition map: a closed site state determines a unique 4-component partition.
  • lhs: term_phi_3_lhs
  • rhs: term_phi_3_rhs
  • forAll: term_phi_3_forAll
  • verificationDomain: Pipeline
phi_4IdentityResolution pipeline: φ₄ = φ₃ ∘ φ₂ ∘ φ₁ is the composite resolution map.
  • lhs: term_phi_4_lhs
  • rhs: term_phi_4_rhs
  • forAll: term_phi_4_forAll
  • verificationDomain: Pipeline
phi_5IdentityOperations → Observables map: negation preserves d_R, may change d_H.
  • lhs: term_phi_5_lhs
  • rhs: term_phi_5_rhs
  • forAll: term_phi_5_forAll
  • verificationDomain: Pipeline
phi_6IdentityObservables → Refinement map: observables on a state yield a refinement suggestion.
  • lhs: term_phi_6_lhs
  • rhs: term_phi_6_rhs
  • forAll: term_phi_6_forAll
  • verificationDomain: Pipeline
psi_1Identityψ_1: Constraints → SimplicialComplex (nerve construction). Maps a set of constraints to its nerve simplicial complex.
  • lhs: term_psi_1_lhs
  • rhs: term_psi_1_rhs
  • forAll: term_psi_1_forAll
  • verificationDomain: Topological
psi_2Identityψ_2: SimplicialComplex → ChainComplex (chain functor). Maps a simplicial complex to its chain complex.
  • lhs: term_psi_2_lhs
  • rhs: term_psi_2_rhs
  • forAll: term_psi_2_forAll
  • verificationDomain: Topological
psi_3Identityψ_3: ChainComplex → HomologyGroups (homology functor). Computes homology groups from a chain complex.
  • lhs: term_psi_3_lhs
  • rhs: term_psi_3_rhs
  • forAll: term_psi_3_forAll
  • verificationDomain: Topological
psi_5Identityψ_5: ChainComplex → CochainComplex (dualization functor). Dualizes a chain complex to obtain a cochain complex.
  • lhs: term_psi_5_lhs
  • rhs: term_psi_5_rhs
  • forAll: term_psi_5_forAll
  • verificationDomain: Topological
psi_6Identityψ_6: CochainComplex → CohomologyGroups (cohomology functor). Computes cohomology groups from a cochain complex.
  • lhs: term_psi_6_lhs
  • rhs: term_psi_6_rhs
  • forAll: term_psi_6_forAll
  • verificationDomain: Topological
D_{2^n}DihedralGroupThe 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.
  • generatedBy: neg
  • generatedBy: bnot
  • presentation: ⟨r, s | r^{2^n} = s² = e, srs = r⁻¹⟩
Surface SymmetryIdentityThe 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.
  • lhs: term_surfaceSymmetry_lhs
  • rhs: term_surfaceSymmetry_rhs
  • forAll: term_surfaceSymmetry_forAll
  • verificationDomain: Pipeline
CC_1IdentityCompleteness implies O(1) resolution: a CompleteType T satisfies ∀ x ∈ R_n, resolution(x, T) terminates in O(1).
  • lhs: term_CC_1_lhs
  • rhs: term_CC_1_rhs
  • forAll: term_CC_1_forAll
  • verificationDomain: Pipeline
CC_2IdentityCompleteness is monotone: if T ⊆ T' (T' has more constraints), then completeness(T) implies completeness(T').
  • lhs: term_CC_2_lhs
  • rhs: term_CC_2_rhs
  • forAll: term_CC_2_forAll
  • verificationDomain: Algebraic
CC_3IdentityWitness composition: concat(W₁, W₂) is a valid audit trail iff W₁.sitesClosed + W₂.sitesClosed = n.
  • lhs: term_CC_3_lhs
  • rhs: term_CC_3_rhs
  • forAll: term_CC_3_forAll
  • verificationDomain: Algebraic
CC_4IdentityThe CompletenessResolver is the unique fixed point of the ψ-pipeline applied to a CompletenessCandidate.
  • lhs: term_CC_4_lhs
  • rhs: term_CC_4_rhs
  • forAll: term_CC_4_forAll
  • verificationDomain: Pipeline
CC_5IdentityCompletenessCertificate soundness: cert.verified = true implies χ(N(C)) = n and for all k: β_k = 0.
  • lhs: term_CC_5_lhs
  • rhs: term_CC_5_rhs
  • forAll: term_CC_5_forAll
  • verificationDomain: Topological
QL_1Identityneg(bnot(x)) = succ(x) holds in Z/(2ⁿ)Z for all n ≥ 1. Universal form of the Critical Identity across all quantum levels.
  • lhs: term_QL_1_lhs
  • rhs: term_QL_1_rhs
  • forAll: term_QL_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
QL_2IdentityThe dihedral group D_{2ⁿ} generated by neg and bnot has order 2ⁿ⁺¹ for all n ≥ 1.
  • lhs: term_QL_2_lhs
  • rhs: term_QL_2_rhs
  • forAll: term_QL_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
QL_3IdentityThe reduction distribution P(j) = 2^{-j} is the Boltzmann distribution at β* = ln 2 for all n ≥ 1.
  • lhs: term_QL_3_lhs
  • rhs: term_QL_3_rhs
  • forAll: term_QL_3_forAll
  • verificationDomain: Thermodynamic
  • universallyValid: true
  • validityKind: Universal
QL_4IdentityThe site budget of a PrimitiveType at quantum level n is exactly n (one site per bit).
  • lhs: term_QL_4_lhs
  • rhs: term_QL_4_rhs
  • forAll: term_QL_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
QL_5IdentityResolution complexity for a CompleteType is O(1) for all n ≥ 1.
  • lhs: term_QL_5_lhs
  • rhs: term_QL_5_rhs
  • forAll: term_QL_5_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
QL_6IdentityContent addressing is a bijection for all n ≥ 1 (AD_1/AD_2 universality).
  • lhs: term_QL_6_lhs
  • rhs: term_QL_6_rhs
  • forAll: term_QL_6_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
QL_7IdentityThe ψ-pipeline produces a valid ChainComplex for any ConstrainedType at any quantum level n ≥ 1.
  • lhs: term_QL_7_lhs
  • rhs: term_QL_7_rhs
  • forAll: term_QL_7_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
GR_1IdentityBinding monotonicity: freeRank(B_{i+1}) ≤ freeRank(B_i) for all i in a Session.
  • lhs: term_GR_1_lhs
  • rhs: term_GR_1_rhs
  • forAll: term_GR_1_forAll
  • verificationDomain: Algebraic
GR_2IdentityBinding soundness: a Binding b is sound iff b.datum resolves under b.constraint in O(1).
  • lhs: term_GR_2_lhs
  • rhs: term_GR_2_rhs
  • forAll: term_GR_2_forAll
  • verificationDomain: Pipeline
GR_3IdentitySession convergence: a Session S converges iff there exists i such that freeRank(B_i) = 0.
  • lhs: term_GR_3_lhs
  • rhs: term_GR_3_rhs
  • forAll: term_GR_3_forAll
  • verificationDomain: Algebraic
GR_4IdentityContext reset isolation: bindings in C_fresh are independent of bindings in C_prior after a SessionBoundary.
  • lhs: term_GR_4_lhs
  • rhs: term_GR_4_rhs
  • forAll: term_GR_4_forAll
  • verificationDomain: Algebraic
GR_5IdentityContradiction detection: ContradictionBoundary fires iff there exist bindings b, b' with the same address, different datum, under the same constraint.
  • lhs: term_GR_5_lhs
  • rhs: term_GR_5_rhs
  • forAll: term_GR_5_forAll
  • verificationDomain: Algebraic
TS_1IdentityNerve 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.
  • lhs: term_TS_1_lhs
  • rhs: term_TS_1_rhs
  • forAll: term_TS_1_forAll
  • verificationDomain: Pipeline
TS_2IdentityMinimal 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.
  • lhs: term_TS_2_lhs
  • rhs: term_TS_2_rhs
  • forAll: term_TS_2_forAll
  • verificationDomain: Pipeline
TS_3IdentitySynthesis monotonicity: adding a constraint to a synthesis candidate never decreases the Euler characteristic of the resulting nerve (χ is monotone non-decreasing under constraint addition).
  • lhs: term_TS_3_lhs
  • rhs: term_TS_3_rhs
  • forAll: term_TS_3_forAll
  • verificationDomain: Pipeline
TS_4IdentitySynthesis convergence: the TypeSynthesisResolver terminates for any realisable target in at most n constraint additions (for n-site types).
  • lhs: term_TS_4_lhs
  • rhs: term_TS_4_rhs
  • forAll: term_TS_4_forAll
  • verificationDomain: Pipeline
TS_5IdentitySynthesis–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.
  • lhs: term_TS_5_lhs
  • rhs: term_TS_5_rhs
  • forAll: term_TS_5_forAll
  • verificationDomain: Pipeline
TS_6IdentityJacobian-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).
  • lhs: term_TS_6_lhs
  • rhs: term_TS_6_rhs
  • forAll: term_TS_6_forAll
  • verificationDomain: Pipeline
TS_7IdentityUnreachable 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).
  • lhs: term_TS_7_lhs
  • rhs: term_TS_7_rhs
  • forAll: term_TS_7_forAll
  • verificationDomain: Pipeline
WLS_1IdentityLift 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).
  • lhs: term_WLS_1_lhs
  • rhs: term_WLS_1_rhs
  • forAll: term_WLS_1_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WLS_2IdentityObstruction 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.
  • lhs: term_WLS_2_lhs
  • rhs: term_WLS_2_rhs
  • forAll: term_WLS_2_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WLS_3IdentityMonotone 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.
  • lhs: term_WLS_3_lhs
  • rhs: term_WLS_3_rhs
  • forAll: term_WLS_3_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WLS_4IdentitySpectral 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}.
  • lhs: term_WLS_4_lhs
  • rhs: term_WLS_4_rhs
  • forAll: term_WLS_4_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WLS_5IdentityUniversal 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.
  • lhs: term_WLS_5_lhs
  • rhs: term_WLS_5_rhs
  • forAll: term_WLS_5_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WLS_6Identityψ-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.
  • lhs: term_WLS_6_lhs
  • rhs: term_WLS_6_rhs
  • forAll: term_WLS_6_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
MN_1IdentityHolonomy 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.
  • lhs: term_MN_1_lhs
  • rhs: term_MN_1_rhs
  • forAll: term_MN_1_forAll
  • verificationDomain: Topological
MN_2IdentityAdditive flatness (extends OB_H1): if all constraints in T are additive (ResidueConstraint or DepthConstraint type), then HolonomyGroup(T) = {id} — T is a FlatType.
  • lhs: term_MN_2_lhs
  • rhs: term_MN_2_rhs
  • forAll: term_MN_2_forAll
  • verificationDomain: Topological
MN_3IdentityDihedral 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.
  • lhs: term_MN_3_lhs
  • rhs: term_MN_3_rhs
  • forAll: term_MN_3_forAll
  • verificationDomain: Topological
MN_4IdentityHolonomy-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.)
  • lhs: term_MN_4_lhs
  • rhs: term_MN_4_rhs
  • forAll: term_MN_4_forAll
  • verificationDomain: Topological
MN_5IdentityCompleteType 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.
  • lhs: term_MN_5_lhs
  • rhs: term_MN_5_rhs
  • forAll: term_MN_5_forAll
  • verificationDomain: Topological
MN_6IdentityMonodromy 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).
  • lhs: term_MN_6_lhs
  • rhs: term_MN_6_rhs
  • forAll: term_MN_6_forAll
  • verificationDomain: Topological
MN_7IdentityTwistedType 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.
  • lhs: term_MN_7_lhs
  • rhs: term_MN_7_rhs
  • forAll: term_MN_7_forAll
  • verificationDomain: Topological
PT_1IdentityProduct type site additivity: siteBudget(A × B) = siteBudget(A) + siteBudget(B).
  • lhs: term_PT_1_lhs
  • rhs: term_PT_1_rhs
  • forAll: term_PT_1_forAll
  • verificationDomain: Algebraic
PT_2IdentityProduct type partition product: partition(A × B) = partition(A) ⊗ partition(B).
  • lhs: term_PT_2_lhs
  • rhs: term_PT_2_rhs
  • forAll: term_PT_2_forAll
  • verificationDomain: Topological
PT_3IdentityProduct type Euler additivity: χ(N(C(A × B))) = χ(N(C(A))) + χ(N(C(B))).
  • lhs: term_PT_3_lhs
  • rhs: term_PT_3_rhs
  • forAll: term_PT_3_forAll
  • verificationDomain: IndexTheoretic
PT_4IdentityProduct type entropy additivity: S(A × B) = S(A) + S(B).
  • lhs: term_PT_4_lhs
  • rhs: term_PT_4_rhs
  • forAll: term_PT_4_forAll
  • verificationDomain: Thermodynamic
ST_1IdentitySum type site budget: siteBudget(A + B) = max(siteBudget(A), siteBudget(B)).
  • lhs: term_ST_1_lhs
  • rhs: term_ST_1_rhs
  • forAll: term_ST_1_forAll
  • verificationDomain: Algebraic
ST_2IdentitySum type entropy: S(A + B) = ln 2 + max(S(A), S(B)).
  • lhs: term_ST_2_lhs
  • rhs: term_ST_2_rhs
  • forAll: term_ST_2_forAll
  • verificationDomain: Thermodynamic
GS_1IdentityContext temperature: T_ctx(C) = freeRank(C) × ln 2 / n.
  • lhs: term_GS_1_lhs
  • rhs: term_GS_1_rhs
  • forAll: term_GS_1_forAll
  • verificationDomain: Thermodynamic
GS_2IdentityGrounding degree: σ(C) = (n − freeRank(C)) / n.
  • lhs: term_GS_2_lhs
  • rhs: term_GS_2_rhs
  • forAll: term_GS_2_forAll
  • verificationDomain: Algebraic
GS_3IdentityGrounding monotonicity: σ(B_{i+1}) ≥ σ(B_i) for all i in a Session.
  • lhs: term_GS_3_lhs
  • rhs: term_GS_3_rhs
  • forAll: term_GS_3_forAll
  • verificationDomain: Algebraic
GS_4IdentityGround state equivalence: σ(C) = 1 ↔ freeRank(C) = 0 ↔ S(C) = 0 ↔ T_ctx(C) = 0.
  • lhs: term_GS_4_lhs
  • rhs: term_GS_4_rhs
  • forAll: term_GS_4_forAll
  • verificationDomain: Thermodynamic
GS_5IdentityO(1) resolution guarantee: freeRank(C) = 0 ∧ q.address ∈ bindings(C) → stepCount(q, C) = 0.
  • lhs: term_GS_5_lhs
  • rhs: term_GS_5_rhs
  • forAll: term_GS_5_forAll
  • verificationDomain: Pipeline
GS_6IdentityPre-reduction of effective budget: effectiveBudget(q, C) = max(0, siteBudget(q.type) − |pinnedSites(C) ∩ q.siteSet|).
  • lhs: term_GS_6_lhs
  • rhs: term_GS_6_rhs
  • forAll: term_GS_6_forAll
  • verificationDomain: Algebraic
GS_7IdentityThermodynamic cooling cost: Cost_saturation(C) = n × k_B T × ln 2.
  • lhs: term_GS_7_lhs
  • rhs: term_GS_7_rhs
  • forAll: term_GS_7_forAll
  • verificationDomain: Thermodynamic
MS_1IdentityConnectivity lower bound: β₀(N(C)) ≥ 1 for all non-empty C.
  • lhs: term_MS_1_lhs
  • rhs: term_MS_1_rhs
  • forAll: term_MS_1_forAll
  • verificationDomain: Pipeline
MS_2IdentityEuler capacity ceiling: χ(N(C)) ≤ n for all C at quantum level n.
  • lhs: term_MS_2_lhs
  • rhs: term_MS_2_rhs
  • forAll: term_MS_2_forAll
  • verificationDomain: Algebraic
MS_3IdentityBetti monotonicity under addition: χ(N(C + c)) ≥ χ(N(C)) for any constraint c added to C.
  • lhs: term_MS_3_lhs
  • rhs: term_MS_3_rhs
  • forAll: term_MS_3_forAll
  • verificationDomain: Topological
MS_4IdentityLevel-relative achievability: a signature achievable at quantum level n remains achievable at level n+1.
  • lhs: term_MS_4_lhs
  • rhs: term_MS_4_rhs
  • forAll: term_MS_4_forAll
  • verificationDomain: Pipeline
MS_5IdentityEmpirical completeness convergence: verified SynthesisSignature individuals converge to the exact morphospace boundary.
  • lhs: term_MS_5_lhs
  • rhs: term_MS_5_rhs
  • forAll: term_MS_5_forAll
  • verificationDomain: Pipeline
GD_1IdentityGeodesic 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).
  • lhs: term_GD_1_lhs
  • rhs: term_GD_1_rhs
  • forAll: term_GD_1_forAll
  • verificationDomain: Analytical
GD_2IdentityGeodesic entropy bound: ΔS_step(i) = ln 2 for every step i of a geodesic trace.
  • lhs: term_GD_2_lhs
  • rhs: term_GD_2_rhs
  • forAll: term_GD_2_forAll
  • verificationDomain: Thermodynamic
GD_3IdentityTotal geodesic cost: Cost_geodesic(T) = freeRank_initial × k_B T ln 2 = TH_4.
  • lhs: term_GD_3_lhs
  • rhs: term_GD_3_rhs
  • forAll: term_GD_3_forAll
  • verificationDomain: Thermodynamic
GD_4IdentityGeodesic uniqueness up to step-order equivalence: all geodesics for the same ConstrainedType share stepCount and constraint set.
  • lhs: term_GD_4_lhs
  • rhs: term_GD_4_rhs
  • forAll: term_GD_4_forAll
  • verificationDomain: Analytical
GD_5IdentitySubgeodesic detectability: a trace is sub-geodesic iff ∃ step i where J_k(step_i) < max_{free sites} J_k(state_i).
  • lhs: term_GD_5_lhs
  • rhs: term_GD_5_rhs
  • forAll: term_GD_5_forAll
  • verificationDomain: Pipeline
QM_1IdentityVon Neumann–Landauer bridge: S_vonNeumann(ψ) = Cost_Landauer(collapse(ψ)).
  • lhs: term_QM_1_lhs
  • rhs: term_QM_1_rhs
  • forAll: term_QM_1_forAll
  • verificationDomain: QuantumThermodynamic
QM_2IdentityMeasurement as site topology change: projective collapse on a SuperposedSiteState is topologically equivalent to applying a ResidueConstraint that pins the collapsed site.
  • lhs: term_QM_2_lhs
  • rhs: term_QM_2_rhs
  • forAll: term_QM_2_forAll
  • verificationDomain: Topological
QM_3IdentitySuperposition entropy bound: 0 ≤ S_vN(ψ) ≤ ln 2 for any single-site SuperposedSiteState.
  • lhs: term_QM_3_lhs
  • rhs: term_QM_3_rhs
  • forAll: term_QM_3_forAll
  • verificationDomain: QuantumThermodynamic
QM_4IdentityCollapse idempotence: collapse(collapse(ψ)) = collapse(ψ). Measurement on an already-collapsed state is a no-op.
  • lhs: term_QM_4_lhs
  • rhs: term_QM_4_rhs
  • forAll: term_QM_4_forAll
  • verificationDomain: Algebraic
QM_5IdentityAmplitude normalization (Born rule): the sum of squared amplitudes equals 1 for any well-formed SuperposedSiteState.
  • lhs: term_QM_5_lhs
  • rhs: term_QM_5_rhs
  • forAll: term_QM_5_forAll
  • verificationDomain: QuantumThermodynamic
  • universallyValid: true
  • validityKind: Universal
RC_6IdentityAmplitude renormalization: a SuperposedSiteState can always be normalized to satisfy QM_5.
  • lhs: term_RC_6_lhs
  • rhs: term_RC_6_rhs
  • forAll: term_RC_6_forAll
  • verificationDomain: SuperpositionDomain
  • universallyValid: true
  • validityKind: Universal
FPM_8IdentityPartition exhaustiveness: the four component cardinalities sum to the ring size.
  • lhs: term_FPM_8_lhs
  • rhs: term_FPM_8_rhs
  • forAll: term_FPM_8_forAll
  • verificationDomain: Enumerative
  • universallyValid: true
  • validityKind: Universal
FPM_9IdentityExterior membership criterion: x is exterior iff x is not in the carrier of T.
  • lhs: term_FPM_9_lhs
  • rhs: term_FPM_9_rhs
  • forAll: term_FPM_9_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MN_8IdentityHolonomy classification covering: every ConstrainedType with a computed holonomy group is either flat or twisted, not both.
  • lhs: term_MN_8_lhs
  • rhs: term_MN_8_rhs
  • forAll: term_MN_8_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
QL_8IdentityWitt level chain inverse: wittLevelPredecessor is the left inverse of nextWittLevel.
  • lhs: term_QL_8_lhs
  • rhs: term_QL_8_rhs
  • forAll: term_QL_8_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
D_7IdentityDihedral composition rule: (rᵃ sᵖ)(rᵇ sᵠ) = r^(a + (-1)ᵖ b mod 2ⁿ) s^(p xor q).
  • lhs: term_D_7_lhs
  • rhs: term_D_7_rhs
  • forAll: term_D_7_forAll
  • verificationDomain: Geometric
  • universallyValid: true
  • validityKind: Universal
SP_1IdentityClassical embedding: superposition resolution of a classical (non-superposed) datum reduces to classical resolution.
  • lhs: term_SP_1_lhs
  • rhs: term_SP_1_rhs
  • forAll: term_SP_1_forAll
  • verificationDomain: SuperpositionDomain
  • universallyValid: true
  • validityKind: Universal
SP_2IdentityCollapse–resolve commutativity: collapsing then resolving classically equals resolving in superposition then collapsing.
  • lhs: term_SP_2_lhs
  • rhs: term_SP_2_rhs
  • forAll: term_SP_2_forAll
  • verificationDomain: QuantumThermodynamic
  • universallyValid: true
  • validityKind: Universal
SP_3IdentityAmplitude preservation: the SuperpositionResolver preserves the normalized amplitude vector during ψ-pipeline traversal.
  • lhs: term_SP_3_lhs
  • rhs: term_SP_3_rhs
  • forAll: term_SP_3_forAll
  • verificationDomain: SuperpositionDomain
  • universallyValid: true
  • validityKind: Universal
SP_4IdentityBorn rule outcome probability: the probability of collapsing to site k equals the squared amplitude of that site.
  • lhs: term_SP_4_lhs
  • rhs: term_SP_4_rhs
  • forAll: term_SP_4_forAll
  • verificationDomain: QuantumThermodynamic
  • universallyValid: true
  • validityKind: Universal
PT_2aIdentityProduct type partition tensor: the partition of a product type is the tensor product of the component partitions.
  • lhs: term_PT_2a_lhs
  • rhs: term_PT_2a_rhs
  • forAll: term_PT_2a_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
PT_2bIdentitySum type partition coproduct: the partition of a sum type is the coproduct of the variant partitions.
  • lhs: term_PT_2b_lhs
  • rhs: term_PT_2b_rhs
  • forAll: term_PT_2b_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
GD_6IdentityGeodesic predicate decomposition: a trace is geodesic iff it is both AR_1-ordered and DC_10-selected.
  • lhs: term_GD_6_lhs
  • rhs: term_GD_6_rhs
  • forAll: term_GD_6_forAll
  • verificationDomain: Analytical
  • universallyValid: true
  • validityKind: Universal
WT_1IdentityLiftChain(Q_j, Q_k) is valid CompleteType tower iff every chainStep WittLift has trivial or resolved LiftObstruction.
  • lhs: term_WT_1_lhs
  • rhs: term_WT_1_rhs
  • forAll: term_WT_1_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WT_2IdentityObstruction count bound: the number of non-trivial LiftObstructions in a chain is at most the chain length.
  • lhs: term_WT_2_lhs
  • rhs: term_WT_2_rhs
  • forAll: term_WT_2_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WT_3IdentityResolved basis size formula: the basis size at Q_k equals basisSize(Q_j) + chainLength + obstructionResolutionCost.
  • lhs: term_WT_3_lhs
  • rhs: term_WT_3_rhs
  • forAll: term_WT_3_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WT_4IdentityFlat tower characterization: isFlat(chain) iff obstructionCount = 0 iff HolonomyGroup trivial at every step.
  • lhs: term_WT_4_lhs
  • rhs: term_WT_4_rhs
  • forAll: term_WT_4_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
WT_5IdentityLiftChainCertificate existence: a CompleteType at Q_k satisfies IT_7d with a witness chain.
  • lhs: term_WT_5_lhs
  • rhs: term_WT_5_rhs
  • forAll: term_WT_5_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WT_6IdentitySingle-step reduction: QT_3 with chainLength=1 and cost=0 reduces to QLS_3.
  • lhs: term_WT_6_lhs
  • rhs: term_WT_6_rhs
  • forAll: term_WT_6_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WT_7IdentityFlat chain basis size: for flat chains, resolvedBasisSize(Q_k) = basisSize(Q_j) + (k - j).
  • lhs: term_WT_7_lhs
  • rhs: term_WT_7_rhs
  • forAll: term_WT_7_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
CC_PINSIdentityCarry-constraint site-pinning map: pinsSites(CarryConstraint(p)) equals the set of bit positions where p has a 1 plus the first-zero stopping position.
  • lhs: term_CC_PINS_lhs
  • rhs: term_CC_PINS_rhs
  • forAll: term_CC_PINS_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
CC_COST_SITEIdentityCarry-constraint cost-to-site count: the number of sites pinned by a CarryConstraint equals popcount plus one for the stopping position.
  • lhs: term_CC_COST_SITE_lhs
  • rhs: term_CC_COST_SITE_rhs
  • forAll: term_CC_COST_SITE_forAll
  • verificationDomain: Enumerative
  • universallyValid: true
  • validityKind: Universal
jsat_RRIdentityCRT joint satisfiability: two ResidueConstraints are jointly satisfiable iff the gcd of their moduli divides the difference of their residues.
  • lhs: term_jsat_RR_lhs
  • rhs: term_jsat_RR_rhs
  • forAll: term_jsat_RR_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
jsat_CRIdentityCarry-residue joint satisfiability: a CarryConstraint and ResidueConstraint are jointly satisfiable iff the carry-pinned sites are compatible with the residue class.
  • lhs: term_jsat_CR_lhs
  • rhs: term_jsat_CR_rhs
  • forAll: term_jsat_CR_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
jsat_CCIdentityCarry-carry joint satisfiability: two CarryConstraints are jointly satisfiable iff their bit-patterns have no conflicting positions.
  • lhs: term_jsat_CC_lhs
  • rhs: term_jsat_CC_rhs
  • forAll: term_jsat_CC_forAll
  • verificationDomain: Enumerative
  • universallyValid: true
  • validityKind: Universal
D_8IdentityDihedral inverse formula: the inverse of r^a s^p in D_(2^n) is r^(-(−1)^p a mod 2^n) s^p.
  • lhs: term_D_8_lhs
  • rhs: term_D_8_rhs
  • forAll: term_D_8_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
D_9IdentityDihedral reflection order: every reflection element r^k s^1 in D_(2^n) has order 2.
  • lhs: term_D_9_lhs
  • rhs: term_D_9_rhs
  • forAll: term_D_9_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
EXP_1IdentityMonotone carrier characterization: a ConstrainedType has an upward-closed carrier iff every ResidueConstraint has residue = modulus - 1 and no CarryConstraint or DepthConstraint appears.
  • lhs: term_EXP_1_lhs
  • rhs: term_EXP_1_rhs
  • forAll: term_EXP_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
EXP_2IdentityMonotone constraint count: the number of expressible monotone ConstrainedTypes at quantum level Q_n is 2^n, corresponding to the principal filter count.
  • lhs: term_EXP_2_lhs
  • rhs: term_EXP_2_rhs
  • forAll: term_EXP_2_forAll
  • verificationDomain: Enumerative
  • universallyValid: true
  • validityKind: Universal
EXP_3IdentitySumType carrier semantics: the carrier of a SumType is the coproduct (disjoint union) of component carriers, not the set-theoretic union.
  • lhs: term_EXP_3_lhs
  • rhs: term_EXP_3_rhs
  • forAll: term_EXP_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
ST_3IdentitySumType Euler characteristic additivity: for a SumType with topologically disjoint component nerves, the Euler characteristic is additive.
  • lhs: term_ST_3_lhs
  • rhs: term_ST_3_rhs
  • forAll: term_ST_3_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
ST_4IdentitySumType Betti number additivity: for disjoint component nerves, all Betti numbers are additive.
  • lhs: term_ST_4_lhs
  • rhs: term_ST_4_rhs
  • forAll: term_ST_4_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
ST_5IdentitySumType completeness transfer: a SumType A+B is CompleteType iff both A and B are CompleteType and they have equal quantum levels.
  • lhs: term_ST_5_lhs
  • rhs: term_ST_5_rhs
  • forAll: term_ST_5_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
TS_8IdentityBetti-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.
  • lhs: term_TS_8_lhs
  • rhs: term_TS_8_rhs
  • forAll: term_TS_8_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
TS_9IdentityTypeSynthesisResolver 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.
  • lhs: term_TS_9_lhs
  • rhs: term_TS_9_rhs
  • forAll: term_TS_9_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
TS_10IdentityForbiddenSignature membership criterion: a topological signature is a ForbiddenSignature iff no ConstrainedType with at most n constraints realises it at quantum level Q_n.
  • lhs: term_TS_10_lhs
  • rhs: term_TS_10_rhs
  • forAll: term_TS_10_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
WT_8IdentityObstructionChain length bound: the length of the ObstructionChain from Q_j to Q_k is at most (k-j) times C(basisSize(Q_j), 3).
  • lhs: term_WT_8_lhs
  • rhs: term_WT_8_rhs
  • forAll: term_WT_8_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WT_9IdentityTowerCompletenessResolver termination: the resolver terminates for any finite LiftChain within the QT_8 bound, producing a CompleteType certificate or a bounded ObstructionChain.
  • lhs: term_WT_9_lhs
  • rhs: term_WT_9_rhs
  • forAll: term_WT_9_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
COEFF_1IdentityStandard coefficient ring: the coefficient ring for all psi-pipeline cohomology computations in uor.foundation is Z/2Z, consistent with MN_7.
  • lhs: term_COEFF_1_lhs
  • rhs: term_COEFF_1_rhs
  • forAll: term_COEFF_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
GO_1IdentityGluingObstruction 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.
  • lhs: term_GO_1_lhs
  • rhs: term_GO_1_rhs
  • forAll: term_GO_1_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
GR_6IdentityGrounding 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.
  • lhs: term_GR_6_lhs
  • rhs: term_GR_6_rhs
  • forAll: term_GR_6_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
GR_7IdentityGrounding degree degradation: after re-entry with query q, the grounding degree becomes min(current sigma, 1 - freeRank(q)/n).
  • lhs: term_GR_7_lhs
  • rhs: term_GR_7_rhs
  • forAll: term_GR_7_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
QM_6IdentityAmplitude 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.
  • lhs: term_QM_6_lhs
  • rhs: term_QM_6_rhs
  • forAll: term_QM_6_forAll
  • verificationDomain: SuperpositionDomain
  • universallyValid: true
  • validityKind: Universal
CIC_1IdentityCertificate issuance: every valid Transform admits a TransformCertificate attesting correct source-to-target mapping.
  • lhs: term_CIC_1_lhs
  • rhs: term_CIC_1_rhs
  • forAll: term_CIC_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
CIC_2IdentityCertificate issuance: every metric-preserving Transform admits an IsometryCertificate attesting distance preservation.
  • lhs: term_CIC_2_lhs
  • rhs: term_CIC_2_rhs
  • forAll: term_CIC_2_forAll
  • verificationDomain: Geometric
  • universallyValid: true
  • validityKind: Universal
CIC_3IdentityCertificate issuance: every involutive operation f where f(f(x)) = x admits an InvolutionCertificate.
  • lhs: term_CIC_3_lhs
  • rhs: term_CIC_3_rhs
  • forAll: term_CIC_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
CIC_4IdentityCertificate issuance: full saturation (σ = 1, freeRank = 0) admits a GroundingCertificate.
  • lhs: term_CIC_4_lhs
  • rhs: term_CIC_4_rhs
  • forAll: term_CIC_4_forAll
  • verificationDomain: Thermodynamic
  • universallyValid: true
  • validityKind: Universal
CIC_5IdentityCertificate issuance: an AR_1-ordered and DC_10-selected trace admits a GeodesicCertificate.
  • lhs: term_CIC_5_lhs
  • rhs: term_CIC_5_rhs
  • forAll: term_CIC_5_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
CIC_6IdentityCertificate issuance: a MeasurementEvent verifying the von Neumann–Landauer bridge at β* = ln 2 admits a MeasurementCertificate.
  • lhs: term_CIC_6_lhs
  • rhs: term_CIC_6_rhs
  • forAll: term_CIC_6_forAll
  • verificationDomain: QuantumThermodynamic
  • universallyValid: true
  • validityKind: Universal
CIC_7IdentityCertificate issuance: a MeasurementEvent verifying P(outcome k) = |α_k|² admits a BornRuleVerification certificate.
  • lhs: term_CIC_7_lhs
  • rhs: term_CIC_7_rhs
  • forAll: term_CIC_7_forAll
  • verificationDomain: QuantumThermodynamic
  • universallyValid: true
  • validityKind: Universal
GC_1IdentityCertificate issuance: shared-frame grounding that lands in the type-equivalent neighbourhood admits a GroundingCertificate.
  • lhs: term_GC_1_lhs
  • rhs: term_GC_1_rhs
  • forAll: term_GC_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
GR_8IdentitySession 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.
  • lhs: term_GR_8_lhs
  • rhs: term_GR_8_rhs
  • forAll: term_GR_8_forAll
  • verificationDomain: Algebraic
  • universallyValid: false
  • validityKind: ParametricLower
  • validKMin: 0
GR_9IdentityContextLease disjointness: two distinct leases on the same SharedContext have non-overlapping site sets.
  • lhs: term_GR_9_lhs
  • rhs: term_GR_9_rhs
  • forAll: term_GR_9_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
GR_10IdentityExecutionPolicy confluence: different execution policies on the same pending query set produce the same final resolved state (Church-Rosser for session resolution).
  • lhs: term_GR_10_lhs
  • rhs: term_GR_10_rhs
  • forAll: term_GR_10_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MC_1IdentityLease partition conserves total budget: the sum of freeRank over all leases equals the SharedContext freeRank.
  • lhs: term_MC_1_lhs
  • rhs: term_MC_1_rhs
  • forAll: term_MC_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MC_2IdentityPer-lease binding monotonicity: within a leased sub-domain, freeRank decreases monotonically (SR_1 restricted to lease).
  • lhs: term_MC_2_lhs
  • rhs: term_MC_2_rhs
  • forAll: term_MC_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MC_3IdentityGeneral composition freeRank via inclusion-exclusion.
  • lhs: term_MC_3_lhs
  • rhs: term_MC_3_rhs
  • forAll: term_MC_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MC_4IdentityDisjoint-lease composition is additive: the intersection term vanishes when leases are site-disjoint (SR_9).
  • lhs: term_MC_4_lhs
  • rhs: term_MC_4_rhs
  • forAll: term_MC_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MC_5IdentityPolicy-invariant final binding set: different execution policies produce identical SiteBinding records.
  • lhs: term_MC_5_lhs
  • rhs: term_MC_5_rhs
  • forAll: term_MC_5_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MC_6IdentityFull lease coverage implies composed saturation: k sessions on disjoint covering leases, each locally converged, produce a GroundedContext via composition.
  • lhs: term_MC_6_lhs
  • rhs: term_MC_6_rhs
  • forAll: term_MC_6_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MC_7IdentityDistributed O(1) resolution: a query against a composed GroundedContext resolves in zero steps.
  • lhs: term_MC_7_lhs
  • rhs: term_MC_7_rhs
  • forAll: term_MC_7_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
MC_8IdentityParallelism bound: per-session resolution work is bounded by lease size, not by total site count n.
  • lhs: term_MC_8_lhs
  • rhs: term_MC_8_rhs
  • forAll: term_MC_8_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
WC_1IdentityWitt 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.
  • lhs: term_WC_1_lhs
  • rhs: term_WC_1_rhs
  • forAll: term_WC_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
WC_2IdentityWitt 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).
  • lhs: term_WC_2_lhs
  • rhs: term_WC_2_rhs
  • forAll: term_WC_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
WC_3IdentityCarry recurrence is the Witt polynomial recurrence: CA_2 implements the ghost equation for S_[k+1] at p=2.
  • lhs: term_WC_3_lhs
  • rhs: term_WC_3_rhs
  • forAll: term_WC_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
WC_4IdentityThe δ-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.
  • lhs: term_WC_4_lhs
  • rhs: term_WC_4_rhs
  • forAll: term_WC_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
WC_5IdentityLiftObstruction is equivalent to δ-nonvanishing: a nontrivial LiftObstruction at Q_[k+1] means δ_k ≠ 0 for some element pair.
  • lhs: term_WC_5_lhs
  • rhs: term_WC_5_rhs
  • forAll: term_WC_5_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
WC_6IdentityMetric discrepancy equals Witt defect: d_Δ(x,y) > 0 iff the ghost map correction (carry) is nonzero.
  • lhs: term_WC_6_lhs
  • rhs: term_WC_6_rhs
  • forAll: term_WC_6_forAll
  • verificationDomain: Analytical
  • universallyValid: true
  • validityKind: Universal
WC_7IdentityD_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∞].
  • lhs: term_WC_7_lhs
  • rhs: term_WC_7_rhs
  • forAll: term_WC_7_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
WC_8IdentityD_3 is the Witt-Burnside conjugation relation: neg(succ(neg(x))) = pred(x) is srs = r⁻¹ in the pro-dihedral group.
  • lhs: term_WC_8_lhs
  • rhs: term_WC_8_rhs
  • forAll: term_WC_8_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
WC_9IdentityD_4 is a Witt-Burnside reflection composition: bnot(neg(x)) = pred(x) is the product of two reflections yielding inverse rotation.
  • lhs: term_WC_9_lhs
  • rhs: term_WC_9_rhs
  • forAll: term_WC_9_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
WC_10IdentityThe δ-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).
  • lhs: term_WC_10_lhs
  • rhs: term_WC_10_rhs
  • forAll: term_WC_10_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
WC_11IdentityThe 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.
  • lhs: term_WC_11_lhs
  • rhs: term_WC_11_rhs
  • forAll: term_WC_11_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
WC_12IdentityThe δ-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).
  • lhs: term_WC_12_lhs
  • rhs: term_WC_12_rhs
  • forAll: term_WC_12_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
OA_1IdentityOstrowski product formula at p=2: |2|_2 · |2|_∞ = 1. The 2-adic and Archimedean absolute values of 2 are multiplicative inverses.
  • lhs: term_OA_1_lhs
  • rhs: term_OA_1_rhs
  • forAll: term_OA_1_forAll
  • verificationDomain: ArithmeticValuation
  • universallyValid: true
  • validityKind: Universal
OA_2IdentityCrossing cost equals ln 2: the Archimedean image of one unit of 2-adic valuation, under the product formula, is ln 2 nats.
  • lhs: term_OA_2_lhs
  • rhs: term_OA_2_rhs
  • forAll: term_OA_2_forAll
  • verificationDomain: ArithmeticValuation
  • universallyValid: true
  • validityKind: Universal
OA_3IdentityQM_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.
  • lhs: term_OA_3_lhs
  • rhs: term_OA_3_rhs
  • forAll: term_OA_3_forAll
  • verificationDomain: ArithmeticValuation
  • universallyValid: true
  • validityKind: Universal
OA_4IdentityBorn rule bridge (conditional on amplitude rationality): P(outcome k) = |α_k|_∞², where |·|_∞ is the Archimedean image of the 2-adic amplitude via the product formula.
  • lhs: term_OA_4_lhs
  • rhs: term_OA_4_rhs
  • forAll: term_OA_4_forAll
  • verificationDomain: ArithmeticValuation
  • universallyValid: true
  • validityKind: Universal
OA_5IdentityEntropy 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.
  • lhs: term_OA_5_lhs
  • rhs: term_OA_5_rhs
  • forAll: term_OA_5_forAll
  • verificationDomain: ArithmeticValuation
  • universallyValid: true
  • validityKind: Universal
HT_1IdentityKanComplex(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).
  • lhs: term_HT_1_lhs
  • rhs: term_HT_1_rhs
  • forAll: term_HT_1_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
HT_2IdentityPath components of nerve recover β₀: π₀(N(C)) ≅ Z^{β₀} counts the connected components of the constraint configuration.
  • lhs: term_HT_2_lhs
  • rhs: term_HT_2_rhs
  • forAll: term_HT_2_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
HT_3IdentityMN_6 monodromy is abelianisation of full π₁: the fundamental group π₁(N(C)) surjects onto the HolonomyGroup D_{2^n} via abelianisation.
  • lhs: term_HT_3_lhs
  • rhs: term_HT_3_rhs
  • forAll: term_HT_3_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
HT_4IdentityHigher homotopy groups vanish above nerve dimension: π_k(N(C)) = 0 for all k > dim(N(C)), because the nerve is a finite CW-complex.
  • lhs: term_HT_4_lhs
  • rhs: term_HT_4_rhs
  • forAll: term_HT_4_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
HT_5Identity1-truncation determines flat/twisted classification: τ_{≤1}(N(C)) captures the holonomy action that distinguishes FlatType from TwistedType.
  • lhs: term_HT_5_lhs
  • rhs: term_HT_5_rhs
  • forAll: term_HT_5_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
HT_6IdentityTrivial 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}.
  • lhs: term_HT_6_lhs
  • rhs: term_HT_6_rhs
  • forAll: term_HT_6_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
HT_7IdentityNon-trivial Whitehead product implies lift obstruction: [α, β] ≠ 0 in π_{p+q−1} implies a non-trivial LiftObstruction that Betti numbers alone cannot detect.
  • lhs: term_HT_7_lhs
  • rhs: term_HT_7_rhs
  • forAll: term_HT_7_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
HT_8IdentityHurewicz 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.
  • lhs: term_HT_8_lhs
  • rhs: term_HT_8_rhs
  • forAll: term_HT_8_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
psi_7Identityψ_7: KanComplex → PostnikovTower — compute the Postnikov truncations τ_{≤k} for k = 0, 1, …, dim(N(C)).
  • lhs: term_psi_7_lhs
  • rhs: term_psi_7_rhs
  • forAll: term_psi_7_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
psi_8Identityψ_8: PostnikovTower → HomotopyGroups — extract the homotopy groups π_k from each truncation stage.
  • lhs: term_psi_8_lhs
  • rhs: term_psi_8_rhs
  • forAll: term_psi_8_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
psi_9Identityψ_9: HomotopyGroups → KInvariants — compute the k-invariants κ_k classifying the Postnikov tower.
  • lhs: term_psi_9_lhs
  • rhs: term_psi_9_rhs
  • forAll: term_psi_9_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
HP_1IdentityPipeline composition: nerve construction + Kan promotion = ψ_7 ∘ ψ_1.
  • lhs: term_HP_1_lhs
  • rhs: term_HP_1_rhs
  • forAll: term_HP_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
HP_2IdentityHomotopy extraction agrees with homology on k-skeleton.
  • lhs: term_HP_2_lhs
  • rhs: term_HP_2_rhs
  • forAll: term_HP_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
HP_3Identityk-invariant computation detects QLS_4 convergence.
  • lhs: term_HP_3_lhs
  • rhs: term_HP_3_rhs
  • forAll: term_HP_3_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
HP_4IdentityComplexity bound for homotopy type computation.
  • lhs: term_HP_4_lhs
  • rhs: term_HP_4_rhs
  • forAll: term_HP_4_forAll
  • verificationDomain: Analytical
  • universallyValid: true
  • validityKind: Universal
MD_1IdentityModuli space dimension equals basis size of any contained type.
  • lhs: term_MD_1_lhs
  • rhs: term_MD_1_rhs
  • forAll: term_MD_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MD_2IdentityZeroth deformation cohomology = automorphism group intersected with dihedral group.
  • lhs: term_MD_2_lhs
  • rhs: term_MD_2_rhs
  • forAll: term_MD_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MD_3IdentityFirst deformation cohomology = tangent space to the moduli space at T.
  • lhs: term_MD_3_lhs
  • rhs: term_MD_3_rhs
  • forAll: term_MD_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MD_4IdentitySecond deformation cohomology = LiftObstruction space.
  • lhs: term_MD_4_lhs
  • rhs: term_MD_4_rhs
  • forAll: term_MD_4_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
MD_5IdentityFlatType stratum has codimension zero in the moduli space.
  • lhs: term_MD_5_lhs
  • rhs: term_MD_5_rhs
  • forAll: term_MD_5_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
MD_6IdentityTwistedType stratum has codimension at least 1.
  • lhs: term_MD_6_lhs
  • rhs: term_MD_6_rhs
  • forAll: term_MD_6_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
MD_7IdentityVersalDeformation existence is guaranteed when the obstruction space H² vanishes.
  • lhs: term_MD_7_lhs
  • rhs: term_MD_7_rhs
  • forAll: term_MD_7_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MD_8IdentityA deformation family preserves completeness iff H²(Def(T_t)) = 0 along the entire path.
  • lhs: term_MD_8_lhs
  • rhs: term_MD_8_rhs
  • forAll: term_MD_8_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
MD_9IdentityThe site of a ModuliTowerMap at T has dimension 1 when the obstruction is trivial.
  • lhs: term_MD_9_lhs
  • rhs: term_MD_9_rhs
  • forAll: term_MD_9_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
MD_10IdentityThe site of a ModuliTowerMap at T is empty iff T is a TwistedType at every level.
  • lhs: term_MD_10_lhs
  • rhs: term_MD_10_rhs
  • forAll: term_MD_10_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
MR_1IdentityModuliResolver boundary agrees with MorphospaceBoundary.
  • lhs: term_MR_1_lhs
  • rhs: term_MR_1_rhs
  • forAll: term_MR_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MR_2IdentityStratificationRecord covers every CompleteType in exactly one stratum.
  • lhs: term_MR_2_lhs
  • rhs: term_MR_2_rhs
  • forAll: term_MR_2_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
MR_3IdentityModuliResolver complexity bound.
  • lhs: term_MR_3_lhs
  • rhs: term_MR_3_rhs
  • forAll: term_MR_3_forAll
  • verificationDomain: Analytical
  • universallyValid: true
  • validityKind: Universal
MR_4IdentityAchievable signatures correspond to membership in some HolonomyStratum.
  • lhs: term_MR_4_lhs
  • rhs: term_MR_4_rhs
  • forAll: term_MR_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
CY_1IdentityCarry generates at site k iff and(x_k, y_k) = 1. Extends CA_1 (addition decomposition) and WC_2 (Witt sum correction).
  • lhs: term_CY_1_lhs
  • rhs: term_CY_1_rhs
  • forAll: term_CY_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
CY_2IdentityCarry 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).
  • lhs: term_CY_2_lhs
  • rhs: term_CY_2_rhs
  • forAll: term_CY_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
CY_3IdentityCarry 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.
  • lhs: term_CY_3_lhs
  • rhs: term_CY_3_rhs
  • forAll: term_CY_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
CY_4Identityd_Δ(x,y) = |carryCount(x+y) − hammingDistance(x,y)|. The metric incompatibility IS the discrepancy between carry count and Hamming distance. Strengthens WC_6.
  • lhs: term_CY_4_lhs
  • rhs: term_CY_4_rhs
  • forAll: term_CY_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
CY_5IdentityOptimal 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.
  • lhs: term_CY_5_lhs
  • rhs: term_CY_5_rhs
  • forAll: term_CY_5_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
CY_6IdentitySite ordering theorem: d_Δ is minimized when high-significance sites (upstream in the carry chain) encode the most structurally informative observables.
  • lhs: term_CY_6_lhs
  • rhs: term_CY_6_rhs
  • forAll: term_CY_6_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
CY_7IdentityCarry lookahead: the carry chain for n sites is computable in O(log n) using prefix computation on generate/propagate pairs.
  • lhs: term_CY_7_lhs
  • rhs: term_CY_7_rhs
  • forAll: term_CY_7_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
BM_1Identityσ(C) = (n − freeRank(C)) / n. The saturation metric is the complement of free site ratio. Derives from SC_2.
  • lhs: term_BM_1_lhs
  • rhs: term_BM_1_rhs
  • forAll: term_BM_1_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
BM_2Identityχ = Σ(−1)^k β_k. The Euler characteristic of the constraint nerve. Derives from IT_2.
  • lhs: term_BM_2_lhs
  • rhs: term_BM_2_rhs
  • forAll: term_BM_2_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
BM_3IdentityIndex theorem: Σκ_k − χ = S_residual / ln 2. Links all six metrics. Derives from IT_7a.
  • lhs: term_BM_3_lhs
  • rhs: term_BM_3_rhs
  • forAll: term_BM_3_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
BM_4IdentityJ_k = 0 for pinned sites. The Jacobian vanishes on resolved sites.
  • lhs: term_BM_4_lhs
  • rhs: term_BM_4_rhs
  • forAll: term_BM_4_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
BM_5Identityd_Δ > 0 iff carry ≠ 0. The metric discrepancy equals the Witt defect. Derives from WC_6.
  • lhs: term_BM_5_lhs
  • rhs: term_BM_5_rhs
  • forAll: term_BM_5_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
BM_6IdentityMetric composition tower: d_Δ → {σ, J_k} → β_k → χ → r. Each metric derives from previous ones.
  • lhs: term_BM_6_lhs
  • rhs: term_BM_6_rhs
  • forAll: term_BM_6_forAll
  • verificationDomain: IndexTheoretic
  • universallyValid: true
  • validityKind: Universal
GL_1Identityσ = lower adjoint evaluated at current type. The saturation metric is the lower adjoint of the Galois connection. Derives from SC_2.
  • lhs: term_GL_1_lhs
  • rhs: term_GL_1_rhs
  • forAll: term_GL_1_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
GL_2Identityr = complement of upper adjoint image. The residual freedom is what the type closure does not reach.
  • lhs: term_GL_2_lhs
  • rhs: term_GL_2_rhs
  • forAll: term_GL_2_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
GL_3IdentityCompleteType = fixpoint of Galois connection, σ=1, r=0. Derives from IT_7d.
  • lhs: term_GL_3_lhs
  • rhs: term_GL_3_rhs
  • forAll: term_GL_3_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
GL_4IdentityType refinement = ascending in type lattice = descending in site freedom. The Galois connection reverses order.
  • lhs: term_GL_4_lhs
  • rhs: term_GL_4_rhs
  • forAll: term_GL_4_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
NV_1Identitynerve(C₁ ∪ C₂) = nerve(C₁) ∪ nerve(C₂) for disjoint constraint domains.
  • lhs: term_NV_1_lhs
  • rhs: term_NV_1_rhs
  • forAll: term_NV_1_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
NV_2IdentityMayer–Vietoris: β_k(C₁ ∪ C₂) computable from parts and intersection.
  • lhs: term_NV_2_lhs
  • rhs: term_NV_2_rhs
  • forAll: term_NV_2_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
NV_3IdentitySingle constraint addition: Δβ_k ∈ {−1, 0, +1} per dimension.
  • lhs: term_NV_3_lhs
  • rhs: term_NV_3_rhs
  • forAll: term_NV_3_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
NV_4IdentityConstraint accumulation monotonicity: β_k non-increasing under SR_1. Derives from SR_1.
  • lhs: term_NV_4_lhs
  • rhs: term_NV_4_rhs
  • forAll: term_NV_4_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
SD_1IdentityScalarType grounding: quantize(value, range, bits) produces ring element where d_R reflects value proximity.
  • lhs: term_SD_1_lhs
  • rhs: term_SD_1_rhs
  • forAll: term_SD_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
SD_2IdentitySymbolType grounding: argmin_{encoding} Σ d_Δ over observed pairs (CY_5).
  • lhs: term_SD_2_lhs
  • rhs: term_SD_2_rhs
  • forAll: term_SD_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
SD_3IdentitySequenceType = free monoid on element type with backbone constraint.
  • lhs: term_SD_3_lhs
  • rhs: term_SD_3_rhs
  • forAll: term_SD_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
SD_4IdentityTupleType site count = Σ field site counts, site ordering follows CY_6.
  • lhs: term_SD_4_lhs
  • rhs: term_SD_4_rhs
  • forAll: term_SD_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
SD_5IdentityGraphType constraint nerve = graph nerve, β_k equality.
  • lhs: term_SD_5_lhs
  • rhs: term_SD_5_rhs
  • forAll: term_SD_5_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
SD_6IdentitySetType d_Δ invariant under element permutation, D_{2n} symmetry.
  • lhs: term_SD_6_lhs
  • rhs: term_SD_6_rhs
  • forAll: term_SD_6_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
SD_7IdentityTreeType β_1=0, β_0=1 topological constraints.
  • lhs: term_SD_7_lhs
  • rhs: term_SD_7_rhs
  • forAll: term_SD_7_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
SD_8IdentityTableType = SequenceType(TupleType(S)), functorial decomposition.
  • lhs: term_SD_8_lhs
  • rhs: term_SD_8_rhs
  • forAll: term_SD_8_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
DD_1IdentityDispatch determinism: same query and same registry always yield the same resolver.
  • lhs: term_DD_1_lhs
  • rhs: term_DD_1_rhs
  • forAll: term_DD_1_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
DD_2IdentityDispatch coverage: every query in the registry domain has a matching resolver.
  • lhs: term_DD_2_lhs
  • rhs: term_DD_2_rhs
  • forAll: term_DD_2_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PI_1IdentityInference idempotence: ι(ι(s,C),C) = ι(s,C) on GroundedContext.
  • lhs: term_PI_1_lhs
  • rhs: term_PI_1_rhs
  • forAll: term_PI_1_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PI_2IdentityInference soundness: ι(s,C) resolves to a type consistent with C.
  • lhs: term_PI_2_lhs
  • rhs: term_PI_2_rhs
  • forAll: term_PI_2_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PI_3IdentityInference composition: ι = P ∘ Π ∘ G (references phi_4).
  • lhs: term_PI_3_lhs
  • rhs: term_PI_3_rhs
  • forAll: term_PI_3_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PI_4IdentityInference complexity: O(n) worst case, O(1) on CompleteType.
  • lhs: term_PI_4_lhs
  • rhs: term_PI_4_rhs
  • forAll: term_PI_4_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PI_5IdentityInference coherence: roundTrip(P(Π(G(s)))) = s.
  • lhs: term_PI_5_lhs
  • rhs: term_PI_5_rhs
  • forAll: term_PI_5_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PA_1IdentityAccumulation permutation invariance: accumulating bindings in any order yields the same saturated context (derives from SR_10).
  • lhs: term_PA_1_lhs
  • rhs: term_PA_1_rhs
  • forAll: term_PA_1_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PA_2IdentityAccumulation monotonicity: α(b,C) ⊇ C (the context only grows, never loses bindings). Derives from SR_1.
  • lhs: term_PA_2_lhs
  • rhs: term_PA_2_rhs
  • forAll: term_PA_2_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PA_3IdentityAccumulation soundness: α(b,C) preserves all previously satisfied constraints. Derives from SR_2.
  • lhs: term_PA_3_lhs
  • rhs: term_PA_3_rhs
  • forAll: term_PA_3_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PA_4IdentityAccumulation base preservation: α does not modify previously pinned sites.
  • lhs: term_PA_4_lhs
  • rhs: term_PA_4_rhs
  • forAll: term_PA_4_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PA_5IdentityAccumulation identity: α(∅, C) = C.
  • lhs: term_PA_5_lhs
  • rhs: term_PA_5_rhs
  • forAll: term_PA_5_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PL_1IdentityLease disjointness: partitioned leases have pairwise disjoint site sets (derives from SR_9).
  • lhs: term_PL_1_lhs
  • rhs: term_PL_1_rhs
  • forAll: term_PL_1_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PL_2IdentityLease conservation: union of all leases equals the original shared context (derives from MC_1).
  • lhs: term_PL_2_lhs
  • rhs: term_PL_2_rhs
  • forAll: term_PL_2_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PL_3IdentityLease coverage: every site in the shared context appears in exactly one lease (derives from MC_6).
  • lhs: term_PL_3_lhs
  • rhs: term_PL_3_rhs
  • forAll: term_PL_3_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PK_1IdentityComposition validity: κ(S₁,S₂) is a valid session if S₁,S₂ have disjoint leases (derives from SR_8).
  • lhs: term_PK_1_lhs
  • rhs: term_PK_1_rhs
  • forAll: term_PK_1_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PK_2IdentityDistributed resolution: resolving in κ(S₁,S₂) equals resolving in S₁ or S₂ independently (derives from MC_7).
  • lhs: term_PK_2_lhs
  • rhs: term_PK_2_rhs
  • forAll: term_PK_2_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PP_1IdentityPipeline unification: κ(λₖ(α*(ι(s,·))),C) = resolve(s,C). The full composed pipeline equals the top-level resolution function.
  • lhs: term_PP_1_lhs
  • rhs: term_PP_1_rhs
  • forAll: term_PP_1_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
PE_1IdentityStage 0 initializes state vector to 1.
  • lhs: term_PE_1_lhs
  • rhs: term_PE_1_rhs
  • forAll: term_PE_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PE_2IdentityStage 1 dispatches resolver (δ selects).
  • lhs: term_PE_2_lhs
  • rhs: term_PE_2_rhs
  • forAll: term_PE_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PE_3IdentityStage 2 produces valid ring address (G grounds).
  • lhs: term_PE_3_lhs
  • rhs: term_PE_3_rhs
  • forAll: term_PE_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PE_4IdentityStage 3 resolves constraints (Π terminates).
  • lhs: term_PE_4_lhs
  • rhs: term_PE_4_rhs
  • forAll: term_PE_4_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PE_5IdentityStage 4 accumulates without contradiction (α consistent).
  • lhs: term_PE_5_lhs
  • rhs: term_PE_5_rhs
  • forAll: term_PE_5_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PE_6IdentityStage 5 extracts coherent output (P projects).
  • lhs: term_PE_6_lhs
  • rhs: term_PE_6_rhs
  • forAll: term_PE_6_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PE_7IdentityFull pipeline is the composition PE_6 ∘ … ∘ PE_1.
  • lhs: term_PE_7_lhs
  • rhs: term_PE_7_rhs
  • forAll: term_PE_7_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PM_1IdentityPhase rotation Ω^k at stage k.
  • lhs: term_PM_1_lhs
  • rhs: term_PM_1_rhs
  • forAll: term_PM_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PM_2IdentityPhase gate checks Ω^k at boundary.
  • lhs: term_PM_2_lhs
  • rhs: term_PM_2_rhs
  • forAll: term_PM_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PM_3IdentityGate failure triggers complex conjugate rollback.
  • lhs: term_PM_3_lhs
  • rhs: term_PM_3_rhs
  • forAll: term_PM_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PM_4IdentityRollback is involutory: (z̄)̄ = z.
  • lhs: term_PM_4_lhs
  • rhs: term_PM_4_rhs
  • forAll: term_PM_4_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PM_5IdentityEpoch boundary preserves saturation.
  • lhs: term_PM_5_lhs
  • rhs: term_PM_5_rhs
  • forAll: term_PM_5_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PM_6IdentityService window provides base context.
  • lhs: term_PM_6_lhs
  • rhs: term_PM_6_rhs
  • forAll: term_PM_6_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PM_7IdentityMachine is deterministic given initial state.
  • lhs: term_PM_7_lhs
  • rhs: term_PM_7_rhs
  • forAll: term_PM_7_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
ER_1IdentityStage transition requires guard satisfaction.
  • lhs: term_ER_1_lhs
  • rhs: term_ER_1_rhs
  • forAll: term_ER_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
ER_2IdentityEffect application is atomic.
  • lhs: term_ER_2_lhs
  • rhs: term_ER_2_rhs
  • forAll: term_ER_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
ER_3IdentityGuard evaluation is side-effect-free.
  • lhs: term_ER_3_lhs
  • rhs: term_ER_3_rhs
  • forAll: term_ER_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
ER_4IdentityEffect composition is order-independent within a stage.
  • lhs: term_ER_4_lhs
  • rhs: term_ER_4_rhs
  • forAll: term_ER_4_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
EA_1IdentityEpoch boundary resets free sites.
  • lhs: term_EA_1_lhs
  • rhs: term_EA_1_rhs
  • forAll: term_EA_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
EA_2IdentityGrounding carries across epochs.
  • lhs: term_EA_2_lhs
  • rhs: term_EA_2_rhs
  • forAll: term_EA_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
EA_3IdentityService window bounds context size.
  • lhs: term_EA_3_lhs
  • rhs: term_EA_3_rhs
  • forAll: term_EA_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
EA_4IdentityEpoch admits one datum or one refinement pass.
  • lhs: term_EA_4_lhs
  • rhs: term_EA_4_rhs
  • forAll: term_EA_4_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
OE_1IdentityAdjacent stages with compatible guards may fuse.
  • lhs: term_OE_1_lhs
  • rhs: term_OE_1_rhs
  • forAll: term_OE_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
OE_2IdentityIndependent effects commute.
  • lhs: term_OE_2_lhs
  • rhs: term_OE_2_rhs
  • forAll: term_OE_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
OE_3IdentityDisjoint leases parallelize.
  • lhs: term_OE_3_lhs
  • rhs: term_OE_3_rhs
  • forAll: term_OE_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
OE_4aIdentityStage fusion preserves semantics.
  • lhs: term_OE_4a_lhs
  • rhs: term_OE_4a_rhs
  • forAll: term_OE_4a_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
OE_4bIdentityEffect commutation preserves outcome.
  • lhs: term_OE_4b_lhs
  • rhs: term_OE_4b_rhs
  • forAll: term_OE_4b_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
OE_4cIdentityLease parallelism preserves coverage.
  • lhs: term_OE_4c_lhs
  • rhs: term_OE_4c_rhs
  • forAll: term_OE_4c_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
CS_1IdentityEach stage has bounded cost.
  • lhs: term_CS_1_lhs
  • rhs: term_CS_1_rhs
  • forAll: term_CS_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
CS_2IdentityPipeline cost = sum of stage costs.
  • lhs: term_CS_2_lhs
  • rhs: term_CS_2_rhs
  • forAll: term_CS_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
CS_3IdentityRollback cost is at most forward cost.
  • lhs: term_CS_3_lhs
  • rhs: term_CS_3_rhs
  • forAll: term_CS_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
CS_4IdentityPreflight cost is O(1).
  • lhs: term_CS_4_lhs
  • rhs: term_CS_4_rhs
  • forAll: term_CS_4_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
CS_5IdentityTotal reduction cost bounded by n × stage_max_cost.
  • lhs: term_CS_5_lhs
  • rhs: term_CS_5_rhs
  • forAll: term_CS_5_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
CS_6IdentityBudget 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.
  • lhs: term_CS_6_lhs
  • rhs: term_CS_6_rhs
  • forAll: term_CS_6_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
CS_7IdentityUnit 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.
  • lhs: term_CS_7_lhs
  • rhs: term_CS_7_rhs
  • forAll: term_CS_7_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FA_1IdentityEvery pending query eventually reaches a stage gate.
  • lhs: term_FA_1_lhs
  • rhs: term_FA_1_rhs
  • forAll: term_FA_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
FA_2IdentityNo starvation under bounded epoch admission.
  • lhs: term_FA_2_lhs
  • rhs: term_FA_2_rhs
  • forAll: term_FA_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
FA_3IdentityFair lease allocation under disjoint composition.
  • lhs: term_FA_3_lhs
  • rhs: term_FA_3_rhs
  • forAll: term_FA_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
SW_1IdentityService window bounds context memory.
  • lhs: term_SW_1_lhs
  • rhs: term_SW_1_rhs
  • forAll: term_SW_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
SW_2IdentityWindow slide preserves saturation invariant.
  • lhs: term_SW_2_lhs
  • rhs: term_SW_2_rhs
  • forAll: term_SW_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
SW_3IdentityEvicted epochs release lease resources.
  • lhs: term_SW_3_lhs
  • rhs: term_SW_3_rhs
  • forAll: term_SW_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
SW_4IdentityWindow size ≥ 1 (non-empty).
  • lhs: term_SW_4_lhs
  • rhs: term_SW_4_rhs
  • forAll: term_SW_4_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
LS_1IdentitySuspended lease preserves pinned state.
  • lhs: term_LS_1_lhs
  • rhs: term_LS_1_rhs
  • forAll: term_LS_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
LS_2IdentityLease expiry triggers resource release.
  • lhs: term_LS_2_lhs
  • rhs: term_LS_2_rhs
  • forAll: term_LS_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
LS_3IdentityCheckpoint restore is idempotent.
  • lhs: term_LS_3_lhs
  • rhs: term_LS_3_rhs
  • forAll: term_LS_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
LS_4IdentityActive → Suspended → Active round-trip preserves state.
  • lhs: term_LS_4_lhs
  • rhs: term_LS_4_rhs
  • forAll: term_LS_4_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
TJ_1IdentityAllOrNothing transaction rolls back on any failure.
  • lhs: term_TJ_1_lhs
  • rhs: term_TJ_1_rhs
  • forAll: term_TJ_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
TJ_2IdentityBestEffort transaction commits partial results.
  • lhs: term_TJ_2_lhs
  • rhs: term_TJ_2_rhs
  • forAll: term_TJ_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
TJ_3IdentityTransaction atomicity within a single epoch.
  • lhs: term_TJ_3_lhs
  • rhs: term_TJ_3_rhs
  • forAll: term_TJ_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
AP_1IdentityPartial saturation is monotonically non-decreasing across stages.
  • lhs: term_AP_1_lhs
  • rhs: term_AP_1_rhs
  • forAll: term_AP_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
AP_2IdentityApproximation quality improves with additional epochs.
  • lhs: term_AP_2_lhs
  • rhs: term_AP_2_rhs
  • forAll: term_AP_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
AP_3IdentityDeferred queries are eventually processed or explicitly dropped.
  • lhs: term_AP_3_lhs
  • rhs: term_AP_3_rhs
  • forAll: term_AP_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
EC_1IdentityΩ⁶ = −1: reduction converges in 6 stages (phase half-turn).
  • lhs: term_EC_1_lhs
  • rhs: term_EC_1_rhs
  • forAll: term_EC_1_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
EC_2IdentityComplex conjugate rollback involutory: (z̄)̄ = z.
  • lhs: term_EC_2_lhs
  • rhs: term_EC_2_rhs
  • forAll: term_EC_2_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
EC_3IdentityPairwise convergence: commutator converges to identity.
  • lhs: term_EC_3_lhs
  • rhs: term_EC_3_rhs
  • forAll: term_EC_3_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
EC_4IdentityTriple convergence: associator converges to zero.
  • lhs: term_EC_4_lhs
  • rhs: term_EC_4_rhs
  • forAll: term_EC_4_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
EC_4aIdentityAssociator monotonicity: associator norm non-increasing.
  • lhs: term_EC_4a_lhs
  • rhs: term_EC_4a_rhs
  • forAll: term_EC_4a_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
EC_4bIdentityAssociator finiteness: reaches 0 in bounded steps.
  • lhs: term_EC_4b_lhs
  • rhs: term_EC_4b_rhs
  • forAll: term_EC_4b_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
EC_4cIdentityAssociator vanishing implies associativity on resolved site space.
  • lhs: term_EC_4c_lhs
  • rhs: term_EC_4c_rhs
  • forAll: term_EC_4c_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
EC_5IdentityAdams termination: no convergence level beyond L3_Self.
  • lhs: term_EC_5_lhs
  • rhs: term_EC_5_rhs
  • forAll: term_EC_5_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
DA_1IdentityCayley-Dickson R→C: adjoin i with i²=−1, conjugation (a+bi)* = a−bi.
  • lhs: term_DA_1_lhs
  • rhs: term_DA_1_rhs
  • forAll: term_DA_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
DA_2IdentityCayley-Dickson C→H: adjoin j with j²=−1, ij=k, ji=−k, k²=−1.
  • lhs: term_DA_2_lhs
  • rhs: term_DA_2_rhs
  • forAll: term_DA_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
DA_3IdentityCayley-Dickson H→O: adjoin l, Fano plane products, associativity fails.
  • lhs: term_DA_3_lhs
  • rhs: term_DA_3_rhs
  • forAll: term_DA_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
DA_4IdentityAdams theorem: no normed division algebra of dimension 16 exists.
  • lhs: term_DA_4_lhs
  • rhs: term_DA_4_rhs
  • forAll: term_DA_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
DA_5IdentityConvergence level k lives in k-th division algebra: L0 in R, L1 in C, L2 in H, L3 in O.
  • lhs: term_DA_5_lhs
  • rhs: term_DA_5_rhs
  • forAll: term_DA_5_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
DA_6IdentityCommutator vanishes iff algebra at that level is commutative.
  • lhs: term_DA_6_lhs
  • rhs: term_DA_6_rhs
  • forAll: term_DA_6_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
DA_7IdentityAssociator vanishes iff algebra at that level is associative.
  • lhs: term_DA_7_lhs
  • rhs: term_DA_7_rhs
  • forAll: term_DA_7_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
IN_1Identityd_Δ as interaction cost between entities.
  • lhs: term_IN_1_lhs
  • rhs: term_IN_1_rhs
  • forAll: term_IN_1_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
IN_2IdentityDisjoint leases imply commutator = 0.
  • lhs: term_IN_2_lhs
  • rhs: term_IN_2_rhs
  • forAll: term_IN_2_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
IN_3IdentityShared sites imply commutator > 0.
  • lhs: term_IN_3_lhs
  • rhs: term_IN_3_rhs
  • forAll: term_IN_3_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
IN_4IdentitySR_8 implies negotiation converges (commutator decreases monotonically).
  • lhs: term_IN_4_lhs
  • rhs: term_IN_4_rhs
  • forAll: term_IN_4_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
IN_5IdentityConvergent negotiation selects U(1) ⊂ SU(2).
  • lhs: term_IN_5_lhs
  • rhs: term_IN_5_rhs
  • forAll: term_IN_5_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
IN_6IdentityOutcome space of pairwise negotiation is S².
  • lhs: term_IN_6_lhs
  • rhs: term_IN_6_rhs
  • forAll: term_IN_6_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
IN_7IdentityMutual modeling selects H ⊂ O.
  • lhs: term_IN_7_lhs
  • rhs: term_IN_7_rhs
  • forAll: term_IN_7_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
IN_8IdentityInteraction nerve β_k bounds coupling complexity at dimension k.
  • lhs: term_IN_8_lhs
  • rhs: term_IN_8_rhs
  • forAll: term_IN_8_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
IN_9Identityβ_2(nerve) × max_disagreement bounds associator norm.
  • lhs: term_IN_9_lhs
  • rhs: term_IN_9_rhs
  • forAll: term_IN_9_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
AS_1Identityδ-ι-κ non-associativity: δ reads registry written by κ.
  • lhs: term_AS_1_lhs
  • rhs: term_AS_1_rhs
  • forAll: term_AS_1_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
AS_2Identityι-α-λ non-associativity: λ reads lease state written by α.
  • lhs: term_AS_2_lhs
  • rhs: term_AS_2_rhs
  • forAll: term_AS_2_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
AS_3Identityλ-κ-δ non-associativity: δ reads state written by κ.
  • lhs: term_AS_3_lhs
  • rhs: term_AS_3_rhs
  • forAll: term_AS_3_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
AS_4IdentityRoot cause: non-associativity from read-write interleaving through mediating entity.
  • lhs: term_AS_4_lhs
  • rhs: term_AS_4_rhs
  • forAll: term_AS_4_forAll
  • verificationDomain: ComposedAlgebraic
  • universallyValid: true
  • validityKind: Universal
MO_1IdentityUnit law: I ⊗ A ≅ A ≅ A ⊗ I.
  • lhs: term_MO_1_lhs
  • rhs: term_MO_1_rhs
  • forAll: term_MO_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MO_2IdentityAssociativity: (A⊗B)⊗C ≅ A⊗(B⊗C).
  • lhs: term_MO_2_lhs
  • rhs: term_MO_2_rhs
  • forAll: term_MO_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MO_3IdentityCertificate composition: cert(A⊗B) contains cert(A) and cert(B).
  • lhs: term_MO_3_lhs
  • rhs: term_MO_3_rhs
  • forAll: term_MO_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MO_4Identityσ(A⊗B) ≥ max(σ(A), σ(B)): sequential composition does not lose saturation.
  • lhs: term_MO_4_lhs
  • rhs: term_MO_4_rhs
  • forAll: term_MO_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
MO_5Identityr(A⊗B) ≤ min(r(A), r(B)): residual can only shrink under sequential composition.
  • lhs: term_MO_5_lhs
  • rhs: term_MO_5_rhs
  • forAll: term_MO_5_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
OP_1IdentitySite additivity: siteCount(F(G)) = F.sites + Σ_i G_i.sites.
  • lhs: term_OP_1_lhs
  • rhs: term_OP_1_rhs
  • forAll: term_OP_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
OP_2IdentityGrounding distributivity: grounding(F(G(x))) = F.ground(G.ground(x)).
  • lhs: term_OP_2_lhs
  • rhs: term_OP_2_rhs
  • forAll: term_OP_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
OP_3Identityd_Δ decomposition: d_Δ(F(G)) decomposes into outer + inner d_Δ.
  • lhs: term_OP_3_lhs
  • rhs: term_OP_3_rhs
  • forAll: term_OP_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
OP_4IdentityTable(Tuple(fields)): standard tabular data structure decomposition.
  • lhs: term_OP_4_lhs
  • rhs: term_OP_4_rhs
  • forAll: term_OP_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
OP_5IdentityTree(leaves): standard hierarchical data structure (AST, XML, JSON).
  • lhs: term_OP_5_lhs
  • rhs: term_OP_5_rhs
  • forAll: term_OP_5_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FX_1IdentityPinning decrements free count by exactly 1.
  • lhs: term_FX_1_lhs
  • rhs: term_FX_1_rhs
  • forAll: term_FX_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FX_2IdentityUnbinding increments free count by exactly 1.
  • lhs: term_FX_2_lhs
  • rhs: term_FX_2_rhs
  • forAll: term_FX_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FX_3IdentityPhase effects preserve site budget.
  • lhs: term_FX_3_lhs
  • rhs: term_FX_3_rhs
  • forAll: term_FX_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FX_4IdentityDisjoint effects commute.
  • lhs: term_FX_4_lhs
  • rhs: term_FX_4_rhs
  • forAll: term_FX_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FX_5IdentityComposite free-count delta is additive.
  • lhs: term_FX_5_lhs
  • rhs: term_FX_5_rhs
  • forAll: term_FX_5_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FX_6IdentityEvery ReversibleEffect has an inverse (PinningEffect⁻¹ = UnbindingEffect on same site, PhaseEffect⁻¹ = conjugate phase).
  • lhs: term_FX_6_lhs
  • rhs: term_FX_6_rhs
  • forAll: term_FX_6_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FX_7IdentityExternal effects must match their declared shape.
  • lhs: term_FX_7_lhs
  • rhs: term_FX_7_rhs
  • forAll: term_FX_7_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PR_1IdentityEvery predicate is total: evaluation terminates for all inputs.
  • lhs: term_PR_1_lhs
  • rhs: term_PR_1_rhs
  • forAll: term_PR_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PR_2IdentityEvery predicate is pure: evaluation does not modify state.
  • lhs: term_PR_2_lhs
  • rhs: term_PR_2_rhs
  • forAll: term_PR_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PR_3IdentityExhaustive + mutually exclusive dispatch is deterministic.
  • lhs: term_PR_3_lhs
  • rhs: term_PR_3_rhs
  • forAll: term_PR_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PR_4IdentityMatch evaluation is deterministic given exhaustive, ordered arms.
  • lhs: term_PR_4_lhs
  • rhs: term_PR_4_rhs
  • forAll: term_PR_4_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PR_5IdentityStage transition requires typed guard satisfaction.
  • lhs: term_PR_5_lhs
  • rhs: term_PR_5_rhs
  • forAll: term_PR_5_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
CG_1IdentityEntry guard must be satisfied to enter a stage.
  • lhs: term_CG_1_lhs
  • rhs: term_CG_1_rhs
  • forAll: term_CG_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
CG_2IdentityExit guard must be satisfied, then the stage effect is applied.
  • lhs: term_CG_2_lhs
  • rhs: term_CG_2_rhs
  • forAll: term_CG_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
DIS_1IdentityThe root resolver dispatch table is exhaustive and mutually exclusive over all TypeDefinitions.
  • lhs: term_DIS_1_lhs
  • rhs: term_DIS_1_rhs
  • forAll: term_DIS_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
DIS_2IdentityResolver dispatch is deterministic for every type.
  • lhs: term_DIS_2_lhs
  • rhs: term_DIS_2_rhs
  • forAll: term_DIS_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
PAR_1IdentityDisjoint parallel computations commute: A ⊗ B = B ⊗ A when site targets are disjoint.
  • lhs: term_PAR_1_lhs
  • rhs: term_PAR_1_rhs
  • forAll: term_PAR_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
PAR_2IdentityParallel free-count deltas are additive.
  • lhs: term_PAR_2_lhs
  • rhs: term_PAR_2_rhs
  • forAll: term_PAR_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
PAR_3IdentityPartitioning is exhaustive: component cardinalities sum to total site budget.
  • lhs: term_PAR_3_lhs
  • rhs: term_PAR_3_rhs
  • forAll: term_PAR_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
PAR_4IdentityAll interleavings of disjoint parallel computations yield the same final context.
  • lhs: term_PAR_4_lhs
  • rhs: term_PAR_4_rhs
  • forAll: term_PAR_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
PAR_5IdentityParallel certificate is the conjunction of component certificates plus disjointness.
  • lhs: term_PAR_5_lhs
  • rhs: term_PAR_5_rhs
  • forAll: term_PAR_5_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
HO_1IdentityA ComputationDatum’s ring value is the content hash of its certificate.
  • lhs: term_HO_1_lhs
  • rhs: term_HO_1_rhs
  • forAll: term_HO_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
HO_2IdentityApplication preserves certification.
  • lhs: term_HO_2_lhs
  • rhs: term_HO_2_rhs
  • forAll: term_HO_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
HO_3IdentityComposition certification requires both components certified and type-compatible.
  • lhs: term_HO_3_lhs
  • rhs: term_HO_3_rhs
  • forAll: term_HO_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
HO_4IdentityFully saturated partial application equals direct application.
  • lhs: term_HO_4_lhs
  • rhs: term_HO_4_rhs
  • forAll: term_HO_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
STR_1IdentityEvery epoch terminates: the reduction within each epoch reaches convergence angle π.
  • lhs: term_STR_1_lhs
  • rhs: term_STR_1_rhs
  • forAll: term_STR_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
STR_2IdentityGrounding preservation across epoch boundaries.
  • lhs: term_STR_2_lhs
  • rhs: term_STR_2_rhs
  • forAll: term_STR_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
STR_3IdentityEvery finite prefix computes in finite time.
  • lhs: term_STR_3_lhs
  • rhs: term_STR_3_rhs
  • forAll: term_STR_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
STR_4IdentityThe first epoch starts from the unfold seed context.
  • lhs: term_STR_4_lhs
  • rhs: term_STR_4_rhs
  • forAll: term_STR_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
STR_5IdentityEach subsequent epoch starts from the previous boundary’s continuation context.
  • lhs: term_STR_5_lhs
  • rhs: term_STR_5_rhs
  • forAll: term_STR_5_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
STR_6IdentityLease expiry at an epoch boundary returns claimed sites to the next epoch’s linear budget.
  • lhs: term_STR_6_lhs
  • rhs: term_STR_6_rhs
  • forAll: term_STR_6_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FLR_1IdentityEvery partial computation produces exactly one of Success or Failure.
  • lhs: term_FLR_1_lhs
  • rhs: term_FLR_1_rhs
  • forAll: term_FLR_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FLR_2IdentityA total computation always succeeds.
  • lhs: term_FLR_2_lhs
  • rhs: term_FLR_2_rhs
  • forAll: term_FLR_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
FLR_3IdentitySequential failure propagation: if A fails, B is not evaluated.
  • lhs: term_FLR_3_lhs
  • rhs: term_FLR_3_rhs
  • forAll: term_FLR_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FLR_4IdentityParallel failure independence: one component’s failure does not prevent the other’s success.
  • lhs: term_FLR_4_lhs
  • rhs: term_FLR_4_rhs
  • forAll: term_FLR_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
FLR_5IdentityRecovery produces a new ComputationResult.
  • lhs: term_FLR_5_lhs
  • rhs: term_FLR_5_rhs
  • forAll: term_FLR_5_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
FLR_6IdentityThe reduction’s existing rollback mechanism is a Recovery whose effect is the conjugate phase rotation.
  • lhs: term_FLR_6_lhs
  • rhs: term_FLR_6_rhs
  • forAll: term_FLR_6_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
LN_1IdentityIn a linear trace, every site is targeted exactly once. Total effect count equals site budget.
  • lhs: term_LN_1_lhs
  • rhs: term_LN_1_rhs
  • forAll: term_LN_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
LN_2IdentityAfter a LinearEffect, the target site is pinned.
  • lhs: term_LN_2_lhs
  • rhs: term_LN_2_rhs
  • forAll: term_LN_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
LN_3IdentityA consumed LinearSite cannot be targeted again.
  • lhs: term_LN_3_lhs
  • rhs: term_LN_3_rhs
  • forAll: term_LN_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
LN_4IdentityLease allocation decrements the linear budget by the lease cardinality.
  • lhs: term_LN_4_lhs
  • rhs: term_LN_4_rhs
  • forAll: term_LN_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
LN_5IdentityLease expiry returns claimed sites to the budget.
  • lhs: term_LN_5_lhs
  • rhs: term_LN_5_rhs
  • forAll: term_LN_5_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
LN_6IdentityEvery geodesic trace is a linear trace.
  • lhs: term_LN_6_lhs
  • rhs: term_LN_6_rhs
  • forAll: term_LN_6_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
SB_1IdentitySubtyping is constraint superset: more constraints = more specific.
  • lhs: term_SB_1_lhs
  • rhs: term_SB_1_rhs
  • forAll: term_SB_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
SB_2IdentitySubtype has fewer valid resolutions.
  • lhs: term_SB_2_lhs
  • rhs: term_SB_2_rhs
  • forAll: term_SB_2_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
SB_3IdentityThe constraint nerve of the supertype is a sub-complex of the subtype’s nerve.
  • lhs: term_SB_3_lhs
  • rhs: term_SB_3_rhs
  • forAll: term_SB_3_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
SB_4IdentityCovariance preserves inclusion.
  • lhs: term_SB_4_lhs
  • rhs: term_SB_4_rhs
  • forAll: term_SB_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
SB_5IdentityContravariance reverses inclusion.
  • lhs: term_SB_5_lhs
  • rhs: term_SB_5_rhs
  • forAll: term_SB_5_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
SB_6IdentityLattice depth equals site budget.
  • lhs: term_SB_6_lhs
  • rhs: term_SB_6_rhs
  • forAll: term_SB_6_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
BR_1IdentityEvery recursive step strictly decreases the descent measure.
  • lhs: term_BR_1_lhs
  • rhs: term_BR_1_rhs
  • forAll: term_BR_1_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
BR_2IdentityRecursion depth is bounded by the initial measure value.
  • lhs: term_BR_2_lhs
  • rhs: term_BR_2_rhs
  • forAll: term_BR_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
BR_3IdentityEvery bounded recursion terminates.
  • lhs: term_BR_3_lhs
  • rhs: term_BR_3_rhs
  • forAll: term_BR_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
BR_4IdentityStructural recursion’s measure is the input type’s structural size.
  • lhs: term_BR_4_lhs
  • rhs: term_BR_4_rhs
  • forAll: term_BR_4_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
BR_5IdentityThe base predicate is satisfied exactly when the measure reaches zero.
  • lhs: term_BR_5_lhs
  • rhs: term_BR_5_rhs
  • forAll: term_BR_5_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
RG_1IdentityThe working set is determined by the constraint nerve and the stage’s site targets.
  • lhs: term_RG_1_lhs
  • rhs: term_RG_1_rhs
  • forAll: term_RG_1_forAll
  • verificationDomain: Topological
  • universallyValid: true
  • validityKind: Universal
RG_2IdentityAll addresses within a region are within the region’s diameter under the chosen metric.
  • lhs: term_RG_2_lhs
  • rhs: term_RG_2_rhs
  • forAll: term_RG_2_forAll
  • verificationDomain: Analytical
  • universallyValid: true
  • validityKind: Universal
RG_3IdentityTotal working set size is bounded by the addressable space at the quantum level.
  • lhs: term_RG_3_lhs
  • rhs: term_RG_3_rhs
  • forAll: term_RG_3_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal
RG_4IdentityThe resolver at stage k accesses only addresses within its working set.
  • lhs: term_RG_4_lhs
  • rhs: term_RG_4_rhs
  • forAll: term_RG_4_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
IO_1IdentityIngested data conforms to the source’s declared type.
  • lhs: term_IO_1_lhs
  • rhs: term_IO_1_rhs
  • forAll: term_IO_1_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
IO_2IdentityEmitted data conforms to the sink’s declared type.
  • lhs: term_IO_2_lhs
  • rhs: term_IO_2_rhs
  • forAll: term_IO_2_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
IO_3IdentityEvery ingestion through a source produces a valid ring datum via grounding.
  • lhs: term_IO_3_lhs
  • rhs: term_IO_3_rhs
  • forAll: term_IO_3_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
IO_4IdentityEvery emission through a sink produces a valid surface symbol via projection.
  • lhs: term_IO_4_lhs
  • rhs: term_IO_4_rhs
  • forAll: term_IO_4_forAll
  • verificationDomain: Pipeline
  • universallyValid: true
  • validityKind: Universal
IO_5IdentityEvery boundary effect touches at least one site.
  • lhs: term_IO_5_lhs
  • rhs: term_IO_5_rhs
  • forAll: term_IO_5_forAll
  • verificationDomain: Algebraic
  • universallyValid: true
  • validityKind: Universal

Related Concepts