Algebraic Identities

An algebraic identity is a named equation that holds over the ring substrate Z/(2^n)Z. Each identity is an op:Identity individual in the ontology, paired with a proof:AxiomaticDerivation or proof:ComputationCertificate that certifies it.

Identities are classified by verification domain — the mathematical discipline used to prove them. Domains include Enumerative (exhaustive check at Q0), Algebraic (ring-theoretic derivation), Geometric (metric-space arguments), and others. The chart below shows the distribution across all 624 identities.

Each identity also has a validity scope: Universal (valid at all Witt levels), ParametricLower (valid at level ≥ k), ParametricRange (valid in [k_min, k_max]), or LevelSpecific (valid at exactly one level). See The Ring Substrate for the ring foundation and Proofs, Derivations & Traces for the certification pipeline.

Identity count by verification domain
Identity count distribution across 12 verification domains Algebraic 247 Analytical 67 ArithmeticValuation 5 ComposedAlgebraic 0 Enumerative 4 Geometric 31 IndexTheoretic 34 Pipeline 138 QuantumThermodynamic 7 SuperpositionDomain 4 Thermodynamic 29 Topological 66
IDLabelDomainComment
criticalIdentity Critical Identity Algebraic The foundational theorem of the UOR kernel: neg(bnot(x)) = succ(x) for all x in R_n. This identity links the two involutions (neg and bnot) to the successor operation, making succ derivable from neg and bnot.
AD_1 AD_1 Analytical Addressing bijection: addresses(glyph(d)) = d. Round-trip from datum through glyph and back is identity.
AD_2 AD_2 Analytical Embedding coherence: glyph(ι(addresses(a))) = ι_addr(a). The addressing diagram commutes through embeddings.
R_A1 R_A1 Algebraic Additive associativity: add(x, add(y, z)) = add(add(x, y), z).
R_A2 R_A2 Algebraic Additive identity: add(x, 0) = x.
R_A3 R_A3 Algebraic Additive inverse: add(x, neg(x)) = 0.
R_A4 R_A4 Algebraic Additive commutativity: add(x, y) = add(y, x).
R_A5 R_A5 Algebraic Subtraction definition: sub(x, y) = add(x, neg(y)).
R_A6 R_A6 Algebraic Negation involution: neg(neg(x)) = x.
R_M1 R_M1 Algebraic Multiplicative associativity: mul(x, mul(y, z)) = mul(mul(x, y), z).
R_M2 R_M2 Algebraic Multiplicative identity: mul(x, 1) = x.
R_M3 R_M3 Algebraic Multiplicative commutativity: mul(x, y) = mul(y, x).
R_M4 R_M4 Algebraic Distributivity: mul(x, add(y, z)) = add(mul(x, y), mul(x, z)).
R_M5 R_M5 Algebraic Annihilation: mul(x, 0) = 0.
B_1 B_1 Algebraic XOR associativity: xor(x, xor(y, z)) = xor(xor(x, y), z).
B_2 B_2 Algebraic XOR identity: xor(x, 0) = x.
B_3 B_3 Algebraic XOR self-inverse: xor(x, x) = 0.
B_4 B_4 Algebraic AND associativity: and(x, and(y, z)) = and(and(x, y), z).
B_5 B_5 Algebraic AND identity: and(x, 2^n - 1) = x.
B_6 B_6 Algebraic AND annihilation: and(x, 0) = 0.
B_7 B_7 Algebraic OR associativity: or(x, or(y, z)) = or(or(x, y), z).
B_8 B_8 Algebraic OR identity: or(x, 0) = x.
B_9 B_9 Algebraic Absorption: and(x, or(x, y)) = x.
B_10 B_10 Algebraic AND distributes over OR: and(x, or(y, z)) = or(and(x, y), and(x, z)).
B_11 B_11 Algebraic De Morgan 1: bnot(and(x, y)) = or(bnot(x), bnot(y)).
B_12 B_12 Algebraic De Morgan 2: bnot(or(x, y)) = and(bnot(x), bnot(y)).
B_13 B_13 Algebraic Bnot involution: bnot(bnot(x)) = x.
X_1 X_1 Algebraic Neg via subtraction: neg(x) = sub(0, x).
X_2 X_2 Algebraic Complement via XOR: bnot(x) = xor(x, 2^n - 1).
X_3 X_3 Algebraic Succ via addition: succ(x) = add(x, 1).
X_4 X_4 Algebraic Pred via subtraction: pred(x) = sub(x, 1).
X_5 X_5 Algebraic Neg-bnot bridge: neg(x) = add(bnot(x), 1).
X_6 X_6 Algebraic Complement predecessor: bnot(x) = pred(neg(x)).
X_7 X_7 Algebraic XOR-add bridge: xor(x, y) = add(x, y) - 2 * and(x, y) (in Z before mod).
D_1 D_1 Algebraic Rotation order: succ^[2^n](x) = x.
D_3 D_3 Algebraic Conjugation: neg(succ(neg(x))) = pred(x).
D_4 D_4 Algebraic Reverse composition: bnot(neg(x)) = pred(x).
D_5 D_5 Algebraic Group closure: D_[2^n] = [succ^k, neg ∘ succ^k : 0 ≤ k < 2^n].
U_1 U_1 Algebraic Unit group decomposition: R_n× ≅ Z/2 × Z/2^[n-2] for n ≥ 3.
U_2 U_2 Algebraic Unit group special cases: R_1× ≅ [1]; R_2× ≅ Z/2.
U_3 U_3 Algebraic Multiplicative order: ord(u) = lcm(ord((-1)^a), ord(3^b)).
U_4 U_4 Algebraic Resonance period: ord_g(2) divides φ(g).
U_5 U_5 Algebraic Step formula derivation: step_g = 2 * ((g - (2^n mod g)) mod g) + 1.
AG_1 AG_1 Algebraic Scaling not dihedral: μ_u ∉ D_[2^n] for u ≠ ±1.
AG_2 AG_2 Algebraic Affine group: Aff(R_n) = R_n× ⋉ R_n.
AG_3 AG_3 Algebraic Affine group order: |Aff(R_n)| = 2^[2n-1].
AG_4 AG_4 Algebraic Subgroup inclusion: D_[2^n] ⊂ Aff(R_n) with u ∈ [±1].
CA_1 CA_1 Algebraic Addition decomposition: add(x,y)_k = xor(x_k, xor(y_k, c_k(x,y))).
CA_2 CA_2 Algebraic Carry recurrence: c_[k+1](x,y) = or(and(x_k,y_k), and(xor(x_k,y_k), c_k)).
CA_3 CA_3 Algebraic Carry commutativity: c(x, y) = c(y, x).
CA_4 CA_4 Algebraic Zero carry: c(x, 0) = 0 at all positions.
CA_5 CA_5 Algebraic Negation carry: c(x, neg(x))_k = 1 for k > v_2(x).
CA_6 CA_6 Algebraic Carry-incompatibility link: d_Δ(x, y) > 0 iff ∃ k : c_k(x,y) = 1.
C_1 C_1 Algebraic Constraint pin union: pins of a composite constraint equal the union of component pins.
C_2 C_2 Algebraic Constraint composition commutativity.
C_3 C_3 Algebraic Constraint composition associativity.
C_4 C_4 Algebraic Constraint composition idempotence.
C_5 C_5 Algebraic Constraint composition identity element.
C_6 C_6 Algebraic Constraint composition annihilator.
CDI CDI Algebraic Constraint-depth invariant: carry complexity of the residue representation equals the type depth.
CL_1 CL_1 Algebraic Constraint quotient lattice isomorphism to power set.
CL_2 CL_2 Algebraic Lattice join equals constraint composition.
CL_3 CL_3 Algebraic Lattice meet pins the intersection of component pins.
CL_4 CL_4 Algebraic Constraint lattice distributivity.
CL_5 CL_5 Algebraic Constraint lattice complement existence.
CM_1 CM_1 Algebraic Constraint redundancy criterion.
CM_2 CM_2 Algebraic Minimal cover via greedy irredundant removal.
CM_3 CM_3 Algebraic Minimum constraint count to cover n sites.
CR_1 CR_1 Algebraic Residue constraint cost is the step formula.
CR_2 CR_2 Algebraic Carry constraint cost is the popcount of the pattern.
CR_3 CR_3 Algebraic Depth constraint cost is sum of residue and carry costs.
CR_4 CR_4 Algebraic Composite constraint cost is subadditive.
CR_5 CR_5 Algebraic Optimal resolution order is increasing cost.
F_1 F_1 Algebraic Site monotonicity: a pinned site cannot be unpinned.
F_2 F_2 Algebraic Site budget upper bound: at most n pin operations to close.
F_3 F_3 Algebraic Site budget conservation: pinned + free = total sites.
F_4 F_4 Algebraic Site budget closure: closed iff all sites pinned.
FL_1 FL_1 Algebraic Site lattice bottom: all sites free.
FL_2 FL_2 Algebraic Site lattice top: all sites pinned.
FL_3 FL_3 Algebraic Site lattice join is union of pinnings.
FL_4 FL_4 Algebraic Site lattice height equals n.
FPM_1 FPM_1 Algebraic Unit partition membership: x is a unit iff site_0(x) = 1 (x is odd).
FPM_2 FPM_2 Algebraic Exterior partition membership: x is exterior iff x is not in the carrier of T.
FPM_3 FPM_3 Algebraic Irreducible partition membership: x is irreducible iff x is not a unit, exterior, or reducible.
FPM_4 FPM_4 Algebraic Reducible partition membership: x is reducible iff x is not a unit, exterior, or irreducible.
FPM_5 FPM_5 Algebraic 2-adic decomposition: every element factors as 2^{v(x)} times an odd unit.
FPM_6 FPM_6 Algebraic Stratum size formula.
FPM_7 FPM_7 Algebraic Base type partition cardinalities.
FS_1 FS_1 Algebraic Site extraction: site_k(x) is the k-th bit of x.
FS_2 FS_2 Algebraic Site 0 is parity.
FS_3 FS_3 Algebraic Progressive site determination: site_k given lower sites determines x mod 2^{k+1}.
FS_4 FS_4 Algebraic Cumulative site determination: sites 0..k together determine x mod 2^{k+1}.
FS_5 FS_5 Algebraic Complete site determination: all n sites determine x uniquely.
FS_6 FS_6 Algebraic Stratum from sites: v_2(x) is the minimum k where site_k(x) = 1.
FS_7 FS_7 Algebraic Depth bound: depth(x) ≤ v_2(x) for irreducible elements.
RE_1 RE_1 Pipeline Resolution strategy equivalence: dihedral, canonical-form, and evaluation resolvers all compute the same partition.
IR_1 IR_1 Pipeline Resolution monotonicity: pinned count never decreases.
IR_2 IR_2 Pipeline Resolution convergence bound: at most n iterations.
IR_3 IR_3 Pipeline Convergence rate definition.
IR_4 IR_4 Pipeline Resolution termination: loop terminates if constraint set spans all sites.
SF_1 SF_1 Pipeline Optimal resolution level for a factor: n ≡ 0 (mod ord_g(2)).
SF_2 SF_2 Pipeline Constraint ordering by step cost: smaller step_g first.
RD_1 RD_1 Pipeline Resolution determinism: same type and constraint sequence yield unique partition.
RD_2 RD_2 Pipeline Order independence: complete constraint sets yield the same partition regardless of order.
SE_1 SE_1 Pipeline Evaluation resolver directly computes the set-theoretic partition.
SE_2 SE_2 Pipeline Dihedral factorization resolver yields the same partition via orbit decomposition.
SE_3 SE_3 Pipeline Canonical form resolver yields the same partition via confluent rewrite.
SE_4 SE_4 Pipeline All three strategies compute the same set-theoretic partition.
OO_1 OO_1 Pipeline Benefit of a constraint is the number of new pins it provides.
OO_2 OO_2 Pipeline Constraint cost is step or popcount depending on type.
OO_3 OO_3 Pipeline Greedy selection maximizes benefit-to-cost ratio.
OO_4 OO_4 Pipeline Greedy approximation achieves (1 − 1/e) ≈ 63% of optimal.
OO_5 OO_5 Pipeline Tiebreaker: prefer vertical (residue) before horizontal (carry).
CB_1 CB_1 Pipeline Minimum convergence rate: 1 site per iteration (worst case).
CB_2 CB_2 Pipeline Maximum convergence rate: n sites in 1 iteration (best case).
CB_3 CB_3 Pipeline Expected residue constraint rate: ⌊log_2(m)⌋ sites per constraint.
CB_4 CB_4 Pipeline Stall detection: convergenceRate < 1 for 2 iterations suggests insufficiency.
CB_5 CB_5 Pipeline Sufficiency criterion: pin union covers all site positions.
CB_6 CB_6 Pipeline Iteration bound for k constraints: at most min(k, n) iterations.
OB_M1 OB_M1 Analytical Ring metric triangle inequality.
OB_M2 OB_M2 Analytical Hamming metric triangle inequality.
OB_M3 OB_M3 Analytical Incompatibility metric is the absolute difference of ring and Hamming metrics.
OB_M4 OB_M4 Analytical Negation preserves ring metric.
OB_M5 OB_M5 Analytical Bitwise complement preserves Hamming metric.
OB_M6 OB_M6 Analytical Successor preserves ring metric but may change Hamming metric.
OB_C1 OB_C1 Analytical Negation-complement commutator is constant 2.
OB_C2 OB_C2 Analytical Negation-translation commutator.
OB_C3 OB_C3 Analytical Complement-XOR commutator is trivial.
OB_H1 OB_H1 Analytical Additive paths have trivial monodromy (abelian ⇒ path-independent).
OB_H2 OB_H2 Analytical Dihedral generator paths have monodromy in D_{2^n}.
OB_H3 OB_H3 Analytical Successor-only closed path winding number.
OB_P1 OB_P1 Analytical Path length is additive under concatenation.
OB_P2 OB_P2 Analytical Total variation is subadditive under concatenation.
OB_P3 OB_P3 Analytical Reduction length is additive under sequential composition.
CT_1 CT_1 Analytical Catastrophe boundaries are powers of 2.
CT_2 CT_2 Analytical Odd prime catastrophe transitions visibility via residue constraints.
CT_3 CT_3 Analytical Catastrophe threshold is normalized step cost.
CT_4 CT_4 Analytical Composite catastrophe threshold is max of component thresholds.
CF_1 CF_1 Analytical Curvature flux is the sum of incompatibility along a path.
CF_2 CF_2 Analytical Resolution cost is bounded below by curvature flux of optimal path.
CF_3 CF_3 Analytical Successor curvature flux: trailing_ones(x) for most x, n−1 at maximum.
CF_4 CF_4 Analytical Total successor curvature flux over R_n equals 2^n − 2.
HG_1 HG_1 Analytical Additive holonomy is trivial (abelian group).
HG_2 HG_2 Analytical Dihedral generator holonomy group is D_{2^n}.
HG_3 HG_3 Analytical Unit multiplication holonomy equals the unit group.
HG_4 HG_4 Analytical Full holonomy group is the affine group.
HG_5 HG_5 Analytical Holonomy group decomposition into dihedral and non-trivial units.
T_C1 T_C1 Geometric Category left identity: compose(id, f) = f.
T_C2 T_C2 Geometric Category right identity: compose(f, id) = f.
T_C3 T_C3 Geometric Category associativity of transform composition.
T_C4 T_C4 Geometric Composability condition: f composesWith g iff target(f) = source(g).
T_I1 T_I1 Geometric Negation is a ring-metric isometry.
T_I2 T_I2 Geometric Bitwise complement is a Hamming-metric isometry.
T_I3 T_I3 Geometric Successor as composed isometries: succ = neg ∘ bnot preserves d_R but not d_H.
T_I4 T_I4 Geometric Ring isometries form a group under composition.
T_I5 T_I5 Geometric CurvatureObservable measures failure of ring isometry to be Hamming isometry.
T_E1 T_E1 Geometric Embedding injectivity.
T_E2 T_E2 Geometric Embedding is a ring homomorphism.
T_E3 T_E3 Geometric Embedding transitivity: composition of embeddings is an embedding.
T_E4 T_E4 Geometric Embedding address coherence: glyph ∘ ι ∘ addresses is well-defined.
T_A1 T_A1 Geometric Dihedral group acts on constraints by transforming them.
T_A2 T_A2 Geometric Dihedral group action on partitions permutes components.
T_A3 T_A3 Geometric Dihedral orbits determine irreducibility boundaries.
T_A4 T_A4 Geometric Fixed points of negation are {0, 2^{n−1}}; bnot has no fixed points.
AU_1 AU_1 Geometric Automorphism group consists of unit multiplications.
AU_2 AU_2 Geometric Automorphism group is isomorphic to the unit group.
AU_3 AU_3 Geometric Automorphism group order is 2^{n−1}.
AU_4 AU_4 Geometric Intersection of automorphism group with dihedral group is {id, neg}.
AU_5 AU_5 Geometric Affine group is generated by D_{2^n} and μ_3.
EF_1 EF_1 Geometric Embedding functor action on morphisms.
EF_2 EF_2 Geometric Embedding functor preserves composition.
EF_3 EF_3 Geometric Embedding functor preserves identities.
EF_4 EF_4 Geometric Embedding functor composition is functorial.
EF_5 EF_5 Geometric Embedding functor preserves ring isometries.
EF_6 EF_6 Geometric Embedding functor maps dihedral subgroup into target dihedral group.
EF_7 EF_7 Geometric Embedding functor maps unit group into target unit group.
AA_1 AA_1 Analytical Braille glyph encoding: 6-bit blocks to Braille characters.
AA_2 AA_2 Analytical Braille XOR homomorphism: Braille encoding commutes with XOR.
AA_3 AA_3 Analytical Braille complement: glyph of bnot(x) is character-wise complement of glyph(x).
AA_4 AA_4 Analytical Addition does not lift to address space: no glyph homomorphism for add.
AA_5 AA_5 Analytical Liftable operations are exactly the Boolean operations.
AA_6 AA_6 Analytical Negation decomposes into liftable bnot and non-liftable succ.
AM_1 AM_1 Analytical Address metric is sum of per-character Hamming distances.
AM_2 AM_2 Analytical Address metric equals Hamming metric on ring elements.
AM_3 AM_3 Analytical Address metric does not preserve ring metric in general.
AM_4 AM_4 Analytical Address incompatibility metric.
TH_1 TH_1 Thermodynamic Entropy of a site budget state.
TH_2 TH_2 Thermodynamic Maximum entropy: unconstrained state has S = n × ln 2.
TH_3 TH_3 Thermodynamic Zero entropy: fully resolved state has S = 0.
TH_4 TH_4 Thermodynamic Landauer bound on total resolution cost.
TH_5 TH_5 Thermodynamic Critical inverse temperature for UOR site system.
TH_6 TH_6 Thermodynamic Constraint application removes entropy; convergence rate equals cooling rate.
TH_7 TH_7 Thermodynamic CatastropheThreshold is the temperature of a partition phase transition.
TH_8 TH_8 Thermodynamic Step formula as free-energy cost of a constraint boundary.
TH_9 TH_9 Thermodynamic Computational hardness maps to type incompleteness (high temperature).
TH_10 TH_10 Thermodynamic Type resolution is measurement; cost ≥ entropy removed.
AR_1 AR_1 Analytical Adiabatic schedule: decreasing freeRank, cost-per-site ordering.
AR_2 AR_2 Analytical Adiabatic cost is sum of constraint costs in optimal order.
AR_3 AR_3 Analytical Adiabatic cost satisfies Landauer bound.
AR_4 AR_4 Analytical Adiabatic efficiency η ≤ 1.
AR_5 AR_5 Analytical Greedy vs adiabatic cost difference: ≤ 5% for n ≤ 16.
PD_1 PD_1 Thermodynamic Phase space definition.
PD_2 PD_2 Thermodynamic Phase boundaries occur where g divides 2^n − 1 or g is a power of 2.
PD_3 PD_3 Thermodynamic Parity boundary divides R_n into equal halves.
PD_4 PD_4 Thermodynamic Resonance lines in the phase diagram.
PD_5 PD_5 Thermodynamic Phase count at level n is at most 2^n (typically O(n)).
RC_1 RC_1 Thermodynamic Reversible pinning stores prior state in ancilla site.
RC_2 RC_2 Thermodynamic Reversible pinning has zero total entropy change.
RC_3 RC_3 Thermodynamic Deferred Landauer cost at ancilla erasure.
RC_4 RC_4 Thermodynamic Reversible total cost equals irreversible total cost (redistributed).
RC_5 RC_5 Thermodynamic Quantum UOR: superposed sites, cost proportional to winning path.
DC_1 DC_1 Analytical Ring derivative: ∂_R f(x) = f(succ(x)) - f(x).
DC_2 DC_2 Analytical Hamming derivative: ∂_H f(x) = f(bnot(x)) - f(x).
DC_3 DC_3 Analytical Hamming derivative of identity: ∂_H id(x) = -(2x + 1) mod 2^n.
DC_4 DC_4 Analytical Commutator from derivatives: [neg, bnot](x) = ∂_R neg(x) - ∂_H neg(x).
DC_5 DC_5 Analytical Carry dependence: the difference ∂_R f - ∂_H f decomposes into carry contributions.
DC_6 DC_6 Analytical Jacobian definition: J_k(x) = ∂_R f_k(x) where f_k = site_k.
DC_7 DC_7 Analytical Top-site anomaly: J_{n-1}(x) may differ from lower sites.
DC_8 DC_8 Analytical Rank-curvature identity: rank(J(x)) = d_H(x, succ(x)) - 1 for generic x.
DC_9 DC_9 Analytical Total curvature from Jacobian: κ(x) = Σ_k J_k(x).
DC_10 DC_10 Analytical Curvature-weighted ordering: optimal next constraint maximizes J_k over free sites.
DC_11 DC_11 Analytical Curvature equipartition: Σ_{x} J_k(x) ≈ (2^n - 2)/n for each k.
HA_1 HA_1 Topological Constraint nerve: N(C) is the simplicial complex on constraints.
HA_2 HA_2 Topological Stall iff non-trivial homology: resolution stalls ⟺ H_k(N(C)) ≠ 0 for some k > 0.
HA_3 HA_3 Topological Betti-entropy theorem: S_residual ≥ Σ_k β_k × ln 2.
IT_2 IT_2 Topological Euler-Poincaré formula for constraint nerve.
IT_3 IT_3 Topological Spectral Euler characteristic.
IT_6 IT_6 Topological Spectral gap bounds convergence rate from below.
IT_7a IT_7a IndexTheoretic, Analytical, Topological UOR index theorem (topological form): total curvature minus Euler characteristic equals residual entropy in bits.
IT_7b IT_7b IndexTheoretic, Analytical, Topological UOR index theorem (entropy-topology duality).
IT_7c IT_7c IndexTheoretic, Analytical, Topological UOR index theorem (spectral cost bound): resolution cost ≥ n - χ(N(C)).
IT_7d IT_7d IndexTheoretic, Analytical, Topological UOR index theorem (completeness criterion): resolution is complete iff χ(N(C)) = n and all Betti numbers vanish.
phi_1 phi_1 Pipeline Ring → Constraints map: negation transforms a residue constraint.
phi_2 phi_2 Pipeline Constraints → Sites map: composition maps to union of site pinnings.
phi_3 phi_3 Pipeline Sites → Partition map: a closed site state determines a unique 4-component partition.
phi_4 phi_4 Pipeline Resolution pipeline: φ₄ = φ₃ ∘ φ₂ ∘ φ₁ is the composite resolution map.
phi_5 phi_5 Pipeline Operations → Observables map: negation preserves d_R, may change d_H.
phi_6 phi_6 Pipeline Observables → Refinement map: observables on a state yield a refinement suggestion.
psi_1 psi_1 Topological ψ_1: Constraints → SimplicialComplex (nerve construction). Maps a set of constraints to its nerve simplicial complex.
psi_2 psi_2 Topological ψ_2: SimplicialComplex → ChainComplex (chain functor). Maps a simplicial complex to its chain complex.
psi_3 psi_3 Topological ψ_3: ChainComplex → HomologyGroups (homology functor). Computes homology groups from a chain complex.
psi_5 psi_5 Topological ψ_5: ChainComplex → CochainComplex (dualization functor). Dualizes a chain complex to obtain a cochain complex.
psi_6 psi_6 Topological ψ_6: CochainComplex → CohomologyGroups (cohomology functor). Computes cohomology groups from a cochain complex.
surfaceSymmetry Surface Symmetry Pipeline The Surface Symmetry Theorem: the composite P∘Π∘G is a well-typed morphism iff G and P share the same state:Frame F. When the shared-frame condition holds, the output lands in the type-equivalent neighbourhood of the source symbol.
CC_1 CC_1 Pipeline Completeness implies O(1) resolution: a CompleteType T satisfies ∀ x ∈ R_n, resolution(x, T) terminates in O(1).
CC_2 CC_2 Algebraic Completeness is monotone: if T ⊆ T' (T' has more constraints), then completeness(T) implies completeness(T').
CC_3 CC_3 Algebraic Witness composition: concat(W₁, W₂) is a valid audit trail iff W₁.sitesClosed + W₂.sitesClosed = n.
CC_4 CC_4 Pipeline The CompletenessResolver is the unique fixed point of the ψ-pipeline applied to a CompletenessCandidate.
CC_5 CC_5 Topological CompletenessCertificate soundness: cert.verified = true implies χ(N(C)) = n and for all k: β_k = 0.
QL_1 QL_1 Algebraic neg(bnot(x)) = succ(x) holds in Z/(2ⁿ)Z for all n ≥ 1. Universal form of the Critical Identity across all quantum levels.
QL_2 QL_2 Algebraic The dihedral group D_{2ⁿ} generated by neg and bnot has order 2ⁿ⁺¹ for all n ≥ 1.
QL_3 QL_3 Thermodynamic The reduction distribution P(j) = 2^{-j} is the Boltzmann distribution at β* = ln 2 for all n ≥ 1.
QL_4 QL_4 Algebraic The site budget of a PrimitiveType at quantum level n is exactly n (one site per bit).
QL_5 QL_5 Pipeline Resolution complexity for a CompleteType is O(1) for all n ≥ 1.
QL_6 QL_6 Algebraic Content addressing is a bijection for all n ≥ 1 (AD_1/AD_2 universality).
QL_7 QL_7 Topological The ψ-pipeline produces a valid ChainComplex for any ConstrainedType at any quantum level n ≥ 1.
GR_1 GR_1 Algebraic Binding monotonicity: freeRank(B_{i+1}) ≤ freeRank(B_i) for all i in a Session.
GR_2 GR_2 Pipeline Binding soundness: a Binding b is sound iff b.datum resolves under b.constraint in O(1).
GR_3 GR_3 Algebraic Session convergence: a Session S converges iff there exists i such that freeRank(B_i) = 0.
GR_4 GR_4 Algebraic Context reset isolation: bindings in C_fresh are independent of bindings in C_prior after a SessionBoundary.
GR_5 GR_5 Algebraic Contradiction detection: ContradictionBoundary fires iff there exist bindings b, b' with the same address, different datum, under the same constraint.
TS_1 TS_1 Pipeline Nerve realisability: for any target (χ*, β₀* = 1, β_k* = 0 for k ≥ 1) with χ* ≤ n, there exists a ConstrainedType T over R_n whose constraint nerve realises the target.
TS_2 TS_2 Pipeline Minimal basis bound: for the IT_7d target (χ* = n, all β* = 0), the MinimalConstraintBasis has size exactly n (one constraint per site position). No redundant constraints exist in the minimal basis.
TS_3 TS_3 Pipeline Synthesis monotonicity: adding a constraint to a synthesis candidate never decreases the Euler characteristic of the resulting nerve (χ is monotone non-decreasing under constraint addition).
TS_4 TS_4 Pipeline Synthesis convergence: the TypeSynthesisResolver terminates for any realisable target in at most n constraint additions (for n-site types).
TS_5 TS_5 Pipeline Synthesis–certification duality: a SynthesizedType T achieves the IT_7d target if and only if the CompletenessResolver certifies T as a CompleteType. The forward ψ-pipeline and the inverse TypeSynthesisResolver are dual computations.
TS_6 TS_6 Pipeline Jacobian-guided synthesis efficiency: using the Jacobian (DC_10) to select the next constraint reduces the expected number of synthesis steps from O(n²) (uninformed) to O(n log n) (Jacobian-guided).
TS_7 TS_7 Pipeline Unreachable signatures: a Betti profile with β₀ = 0 is unreachable by any non-empty ConstrainedType — the nerve of a non-empty constraint set is always connected (β₀ ≥ 1).
WLS_1 WLS_1 IndexTheoretic Lift unobstructedness criterion: WittLift T' is a CompleteType iff the spectral sequence E_r^{p,q} collapses at E_2 (d_2 = 0 and all higher differentials zero).
WLS_2 WLS_2 IndexTheoretic Obstruction localisation: a non-trivial LiftObstruction is localised to a specific site at bit position n+1. The obstruction class lives in H²(N(C(T))) and is killed by adding one constraint involving the new site.
WLS_3 WLS_3 IndexTheoretic Monotone lifting for trivially obstructed types: if T is a CompleteType at Q_n and its constraint set is closed under the Q_{n+1} extension map, then T' is a CompleteType at Q_{n+1} with basisSize(T') = basisSize(T) + 1.
WLS_4 WLS_4 IndexTheoretic Spectral sequence convergence bound: for constraint configurations of homological depth d (H_k(N(C(T))) = 0 for k > d), the spectral sequence converges by page E_{d+2}.
WLS_5 WLS_5 IndexTheoretic Universal identity preservation: every op:universallyValid identity holds in ℤ/(2^{n+1})ℤ with the lifted constraint set. The lift does not invalidate any certified universal identity.
WLS_6 WLS_6 IndexTheoretic ψ-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.
MN_1 MN_1 Topological Holonomy group containment: HolonomyGroup(T) ≤ D_{2^n} for all ConstrainedTypes T over R_n. The holonomy group is always a subgroup of the full dihedral group.
MN_2 MN_2 Topological Additive flatness (extends OB_H1): if all constraints in T are additive (ResidueConstraint or DepthConstraint type), then HolonomyGroup(T) = {id} — T is a FlatType.
MN_3 MN_3 Topological Dihedral generation: if T contains both a neg-related and a bnot-related constraint in a common closed path, then HolonomyGroup(T) = D_{2^n} — T has full dihedral holonomy.
MN_4 MN_4 Topological Holonomy-Betti implication: HolonomyGroup(T) ≠ {id} ⟹ β₁(N(C(T))) ≥ 1. Non-trivial monodromy requires a topological loop. (Converse is false: β₁ ≥ 1 does not imply non-trivial holonomy.)
MN_5 MN_5 Topological CompleteType holonomy: a CompleteType (IT_7d: χ = n, all β = 0) has trivial holonomy. IT_7d implies FlatType because IT_7d requires β₁ = 0, which by MN_4 implies trivial monodromy.
MN_6 MN_6 Topological Monodromy composition: if p₁ and p₂ are closed constraint paths, then monodromy(p₁ · p₂) = monodromy(p₁) · monodromy(p₂) in D_{2^n} (group homomorphism from loops to dihedral elements).
MN_7 MN_7 Topological TwistedType obstruction class: the monodromy of a TwistedType contributes a non-zero class to H²(N(C(T')); ℤ/2ℤ) where T' is any WittLift of T. TwistedTypes always have non-trivial lift obstructions.
PT_1 PT_1 Algebraic Product type site additivity: siteBudget(A × B) = siteBudget(A) + siteBudget(B).
PT_2 PT_2 Topological Product type partition product: partition(A × B) = partition(A) ⊗ partition(B).
PT_3 PT_3 IndexTheoretic Product type Euler additivity: χ(N(C(A × B))) = χ(N(C(A))) + χ(N(C(B))).
PT_4 PT_4 Thermodynamic Product type entropy additivity: S(A × B) = S(A) + S(B).
ST_1 ST_1 Algebraic Sum type site budget: siteBudget(A + B) = max(siteBudget(A), siteBudget(B)).
ST_2 ST_2 Thermodynamic Sum type entropy: S(A + B) = ln 2 + max(S(A), S(B)).
GS_1 GS_1 Thermodynamic Context temperature: T_ctx(C) = freeRank(C) × ln 2 / n.
GS_2 GS_2 Algebraic Grounding degree: σ(C) = (n − freeRank(C)) / n.
GS_3 GS_3 Algebraic Grounding monotonicity: σ(B_{i+1}) ≥ σ(B_i) for all i in a Session.
GS_4 GS_4 Thermodynamic Ground state equivalence: σ(C) = 1 ↔ freeRank(C) = 0 ↔ S(C) = 0 ↔ T_ctx(C) = 0.
GS_5 GS_5 Pipeline O(1) resolution guarantee: freeRank(C) = 0 ∧ q.address ∈ bindings(C) → stepCount(q, C) = 0.
GS_6 GS_6 Algebraic Pre-reduction of effective budget: effectiveBudget(q, C) = max(0, siteBudget(q.type) − |pinnedSites(C) ∩ q.siteSet|).
GS_7 GS_7 Thermodynamic Thermodynamic cooling cost: Cost_saturation(C) = n × k_B T × ln 2.
MS_1 MS_1 Pipeline Connectivity lower bound: β₀(N(C)) ≥ 1 for all non-empty C.
MS_2 MS_2 Algebraic Euler capacity ceiling: χ(N(C)) ≤ n for all C at quantum level n.
MS_3 MS_3 Topological Betti monotonicity under addition: χ(N(C + c)) ≥ χ(N(C)) for any constraint c added to C.
MS_4 MS_4 Pipeline Level-relative achievability: a signature achievable at quantum level n remains achievable at level n+1.
MS_5 MS_5 Pipeline Empirical completeness convergence: verified SynthesisSignature individuals converge to the exact morphospace boundary.
GD_1 GD_1 Analytical Geodesic condition: a ComputationTrace is a geodesic iff its steps are AR_1-ordered and each step selects the constraint maximising J_k over free sites (DC_10).
GD_2 GD_2 Thermodynamic Geodesic entropy bound: ΔS_step(i) = ln 2 for every step i of a geodesic trace.
GD_3 GD_3 Thermodynamic Total geodesic cost: Cost_geodesic(T) = freeRank_initial × k_B T ln 2 = TH_4.
GD_4 GD_4 Analytical Geodesic uniqueness up to step-order equivalence: all geodesics for the same ConstrainedType share stepCount and constraint set.
GD_5 GD_5 Pipeline Subgeodesic detectability: a trace is sub-geodesic iff ∃ step i where J_k(step_i) < max_{free sites} J_k(state_i).
QM_1 QM_1 QuantumThermodynamic Von Neumann–Landauer bridge: S_vonNeumann(ψ) = Cost_Landauer(collapse(ψ)).
QM_2 QM_2 Topological Measurement as site topology change: projective collapse on a SuperposedSiteState is topologically equivalent to applying a ResidueConstraint that pins the collapsed site.
QM_3 QM_3 QuantumThermodynamic Superposition entropy bound: 0 ≤ S_vN(ψ) ≤ ln 2 for any single-site SuperposedSiteState.
QM_4 QM_4 Algebraic Collapse idempotence: collapse(collapse(ψ)) = collapse(ψ). Measurement on an already-collapsed state is a no-op.
QM_5 QM_5 QuantumThermodynamic Amplitude normalization (Born rule): the sum of squared amplitudes equals 1 for any well-formed SuperposedSiteState.
RC_6 RC_6 SuperpositionDomain Amplitude renormalization: a SuperposedSiteState can always be normalized to satisfy QM_5.
FPM_8 FPM_8 Enumerative Partition exhaustiveness: the four component cardinalities sum to the ring size.
FPM_9 FPM_9 Algebraic Exterior membership criterion: x is exterior iff x is not in the carrier of T.
MN_8 MN_8 Topological Holonomy classification covering: every ConstrainedType with a computed holonomy group is either flat or twisted, not both.
QL_8 QL_8 Algebraic Witt level chain inverse: wittLevelPredecessor is the left inverse of nextWittLevel.
D_7 D_7 Geometric Dihedral composition rule: (rᵃ sᵖ)(rᵇ sᵠ) = r^(a + (-1)ᵖ b mod 2ⁿ) s^(p xor q).
SP_1 SP_1 SuperpositionDomain Classical embedding: superposition resolution of a classical (non-superposed) datum reduces to classical resolution.
SP_2 SP_2 QuantumThermodynamic Collapse–resolve commutativity: collapsing then resolving classically equals resolving in superposition then collapsing.
SP_3 SP_3 SuperpositionDomain Amplitude preservation: the SuperpositionResolver preserves the normalized amplitude vector during ψ-pipeline traversal.
SP_4 SP_4 QuantumThermodynamic Born rule outcome probability: the probability of collapsing to site k equals the squared amplitude of that site.
PT_2a PT_2a Algebraic Product type partition tensor: the partition of a product type is the tensor product of the component partitions.
PT_2b PT_2b Algebraic Sum type partition coproduct: the partition of a sum type is the coproduct of the variant partitions.
GD_6 GD_6 Analytical Geodesic predicate decomposition: a trace is geodesic iff it is both AR_1-ordered and DC_10-selected.
WT_1 WT_1 IndexTheoretic LiftChain(Q_j, Q_k) is valid CompleteType tower iff every chainStep WittLift has trivial or resolved LiftObstruction.
WT_2 WT_2 IndexTheoretic Obstruction count bound: the number of non-trivial LiftObstructions in a chain is at most the chain length.
WT_3 WT_3 IndexTheoretic Resolved basis size formula: the basis size at Q_k equals basisSize(Q_j) + chainLength + obstructionResolutionCost.
WT_4 WT_4 Topological Flat tower characterization: isFlat(chain) iff obstructionCount = 0 iff HolonomyGroup trivial at every step.
WT_5 WT_5 IndexTheoretic LiftChainCertificate existence: a CompleteType at Q_k satisfies IT_7d with a witness chain.
WT_6 WT_6 IndexTheoretic Single-step reduction: QT_3 with chainLength=1 and cost=0 reduces to QLS_3.
WT_7 WT_7 IndexTheoretic Flat chain basis size: for flat chains, resolvedBasisSize(Q_k) = basisSize(Q_j) + (k - j).
CC_PINS CC_PINS Algebraic Carry-constraint site-pinning map: pinsSites(CarryConstraint(p)) equals the set of bit positions where p has a 1 plus the first-zero stopping position.
CC_COST_SITE CC_COST_SITE Enumerative Carry-constraint cost-to-site count: the number of sites pinned by a CarryConstraint equals popcount plus one for the stopping position.
jsat_RR jsat_RR Algebraic CRT joint satisfiability: two ResidueConstraints are jointly satisfiable iff the gcd of their moduli divides the difference of their residues.
jsat_CR jsat_CR Algebraic Carry-residue joint satisfiability: a CarryConstraint and ResidueConstraint are jointly satisfiable iff the carry-pinned sites are compatible with the residue class.
jsat_CC jsat_CC Enumerative Carry-carry joint satisfiability: two CarryConstraints are jointly satisfiable iff their bit-patterns have no conflicting positions.
D_8 D_8 Algebraic Dihedral inverse formula: the inverse of r^a s^p in D_(2^n) is r^(-(−1)^p a mod 2^n) s^p.
D_9 D_9 Algebraic Dihedral reflection order: every reflection element r^k s^1 in D_(2^n) has order 2.
EXP_1 EXP_1 Algebraic Monotone carrier characterization: a ConstrainedType has an upward-closed carrier iff every ResidueConstraint has residue = modulus - 1 and no CarryConstraint or DepthConstraint appears.
EXP_2 EXP_2 Enumerative Monotone constraint count: the number of expressible monotone ConstrainedTypes at quantum level Q_n is 2^n, corresponding to the principal filter count.
EXP_3 EXP_3 Algebraic SumType carrier semantics: the carrier of a SumType is the coproduct (disjoint union) of component carriers, not the set-theoretic union.
ST_3 ST_3 IndexTheoretic SumType Euler characteristic additivity: for a SumType with topologically disjoint component nerves, the Euler characteristic is additive.
ST_4 ST_4 Topological SumType Betti number additivity: for disjoint component nerves, all Betti numbers are additive.
ST_5 ST_5 IndexTheoretic SumType completeness transfer: a SumType A+B is CompleteType iff both A and B are CompleteType and they have equal quantum levels.
TS_8 TS_8 Pipeline Betti-1 minimum constraint count: the minimum number of constraints needed to achieve first Betti number beta_1 = k in the constraint nerve is 2k + 1.
TS_9 TS_9 Pipeline TypeSynthesisResolver termination: the resolver terminates in at most 2^n steps for any target signature at quantum level Q_n, returning either a ConstrainedType or a ForbiddenSignature certificate.
TS_10 TS_10 Algebraic ForbiddenSignature membership criterion: a topological signature is a ForbiddenSignature iff no ConstrainedType with at most n constraints realises it at quantum level Q_n.
WT_8 WT_8 IndexTheoretic ObstructionChain length bound: the length of the ObstructionChain from Q_j to Q_k is at most (k-j) times C(basisSize(Q_j), 3).
WT_9 WT_9 Pipeline TowerCompletenessResolver termination: the resolver terminates for any finite LiftChain within the QT_8 bound, producing a CompleteType certificate or a bounded ObstructionChain.
COEFF_1 COEFF_1 Algebraic Standard coefficient ring: the coefficient ring for all psi-pipeline cohomology computations in uor.foundation is Z/2Z, consistent with MN_7.
GO_1 GO_1 Topological GluingObstruction feedback: given a GluingObstruction class in H^1(N(C)), the killing RefinementSuggestion adds a constraint whose pinned sites contain the intersection of the cycle-generating pair.
GR_6 GR_6 Algebraic Grounding re-entry free rank: for a session at full grounding, a new query q has freeRank equal to the number of q's site coordinates not already bound.
GR_7 GR_7 Algebraic Grounding degree degradation: after re-entry with query q, the grounding degree becomes min(current sigma, 1 - freeRank(q)/n).
QM_6 QM_6 SuperpositionDomain Amplitude index set characterization: the amplitude index set of a SuperposedSiteState over ConstrainedType T at Q_n is the set of monotone pinning trajectories consistent with T's constraints.
CIC_1 CIC_1 Pipeline Certificate issuance: every valid Transform admits a TransformCertificate attesting correct source-to-target mapping.
CIC_2 CIC_2 Geometric Certificate issuance: every metric-preserving Transform admits an IsometryCertificate attesting distance preservation.
CIC_3 CIC_3 Algebraic Certificate issuance: every involutive operation f where f(f(x)) = x admits an InvolutionCertificate.
CIC_4 CIC_4 Thermodynamic Certificate issuance: full saturation (σ = 1, freeRank = 0) admits a GroundingCertificate.
CIC_5 CIC_5 Pipeline Certificate issuance: an AR_1-ordered and DC_10-selected trace admits a GeodesicCertificate.
CIC_6 CIC_6 QuantumThermodynamic Certificate issuance: a MeasurementEvent verifying the von Neumann–Landauer bridge at β* = ln 2 admits a MeasurementCertificate.
CIC_7 CIC_7 QuantumThermodynamic Certificate issuance: a MeasurementEvent verifying P(outcome k) = |α_k|² admits a BornRuleVerification certificate.
GC_1 GC_1 Pipeline Certificate issuance: shared-frame grounding that lands in the type-equivalent neighbourhood admits a GroundingCertificate.
GR_8 GR_8 Algebraic Session composition validity: compose(S_A, S_B) is valid at Q_k iff all pinned-site intersections agree at every tower level Q_0 through Q_k.
GR_9 GR_9 Algebraic ContextLease disjointness: two distinct leases on the same SharedContext have non-overlapping site sets.
GR_10 GR_10 Algebraic ExecutionPolicy confluence: different execution policies on the same pending query set produce the same final resolved state (Church-Rosser for session resolution).
MC_1 MC_1 Algebraic Lease partition conserves total budget: the sum of freeRank over all leases equals the SharedContext freeRank.
MC_2 MC_2 Algebraic Per-lease binding monotonicity: within a leased sub-domain, freeRank decreases monotonically (SR_1 restricted to lease).
MC_3 MC_3 Algebraic General composition freeRank via inclusion-exclusion.
MC_4 MC_4 Algebraic Disjoint-lease composition is additive: the intersection term vanishes when leases are site-disjoint (SR_9).
MC_5 MC_5 Algebraic Policy-invariant final binding set: different execution policies produce identical SiteBinding records.
MC_6 MC_6 Algebraic Full lease coverage implies composed saturation: k sessions on disjoint covering leases, each locally converged, produce a GroundedContext via composition.
MC_7 MC_7 Pipeline Distributed O(1) resolution: a query against a composed GroundedContext resolves in zero steps.
MC_8 MC_8 Algebraic Parallelism bound: per-session resolution work is bounded by lease size, not by total site count n.
WC_1 WC_1 Algebraic Witt coordinate identification: the bit coordinates (x_0, …, x_[n−1]) of x ∈ Z/(2ⁿ)Z are exactly its Witt coordinates under the canonical isomorphism W_n(F_2) ≅ Z/(2ⁿ)Z.
WC_2 WC_2 Algebraic Witt sum correction equals carry: the k-th Witt addition polynomial correction term S_k − x_k − y_k (mod 2) is exactly the carry c_k(x,y).
WC_3 WC_3 Algebraic Carry recurrence is the Witt polynomial recurrence: CA_2 implements the ghost equation for S_[k+1] at p=2.
WC_4 WC_4 Algebraic The δ-correction at level k equals the single-level carry c_[k+1](x,y). Each application of δ divides by 2, consuming one unit of 2-adic valuation.
WC_5 WC_5 IndexTheoretic LiftObstruction is equivalent to δ-nonvanishing: a nontrivial LiftObstruction at Q_[k+1] means δ_k ≠ 0 for some element pair.
WC_6 WC_6 Analytical Metric discrepancy equals Witt defect: d_Δ(x,y) > 0 iff the ghost map correction (carry) is nonzero.
WC_7 WC_7 Algebraic D_1 is the Witt truncation order relation: succ^[2ⁿ](x) = x is the group relation r^[2ⁿ] = 1 in the Witt-Burnside ring of D_[2∞].
WC_8 WC_8 Algebraic D_3 is the Witt-Burnside conjugation relation: neg(succ(neg(x))) = pred(x) is srs = r⁻¹ in the pro-dihedral group.
WC_9 WC_9 Algebraic D_4 is a Witt-Burnside reflection composition: bnot(neg(x)) = pred(x) is the product of two reflections yielding inverse rotation.
WC_10 WC_10 Algebraic The δ-ring Frobenius lift on W_n(F_2) is the identity map because F_2 is a perfect field of characteristic 2 (a² = a for a ∈ F_2).
WC_11 WC_11 Algebraic The Verschiebung on W_n(F_2) is multiplication by 2: V(x) = 2x = add(x,x). This is a coordinate shift with zero Witt defect.
WC_12 WC_12 Algebraic The δ-operator on W_n(F_2) is the squaring defect divided by 2: δ(x) = (x − mul(x,x)) / 2. Expressible entirely in existing op/ primitives (sub, mul, arithmetic right shift).
OA_1 OA_1 ArithmeticValuation Ostrowski product formula at p=2: |2|_2 · |2|_∞ = 1. The 2-adic and Archimedean absolute values of 2 are multiplicative inverses.
OA_2 OA_2 ArithmeticValuation Crossing cost equals ln 2: the Archimedean image of one unit of 2-adic valuation, under the product formula, is ln 2 nats.
OA_3 OA_3 ArithmeticValuation QM_1 grounding: the Landauer cost β* = ln 2 is the crossing cost from OA_2, derived from the prime p=2 that structures the Witt tower.
OA_4 OA_4 ArithmeticValuation Born rule bridge (conditional on amplitude rationality): P(outcome k) = |α_k|_∞², where |·|_∞ is the Archimedean image of the 2-adic amplitude via the product formula.
OA_5 OA_5 ArithmeticValuation Entropy per δ-level equals the crossing cost: each application of the δ-operator (division by 2) costs ln 2 nats in the Archimedean completion, which is the per-bit Landauer cost.
HT_1 HT_1 Topological KanComplex(N(C)) — the constraint nerve satisfies the Kan extension condition for all horns of dimension ≤ d where d is the maximum simplex dimension of N(C).
HT_2 HT_2 Topological Path components of nerve recover β₀: π₀(N(C)) ≅ Z^{β₀} counts the connected components of the constraint configuration.
HT_3 HT_3 Topological MN_6 monodromy is abelianisation of full π₁: the fundamental group π₁(N(C)) surjects onto the HolonomyGroup D_{2^n} via abelianisation.
HT_4 HT_4 Topological Higher homotopy groups vanish above nerve dimension: π_k(N(C)) = 0 for all k > dim(N(C)), because the nerve is a finite CW-complex.
HT_5 HT_5 Topological 1-truncation determines flat/twisted classification: τ_{≤1}(N(C)) captures the holonomy action that distinguishes FlatType from TwistedType.
HT_6 HT_6 IndexTheoretic Trivial k-invariants beyond depth d imply spectral collapse: if κ_k is trivial for all k > d then the spectral sequence collapses at E_{d+2}.
HT_7 HT_7 IndexTheoretic Non-trivial Whitehead product implies lift obstruction: [α, β] ≠ 0 in π_{p+q−1} implies a non-trivial LiftObstruction that Betti numbers alone cannot detect.
HT_8 HT_8 Topological Hurewicz isomorphism for first non-vanishing group: π_k(N(C)) ⊗ Z ≅ H_k(N(C); Z) for the smallest k with π_k ≠ 0, linking homotopy invariants to homology.
psi_7 psi_7 Pipeline ψ_7: KanComplex → PostnikovTower — compute the Postnikov truncations τ_{≤k} for k = 0, 1, …, dim(N(C)).
psi_8 psi_8 Pipeline ψ_8: PostnikovTower → HomotopyGroups — extract the homotopy groups π_k from each truncation stage.
psi_9 psi_9 Pipeline ψ_9: HomotopyGroups → KInvariants — compute the k-invariants κ_k classifying the Postnikov tower.
HP_1 HP_1 Pipeline Pipeline composition: nerve construction + Kan promotion = ψ_7 ∘ ψ_1.
HP_2 HP_2 Pipeline Homotopy extraction agrees with homology on k-skeleton.
HP_3 HP_3 IndexTheoretic k-invariant computation detects QLS_4 convergence.
HP_4 HP_4 Analytical Complexity bound for homotopy type computation.
MD_1 MD_1 Algebraic Moduli space dimension equals basis size of any contained type.
MD_2 MD_2 Algebraic Zeroth deformation cohomology = automorphism group intersected with dihedral group.
MD_3 MD_3 Algebraic First deformation cohomology = tangent space to the moduli space at T.
MD_4 MD_4 IndexTheoretic Second deformation cohomology = LiftObstruction space.
MD_5 MD_5 Topological FlatType stratum has codimension zero in the moduli space.
MD_6 MD_6 Topological TwistedType stratum has codimension at least 1.
MD_7 MD_7 Algebraic VersalDeformation existence is guaranteed when the obstruction space H² vanishes.
MD_8 MD_8 IndexTheoretic A deformation family preserves completeness iff H²(Def(T_t)) = 0 along the entire path.
MD_9 MD_9 IndexTheoretic The site of a ModuliTowerMap at T has dimension 1 when the obstruction is trivial.
MD_10 MD_10 IndexTheoretic The site of a ModuliTowerMap at T is empty iff T is a TwistedType at every level.
MR_1 MR_1 Algebraic ModuliResolver boundary agrees with MorphospaceBoundary.
MR_2 MR_2 Topological StratificationRecord covers every CompleteType in exactly one stratum.
MR_3 MR_3 Analytical ModuliResolver complexity bound.
MR_4 MR_4 Algebraic Achievable signatures correspond to membership in some HolonomyStratum.
CY_1 CY_1 Algebraic Carry generates at site k iff and(x_k, y_k) = 1. Extends CA_1 (addition decomposition) and WC_2 (Witt sum correction).
CY_2 CY_2 Algebraic Carry propagates at site k iff xor(x_k, y_k) = 1 and c_k = 1. Extends CA_2 (carry recurrence) and WC_3 (Witt polynomial recurrence).
CY_3 CY_3 Algebraic Carry kills at site k iff and(x_k, y_k) = 0 and xor(x_k, y_k) = 0. Complement of CY_1 and CY_2.
CY_4 CY_4 Algebraic d_Δ(x,y) = |carryCount(x+y) − hammingDistance(x,y)|. The metric incompatibility IS the discrepancy between carry count and Hamming distance. Strengthens WC_6.
CY_5 CY_5 Algebraic Optimal encoding theorem: the encoding that minimizes Σ d_Δ over observed pairs is the one where the carry chain’s significance hierarchy matches the domain’s dependency structure.
CY_6 CY_6 Algebraic Site ordering theorem: d_Δ is minimized when high-significance sites (upstream in the carry chain) encode the most structurally informative observables.
CY_7 CY_7 Algebraic Carry lookahead: the carry chain for n sites is computable in O(log n) using prefix computation on generate/propagate pairs.
BM_1 BM_1 IndexTheoretic σ(C) = (n − freeRank(C)) / n. The saturation metric is the complement of free site ratio. Derives from SC_2.
BM_2 BM_2 IndexTheoretic χ = Σ(−1)^k β_k. The Euler characteristic of the constraint nerve. Derives from IT_2.
BM_3 BM_3 IndexTheoretic Index theorem: Σκ_k − χ = S_residual / ln 2. Links all six metrics. Derives from IT_7a.
BM_4 BM_4 IndexTheoretic J_k = 0 for pinned sites. The Jacobian vanishes on resolved sites.
BM_5 BM_5 IndexTheoretic d_Δ > 0 iff carry ≠ 0. The metric discrepancy equals the Witt defect. Derives from WC_6.
BM_6 BM_6 IndexTheoretic Metric composition tower: d_Δ → {σ, J_k} → β_k → χ → r. Each metric derives from previous ones.
GL_1 GL_1 Topological σ = lower adjoint evaluated at current type. The saturation metric is the lower adjoint of the Galois connection. Derives from SC_2.
GL_2 GL_2 Topological r = complement of upper adjoint image. The residual freedom is what the type closure does not reach.
GL_3 GL_3 Topological CompleteType = fixpoint of Galois connection, σ=1, r=0. Derives from IT_7d.
GL_4 GL_4 Topological Type refinement = ascending in type lattice = descending in site freedom. The Galois connection reverses order.
NV_1 NV_1 Topological nerve(C₁ ∪ C₂) = nerve(C₁) ∪ nerve(C₂) for disjoint constraint domains.
NV_2 NV_2 Topological Mayer–Vietoris: β_k(C₁ ∪ C₂) computable from parts and intersection.
NV_3 NV_3 Topological Single constraint addition: Δβ_k ∈ {−1, 0, +1} per dimension.
NV_4 NV_4 Topological Constraint accumulation monotonicity: β_k non-increasing under SR_1. Derives from SR_1.
SD_1 SD_1 Algebraic ScalarType grounding: quantize(value, range, bits) produces ring element where d_R reflects value proximity.
SD_2 SD_2 Algebraic SymbolType grounding: argmin_{encoding} Σ d_Δ over observed pairs (CY_5).
SD_3 SD_3 Algebraic SequenceType = free monoid on element type with backbone constraint.
SD_4 SD_4 Algebraic TupleType site count = Σ field site counts, site ordering follows CY_6.
SD_5 SD_5 Algebraic GraphType constraint nerve = graph nerve, β_k equality.
SD_6 SD_6 Algebraic SetType d_Δ invariant under element permutation, D_{2n} symmetry.
SD_7 SD_7 Algebraic TreeType β_1=0, β_0=1 topological constraints.
SD_8 SD_8 Algebraic TableType = SequenceType(TupleType(S)), functorial decomposition.
DD_1 DD_1 ComposedAlgebraic Dispatch determinism: same query and same registry always yield the same resolver.
DD_2 DD_2 ComposedAlgebraic Dispatch coverage: every query in the registry domain has a matching resolver.
PI_1 PI_1 ComposedAlgebraic Inference idempotence: ι(ι(s,C),C) = ι(s,C) on GroundedContext.
PI_2 PI_2 ComposedAlgebraic Inference soundness: ι(s,C) resolves to a type consistent with C.
PI_3 PI_3 ComposedAlgebraic Inference composition: ι = P ∘ Π ∘ G (references phi_4).
PI_4 PI_4 ComposedAlgebraic Inference complexity: O(n) worst case, O(1) on CompleteType.
PI_5 PI_5 ComposedAlgebraic Inference coherence: roundTrip(P(Π(G(s)))) = s.
PA_1 PA_1 ComposedAlgebraic Accumulation permutation invariance: accumulating bindings in any order yields the same saturated context (derives from SR_10).
PA_2 PA_2 ComposedAlgebraic Accumulation monotonicity: α(b,C) ⊇ C (the context only grows, never loses bindings). Derives from SR_1.
PA_3 PA_3 ComposedAlgebraic Accumulation soundness: α(b,C) preserves all previously satisfied constraints. Derives from SR_2.
PA_4 PA_4 ComposedAlgebraic Accumulation base preservation: α does not modify previously pinned sites.
PA_5 PA_5 ComposedAlgebraic Accumulation identity: α(∅, C) = C.
PL_1 PL_1 ComposedAlgebraic Lease disjointness: partitioned leases have pairwise disjoint site sets (derives from SR_9).
PL_2 PL_2 ComposedAlgebraic Lease conservation: union of all leases equals the original shared context (derives from MC_1).
PL_3 PL_3 ComposedAlgebraic Lease coverage: every site in the shared context appears in exactly one lease (derives from MC_6).
PK_1 PK_1 ComposedAlgebraic Composition validity: κ(S₁,S₂) is a valid session if S₁,S₂ have disjoint leases (derives from SR_8).
PK_2 PK_2 ComposedAlgebraic Distributed resolution: resolving in κ(S₁,S₂) equals resolving in S₁ or S₂ independently (derives from MC_7).
PP_1 PP_1 ComposedAlgebraic Pipeline unification: κ(λₖ(α*(ι(s,·))),C) = resolve(s,C). The full composed pipeline equals the top-level resolution function.
PE_1 PE_1 Pipeline Stage 0 initializes state vector to 1.
PE_2 PE_2 Pipeline Stage 1 dispatches resolver (δ selects).
PE_3 PE_3 Pipeline Stage 2 produces valid ring address (G grounds).
PE_4 PE_4 Pipeline Stage 3 resolves constraints (Π terminates).
PE_5 PE_5 Pipeline Stage 4 accumulates without contradiction (α consistent).
PE_6 PE_6 Pipeline Stage 5 extracts coherent output (P projects).
PE_7 PE_7 Pipeline Full pipeline is the composition PE_6 ∘ … ∘ PE_1.
PM_1 PM_1 Pipeline Phase rotation Ω^k at stage k.
PM_2 PM_2 Pipeline Phase gate checks Ω^k at boundary.
PM_3 PM_3 Pipeline Gate failure triggers complex conjugate rollback.
PM_4 PM_4 Pipeline Rollback is involutory: (z̄)̄ = z.
PM_5 PM_5 Pipeline Epoch boundary preserves saturation.
PM_6 PM_6 Pipeline Service window provides base context.
PM_7 PM_7 Pipeline Machine is deterministic given initial state.
ER_1 ER_1 Pipeline Stage transition requires guard satisfaction.
ER_2 ER_2 Pipeline Effect application is atomic.
ER_3 ER_3 Pipeline Guard evaluation is side-effect-free.
ER_4 ER_4 Pipeline Effect composition is order-independent within a stage.
EA_1 EA_1 Pipeline Epoch boundary resets free sites.
EA_2 EA_2 Pipeline Grounding carries across epochs.
EA_3 EA_3 Pipeline Service window bounds context size.
EA_4 EA_4 Pipeline Epoch admits one datum or one refinement pass.
OE_1 OE_1 Pipeline Adjacent stages with compatible guards may fuse.
OE_2 OE_2 Pipeline Independent effects commute.
OE_3 OE_3 Pipeline Disjoint leases parallelize.
OE_4a OE_4a Pipeline Stage fusion preserves semantics.
OE_4b OE_4b Pipeline Effect commutation preserves outcome.
OE_4c OE_4c Pipeline Lease parallelism preserves coverage.
CS_1 CS_1 Pipeline Each stage has bounded cost.
CS_2 CS_2 Pipeline Pipeline cost = sum of stage costs.
CS_3 CS_3 Pipeline Rollback cost is at most forward cost.
CS_4 CS_4 Pipeline Preflight cost is O(1).
CS_5 CS_5 Pipeline Total reduction cost bounded by n × stage_max_cost.
CS_6 CS_6 Pipeline Budget solvency rejection: a CompileUnit whose declared thermodynamicBudget is strictly less than the Landauer minimum (bitsWidth(Q_k) × ln 2) is rejected at the BudgetSolvencyCheck preflight.
CS_7 CS_7 Algebraic Unit address identity: the unitAddress of a CompileUnit is the u:Element computed by hashing the canonical byte serialization of the root term’s transitive closure.
FA_1 FA_1 Pipeline Every pending query eventually reaches a stage gate.
FA_2 FA_2 Pipeline No starvation under bounded epoch admission.
FA_3 FA_3 Pipeline Fair lease allocation under disjoint composition.
SW_1 SW_1 Pipeline Service window bounds context memory.
SW_2 SW_2 Pipeline Window slide preserves saturation invariant.
SW_3 SW_3 Pipeline Evicted epochs release lease resources.
SW_4 SW_4 Pipeline Window size ≥ 1 (non-empty).
LS_1 LS_1 Pipeline Suspended lease preserves pinned state.
LS_2 LS_2 Pipeline Lease expiry triggers resource release.
LS_3 LS_3 Pipeline Checkpoint restore is idempotent.
LS_4 LS_4 Pipeline Active → Suspended → Active round-trip preserves state.
TJ_1 TJ_1 Pipeline AllOrNothing transaction rolls back on any failure.
TJ_2 TJ_2 Pipeline BestEffort transaction commits partial results.
TJ_3 TJ_3 Pipeline Transaction atomicity within a single epoch.
AP_1 AP_1 Pipeline Partial saturation is monotonically non-decreasing across stages.
AP_2 AP_2 Pipeline Approximation quality improves with additional epochs.
AP_3 AP_3 Pipeline Deferred queries are eventually processed or explicitly dropped.
EC_1 EC_1 Topological Ω⁶ = −1: reduction converges in 6 stages (phase half-turn).
EC_2 EC_2 Topological Complex conjugate rollback involutory: (z̄)̄ = z.
EC_3 EC_3 Topological Pairwise convergence: commutator converges to identity.
EC_4 EC_4 Topological Triple convergence: associator converges to zero.
EC_4a EC_4a Topological Associator monotonicity: associator norm non-increasing.
EC_4b EC_4b Topological Associator finiteness: reaches 0 in bounded steps.
EC_4c EC_4c Topological Associator vanishing implies associativity on resolved site space.
EC_5 EC_5 Topological Adams termination: no convergence level beyond L3_Self.
DA_1 DA_1 Algebraic Cayley-Dickson R→C: adjoin i with i²=−1, conjugation (a+bi)* = a−bi.
DA_2 DA_2 Algebraic Cayley-Dickson C→H: adjoin j with j²=−1, ij=k, ji=−k, k²=−1.
DA_3 DA_3 Algebraic Cayley-Dickson H→O: adjoin l, Fano plane products, associativity fails.
DA_4 DA_4 Algebraic Adams theorem: no normed division algebra of dimension 16 exists.
DA_5 DA_5 Algebraic Convergence level k lives in k-th division algebra: L0 in R, L1 in C, L2 in H, L3 in O.
DA_6 DA_6 Algebraic Commutator vanishes iff algebra at that level is commutative.
DA_7 DA_7 Algebraic Associator vanishes iff algebra at that level is associative.
IN_1 IN_1 ComposedAlgebraic d_Δ as interaction cost between entities.
IN_2 IN_2 ComposedAlgebraic Disjoint leases imply commutator = 0.
IN_3 IN_3 ComposedAlgebraic Shared sites imply commutator > 0.
IN_4 IN_4 ComposedAlgebraic SR_8 implies negotiation converges (commutator decreases monotonically).
IN_5 IN_5 ComposedAlgebraic Convergent negotiation selects U(1) ⊂ SU(2).
IN_6 IN_6 ComposedAlgebraic Outcome space of pairwise negotiation is S².
IN_7 IN_7 ComposedAlgebraic Mutual modeling selects H ⊂ O.
IN_8 IN_8 ComposedAlgebraic Interaction nerve β_k bounds coupling complexity at dimension k.
IN_9 IN_9 ComposedAlgebraic β_2(nerve) × max_disagreement bounds associator norm.
AS_1 AS_1 ComposedAlgebraic δ-ι-κ non-associativity: δ reads registry written by κ.
AS_2 AS_2 ComposedAlgebraic ι-α-λ non-associativity: λ reads lease state written by α.
AS_3 AS_3 ComposedAlgebraic λ-κ-δ non-associativity: δ reads state written by κ.
AS_4 AS_4 ComposedAlgebraic Root cause: non-associativity from read-write interleaving through mediating entity.
MO_1 MO_1 Algebraic Unit law: I ⊗ A ≅ A ≅ A ⊗ I.
MO_2 MO_2 Algebraic Associativity: (A⊗B)⊗C ≅ A⊗(B⊗C).
MO_3 MO_3 Algebraic Certificate composition: cert(A⊗B) contains cert(A) and cert(B).
MO_4 MO_4 Algebraic σ(A⊗B) ≥ max(σ(A), σ(B)): sequential composition does not lose saturation.
MO_5 MO_5 Algebraic r(A⊗B) ≤ min(r(A), r(B)): residual can only shrink under sequential composition.
OP_1 OP_1 Algebraic Site additivity: siteCount(F(G)) = F.sites + Σ_i G_i.sites.
OP_2 OP_2 Algebraic Grounding distributivity: grounding(F(G(x))) = F.ground(G.ground(x)).
OP_3 OP_3 Algebraic d_Δ decomposition: d_Δ(F(G)) decomposes into outer + inner d_Δ.
OP_4 OP_4 Algebraic Table(Tuple(fields)): standard tabular data structure decomposition.
OP_5 OP_5 Algebraic Tree(leaves): standard hierarchical data structure (AST, XML, JSON).
FX_1 FX_1 Algebraic Pinning decrements free count by exactly 1.
FX_2 FX_2 Algebraic Unbinding increments free count by exactly 1.
FX_3 FX_3 Algebraic Phase effects preserve site budget.
FX_4 FX_4 Algebraic Disjoint effects commute.
FX_5 FX_5 Algebraic Composite free-count delta is additive.
FX_6 FX_6 Algebraic Every ReversibleEffect has an inverse (PinningEffect⁻¹ = UnbindingEffect on same site, PhaseEffect⁻¹ = conjugate phase).
FX_7 FX_7 Pipeline External effects must match their declared shape.
PR_1 PR_1 Pipeline Every predicate is total: evaluation terminates for all inputs.
PR_2 PR_2 Pipeline Every predicate is pure: evaluation does not modify state.
PR_3 PR_3 Pipeline Exhaustive + mutually exclusive dispatch is deterministic.
PR_4 PR_4 Pipeline Match evaluation is deterministic given exhaustive, ordered arms.
PR_5 PR_5 Pipeline Stage transition requires typed guard satisfaction.
CG_1 CG_1 Pipeline Entry guard must be satisfied to enter a stage.
CG_2 CG_2 Pipeline Exit guard must be satisfied, then the stage effect is applied.
DIS_1 DIS_1 Pipeline The root resolver dispatch table is exhaustive and mutually exclusive over all TypeDefinitions.
DIS_2 DIS_2 Pipeline Resolver dispatch is deterministic for every type.
PAR_1 PAR_1 Algebraic Disjoint parallel computations commute: A ⊗ B = B ⊗ A when site targets are disjoint.
PAR_2 PAR_2 Algebraic Parallel free-count deltas are additive.
PAR_3 PAR_3 Algebraic Partitioning is exhaustive: component cardinalities sum to total site budget.
PAR_4 PAR_4 Algebraic All interleavings of disjoint parallel computations yield the same final context.
PAR_5 PAR_5 Pipeline Parallel certificate is the conjunction of component certificates plus disjointness.
HO_1 HO_1 Algebraic A ComputationDatum’s ring value is the content hash of its certificate.
HO_2 HO_2 Pipeline Application preserves certification.
HO_3 HO_3 Pipeline Composition certification requires both components certified and type-compatible.
HO_4 HO_4 Algebraic Fully saturated partial application equals direct application.
STR_1 STR_1 Pipeline Every epoch terminates: the reduction within each epoch reaches convergence angle π.
STR_2 STR_2 Pipeline Grounding preservation across epoch boundaries.
STR_3 STR_3 Pipeline Every finite prefix computes in finite time.
STR_4 STR_4 Algebraic The first epoch starts from the unfold seed context.
STR_5 STR_5 Algebraic Each subsequent epoch starts from the previous boundary’s continuation context.
STR_6 STR_6 Algebraic Lease expiry at an epoch boundary returns claimed sites to the next epoch’s linear budget.
FLR_1 FLR_1 Algebraic Every partial computation produces exactly one of Success or Failure.
FLR_2 FLR_2 Pipeline A total computation always succeeds.
FLR_3 FLR_3 Algebraic Sequential failure propagation: if A fails, B is not evaluated.
FLR_4 FLR_4 Algebraic Parallel failure independence: one component’s failure does not prevent the other’s success.
FLR_5 FLR_5 Pipeline Recovery produces a new ComputationResult.
FLR_6 FLR_6 Pipeline The reduction’s existing rollback mechanism is a Recovery whose effect is the conjugate phase rotation.
LN_1 LN_1 Algebraic In a linear trace, every site is targeted exactly once. Total effect count equals site budget.
LN_2 LN_2 Algebraic After a LinearEffect, the target site is pinned.
LN_3 LN_3 Algebraic A consumed LinearSite cannot be targeted again.
LN_4 LN_4 Algebraic Lease allocation decrements the linear budget by the lease cardinality.
LN_5 LN_5 Pipeline Lease expiry returns claimed sites to the budget.
LN_6 LN_6 Topological Every geodesic trace is a linear trace.
SB_1 SB_1 Algebraic Subtyping is constraint superset: more constraints = more specific.
SB_2 SB_2 Algebraic Subtype has fewer valid resolutions.
SB_3 SB_3 Topological The constraint nerve of the supertype is a sub-complex of the subtype’s nerve.
SB_4 SB_4 Algebraic Covariance preserves inclusion.
SB_5 SB_5 Algebraic Contravariance reverses inclusion.
SB_6 SB_6 Algebraic Lattice depth equals site budget.
BR_1 BR_1 Algebraic Every recursive step strictly decreases the descent measure.
BR_2 BR_2 Pipeline Recursion depth is bounded by the initial measure value.
BR_3 BR_3 Pipeline Every bounded recursion terminates.
BR_4 BR_4 Algebraic Structural recursion’s measure is the input type’s structural size.
BR_5 BR_5 Pipeline The base predicate is satisfied exactly when the measure reaches zero.
RG_1 RG_1 Topological The working set is determined by the constraint nerve and the stage’s site targets.
RG_2 RG_2 Analytical All addresses within a region are within the region’s diameter under the chosen metric.
RG_3 RG_3 Algebraic Total working set size is bounded by the addressable space at the quantum level.
RG_4 RG_4 Pipeline The resolver at stage k accesses only addresses within its working set.
IO_1 IO_1 Pipeline Ingested data conforms to the source’s declared type.
IO_2 IO_2 Pipeline Emitted data conforms to the sink’s declared type.
IO_3 IO_3 Pipeline Every ingestion through a source produces a valid ring datum via grounding.
IO_4 IO_4 Pipeline Every emission through a sink produces a valid surface symbol via projection.
IO_5 IO_5 Algebraic Every boundary effect touches at least one site.
boundarySquaredZero boundarySquaredZero Topological ∂² = 0: the boundary of a boundary is zero.
psi_4 psi_4 Topological ψ_4: HomologyGroups → BettiNumbers (extraction functor).
indexBridge indexBridge Topological Index bridge: connects Euler characteristic to alternating Betti sum.
coboundarySquaredZero coboundarySquaredZero Topological δ² = 0: the coboundary of a coboundary is zero.
deRhamDuality deRhamDuality Topological Discrete de Rham duality: H^k ≅ Hom(H_k, R).
sheafCohomologyBridge sheafCohomologyBridge Topological Sheaf cohomology equals simplicial cohomology for constant sheaves.
localGlobalPrinciple localGlobalPrinciple Topological Local-global principle: H^1(K; F) = 0 implies all local sections glue to global sections.