This is a bridge-space namespace in the Resolve stage of the PRISM pipeline. It provides the resolution infrastructure — queries, partitions, observables, proofs, derivations, and traces that transform inputs into certified results.
A complete term rewriting witness: the full sequence of rewrite steps transforming an original term into its canonical form.
DerivationStep
Thing
An abstract step in a derivation. Concrete subclasses are RewriteStep (term-level rewriting) and RefinementStep (type-level refinement).
RewriteStep
DerivationStep
A single rewrite step in a derivation: the application of one rewrite rule to transform a term.
RefinementStep
DerivationStep
A type-level refinement step: the application of a constraint to narrow a type, pinning additional site coordinates. Complements RewriteStep (term-level) in the derivation hierarchy.
RewriteRule
Thing
A named rewrite rule that can be applied in a derivation step. Each RewriteRule individual represents a specific algebraic law or normalization strategy used during term rewriting.
TermMetrics
Thing
Metrics describing the size and complexity of a term.
SynthesisStep
Thing
A single step in the construction of a SynthesizedType: one constraint added to the synthesis candidate and the resulting change in the constraint nerve's topological signature. Ordered by derivation:stepIndex. Analogous to derivation:RewriteStep in the forward pipeline.
SynthesisCheckpoint
Thing
A persistent snapshot of a ConstraintSearchState at a specific SynthesisStep, allowing a TypeSynthesisResolver to resume exploration after interruption. Essential at Q1+ scale where exhaustive synthesis is computationally significant.
Properties
Name
Kind
Functional
Domain
Range
Comment
originalTerm
Object
true
Derivation
Term
The term at the start of the derivation, before any rewriting.
canonicalTerm
Object
true
Derivation
Term
The canonical form produced at the end of the derivation.
result
Object
true
Derivation
Datum
The datum value obtained by evaluating the canonical term.
step
Object
false
Derivation
RewriteStep
A rewrite step in this derivation.
termMetrics
Object
true
Derivation
TermMetrics
Metrics for the canonical term produced by this derivation.
from
Object
true
RewriteStep
Term
The term before this rewrite step.
to
Object
true
RewriteStep
Term
The term after this rewrite step.
hasRewriteRule
Object
true
RewriteStep
RewriteRule
The typed rewrite rule applied in this step. Provides a structured reference to a named RewriteRule individual, complementing the string-valued derivation:rule property.
groundedIn
Object
true
RewriteRule
Identity
The algebraic identity that grounds this rewrite rule. Links a RewriteRule to the op:Identity individual that justifies its application.
stepCount
Datatype
true
TermMetrics
nonNegativeInteger
The total number of rewrite steps in this derivation.
termSize
Datatype
true
TermMetrics
nonNegativeInteger
The number of nodes in the canonical term's syntax tree.
previousType
Object
true
RefinementStep
TypeDefinition
The type before this refinement step was applied.
appliedConstraint
Object
true
RefinementStep
Constraint
The constraint that was applied in this refinement step.
refinedType
Object
true
RefinementStep
TypeDefinition
The type after this refinement step was applied.
sitesClosed
Datatype
true
RefinementStep
nonNegativeInteger
The number of site coordinates pinned by this refinement step.
stepIndex
Datatype
true
SynthesisStep
nonNegativeInteger
Zero-based sequential index of this step within the synthesis derivation.
addedConstraint
Object
true
SynthesisStep
Constraint
The constraint added in this synthesis step.
signatureBefore
Object
true
SynthesisStep
SynthesisSignature
The constraint nerve signature before this synthesis step.
signatureAfter
Object
true
SynthesisStep
SynthesisSignature
The constraint nerve signature after this synthesis step.
checkpointStep
Object
true
SynthesisCheckpoint
SynthesisStep
The SynthesisStep at which this checkpoint was taken.
checkpointState
Object
true
SynthesisCheckpoint
ConstraintSearchState
The ConstraintSearchState snapshot captured by this checkpoint.
towerCheckpoint
Object
false
TowerCompletenessResolver
SynthesisCheckpoint
Links a TowerCompletenessResolver to a SynthesisCheckpoint issued at each completed step. Cross-namespace bridge property: domain is resolver:TowerCompletenessResolver.
Named Individuals
Name
Type
Comment
CriticalIdentityRule
RewriteRule
The rewrite rule applying the critical identity: neg(bnot(x)) → succ(x). Grounded in op:criticalIdentity.
groundedIn: criticalIdentity
InvolutionRule
RewriteRule
The rewrite rule applying involution cancellation: f(f(x)) → x for any involution f.
AssociativityRule
RewriteRule
The rewrite rule applying associativity to re-bracket nested binary operations.
CommutativityRule
RewriteRule
The rewrite rule applying commutativity to reorder operands of commutative operations.