UOR Proofs

IRI
https://uor.foundation/proof/
Prefix
proof:
Space
bridge
Comment
Kernel-produced verification proofs attesting to algebraic properties of UOR objects and operations.

Imports

  • https://uor.foundation/schema/
  • https://uor.foundation/op/
  • https://uor.foundation/derivation/
  • https://uor.foundation/observable/

Classes

NameIRISubclass OfDisjoint WithComment
Proofhttps://uor.foundation/proof/Proofhttp://www.w3.org/2002/07/owl#ThingA kernel-produced attestation that a given algebraic property holds. The root class for all proof types.
CoherenceProofhttps://uor.foundation/proof/CoherenceProofhttps://uor.foundation/proof/ProofA proof of coherence: the type system and ring structure are mutually consistent at a given quantum level.
ComputationCertificatehttps://uor.foundation/proof/ComputationCertificatehttps://uor.foundation/proof/ProofA proof confirmed by exhaustive execution over R_n at a specific quantum level. The kernel ran the identity against all 2^n inputs and observed that it holds. The proof:atWittLevel property records the level; proof:witness links to the WitnessData. CriticalIdentityProof is a subclass of ComputationCertificate.
AxiomaticDerivationhttps://uor.foundation/proof/AxiomaticDerivationhttps://uor.foundation/proof/ProofA proof that follows from previously established axioms or definitions by equational, structural, or topological reasoning. The proof:derivationWitness property links to a derivation:Derivation individual recording the rewrite chain. All pipeline, constraint, observable, and topological identities are AxiomaticDerivations.
CriticalIdentityProofhttps://uor.foundation/proof/CriticalIdentityProofhttps://uor.foundation/proof/ComputationCertificateA proof of the critical identity: neg(bnot(x)) = succ(x) for all x in R_n. This is the foundational theorem of the UOR kernel.
WitnessDatahttps://uor.foundation/proof/WitnessDatahttp://www.w3.org/2002/07/owl#ThingSupporting data for a proof: specific examples, counter-examples checked, or intermediate computation results.
ImpossibilityWitnesshttps://uor.foundation/proof/ImpossibilityWitnesshttps://uor.foundation/proof/ProofA formal witness that a topological signature (χ, β_k) is impossible to achieve for any ConstrainedType. Carries the algebraic reason and the verification domain grounding the impossibility.
MorphospaceRecordhttps://uor.foundation/proof/MorphospaceRecordhttp://www.w3.org/2002/07/owl#ThingA formal record of a morphospace boundary point — either an achievable or forbidden topological signature. Aggregated by MorphospaceBoundary to form the queryable morphospace map.
MorphospaceBoundaryhttps://uor.foundation/proof/MorphospaceBoundaryhttp://www.w3.org/2002/07/owl#ThingAn aggregate of ImpossibilityWitness instances forming the queryable morphospace map. SPARQL over this structure answers achievability queries in O(1).
InductiveProofhttps://uor.foundation/proof/InductiveProofhttps://uor.foundation/proof/ProofA proof by structural induction on the quantum level index k. Carries a base case proof, an inductive step proof, and the minimum k for which the induction holds.
ProofStrategyhttps://uor.foundation/proof/ProofStrategyhttp://www.w3.org/2002/07/owl#ThingA controlled vocabulary of proof methods. Each proof individual carries exactly one strategy from this vocabulary, enabling compilation to verified theorem provers.
DerivationTermhttps://uor.foundation/proof/DerivationTermhttp://www.w3.org/2002/07/owl#ThingRoot AST node for proof construction terms. Distinct from schema:TermExpression which represents mathematical terms; DerivationTerm represents proof constructions (tactic applications, lemma invocations, induction scaffolding).
TacticApplicationhttps://uor.foundation/proof/TacticApplicationhttps://uor.foundation/proof/DerivationTermA proof step applying a named tactic (from ProofStrategy) with arguments. Maps to a Lean4 tactic invocation.
LemmaInvocationhttps://uor.foundation/proof/LemmaInvocationhttps://uor.foundation/proof/DerivationTermA proof step invoking a previously proved identity as a lemma. References the identity via proof:dependsOn.
InductionStephttps://uor.foundation/proof/InductionStephttps://uor.foundation/proof/DerivationTermA proof step performing structural induction: base case derivation, inductive hypothesis, and step derivation.
ComputationStephttps://uor.foundation/proof/ComputationStephttps://uor.foundation/proof/DerivationTermA proof step performing exhaustive computation at a specific quantum level as verification witness.

Properties

NameKindFunctionalDomainRangeComment
verifiedDatatypetruehttps://uor.foundation/proof/Proofhttp://www.w3.org/2001/XMLSchema#booleanWhether this proof has been verified by the kernel.
timestampDatatypetruehttps://uor.foundation/proof/Proofhttp://www.w3.org/2001/XMLSchema#dateTimeThe time at which this proof was produced.
witnessObjectfalsehttps://uor.foundation/proof/Proofhttps://uor.foundation/proof/WitnessDataSupporting witness data for this proof.
criticalIdentityAnnotationtruehttps://uor.foundation/proof/CriticalIdentityProofhttp://www.w3.org/2001/XMLSchema#stringHuman-readable statement of the critical identity proven. E.g., 'neg(bnot(x)) = succ(x) for all x in R_n'. Annotation only — proof:provesIdentity is the typed reference.
xDatatypefalsehttps://uor.foundation/proof/WitnessDatahttp://www.w3.org/2001/XMLSchema#integerA specific input value used as a witness for the critical identity check.
bnot_xDatatypefalsehttps://uor.foundation/proof/WitnessDatahttp://www.w3.org/2001/XMLSchema#integerThe value bnot(x) for a witness x.
neg_bnot_xDatatypefalsehttps://uor.foundation/proof/WitnessDatahttp://www.w3.org/2001/XMLSchema#integerThe value neg(bnot(x)) for a witness x.
succ_xDatatypefalsehttps://uor.foundation/proof/WitnessDatahttp://www.w3.org/2001/XMLSchema#integerThe value succ(x) for a witness x.
holdsDatatypefalsehttps://uor.foundation/proof/WitnessDatahttp://www.w3.org/2001/XMLSchema#booleanWhether the identity neg(bnot(x)) = succ(x) holds for this specific witness.
provesIdentityObjecttruehttps://uor.foundation/proof/Proofhttps://uor.foundation/op/IdentityThe algebraic identity this proof establishes. Provides a canonical object reference alongside the existing proof:criticalIdentity string property, which remains for human readability.
atWittLevelObjecttruehttps://uor.foundation/proof/ComputationCertificatehttps://uor.foundation/schema/WittLevelThe quantum level at which this computation certificate was produced. A ComputationCertificate at schema:Q0 confirms the identity holds for all 256 inputs of R_8. A certificate at schema:Q1 confirms it for all 65,536 inputs of R_16.
wittNoteAnnotationtruehttps://uor.foundation/proof/ComputationCertificatehttp://www.w3.org/2001/XMLSchema#stringHuman-readable quantum level note, e.g. 'n=8, 256 inputs'. Annotation only — proof:atWittLevel is the typed assertion.
universalScopeDatatypetruehttps://uor.foundation/proof/AxiomaticDerivationhttp://www.w3.org/2001/XMLSchema#booleanTrue when this axiomatic derivation holds for all quantum levels by the definition of Z/(2^n)Z. False when the derivation depends on a property specific to a particular ring size. All current AxiomaticDerivation individuals in the spec carry universalScope true.
derivationWitnessObjectfalsehttps://uor.foundation/proof/AxiomaticDerivationhttps://uor.foundation/derivation/DerivationThe derivation chain that witnesses this axiomatic derivation. Links a proof:AxiomaticDerivation to the derivation:Derivation individual recording the rewrite sequence. Optional at the spec level — the conformance suite requires only that the proof individual exists; full derivation chains live in generated artifacts.
forbidsSignatureAnnotationtruehttps://uor.foundation/proof/ImpossibilityWitnesshttp://www.w3.org/2001/XMLSchema#stringThe topological signature (χ, β_k) that this ImpossibilityWitness formally forbids, expressed as a symbolic notation string (e.g., 'β₀ = 0').
impossibilityReasonDatatypetruehttps://uor.foundation/proof/ImpossibilityWitnesshttp://www.w3.org/2001/XMLSchema#stringHuman-readable statement of the algebraic reason the signature is impossible (e.g., 'β₀ = 0 violates MS_1').
impossibilityDomainObjecttruehttps://uor.foundation/proof/ImpossibilityWitnesshttps://uor.foundation/op/VerificationDomainThe verification domain grounding the impossibility (e.g., Pipeline for β₀ = 0, Algebraic for χ > n).
achievabilityStatusObjecttruehttps://uor.foundation/proof/ImpossibilityWitnesshttps://uor.foundation/observable/AchievabilityStatusThe achievability classification of a proof-linked observable signature: Achievable or Forbidden.
verifiedAtLevelObjectfalsehttps://uor.foundation/proof/Proofhttps://uor.foundation/schema/WittLevelThe specific quantum level at which an empirical verification or impossibility witness was established.
morphospaceRecordObjectfalsehttps://uor.foundation/proof/MorphospaceBoundaryhttps://uor.foundation/proof/MorphospaceRecordLinks a MorphospaceBoundary to one of its constituent MorphospaceRecord individuals.
boundaryTypeObjecttruehttps://uor.foundation/proof/MorphospaceRecordhttps://uor.foundation/observable/AchievabilityStatusWhether this MorphospaceRecord represents an impossibility boundary (from below) or an achievability boundary (from above).
baseCaseObjecttruehttps://uor.foundation/proof/InductiveProofhttps://uor.foundation/proof/ProofThe proof that the claim holds at the base level k_0.
inductiveStepObjecttruehttps://uor.foundation/proof/InductiveProofhttps://uor.foundation/proof/ProofThe proof that if the claim holds at Q_k, it holds at Q_{k+1}.
validForKAtLeastDatatypetruehttps://uor.foundation/proof/InductiveProofhttp://www.w3.org/2001/XMLSchema#nonNegativeIntegerThe minimum k for which the induction is valid.
strategyObjecttruehttps://uor.foundation/proof/Proofhttps://uor.foundation/proof/ProofStrategyThe proof method from the ProofStrategy controlled vocabulary. Determines the compilation target (e.g., `by ring`, `by simp`, `by induction`).
dependsOnObjectfalsehttps://uor.foundation/proof/Proofhttps://uor.foundation/op/IdentityAn identity that this proof depends on as a lemma. Forms the proof dependency DAG. Leaf proofs (provable from definitions alone) have no dependsOn assertions.
formalDerivationObjecttruehttps://uor.foundation/proof/Proofhttps://uor.foundation/proof/DerivationTermThe formal proof construction term: a DerivationTerm AST node encoding the tactic script, lemma chain, or induction scaffold that constitutes the proof.

Named Individuals

NameTypePropertiesComment
RingAxiomhttps://uor.foundation/proof/ProofStrategy—Follows from ZMod ring axioms. Lean4 tactic: `by ring`.
DecideQ0https://uor.foundation/proof/ProofStrategy—Decidable at Q0 by exhaustive evaluation. Lean4: `by native_decide`.
BitwiseInductionhttps://uor.foundation/proof/ProofStrategy—Induction on bit width n. Lean4: `by induction n`.
GroupPresentationhttps://uor.foundation/proof/ProofStrategy—From dihedral group presentation. Lean4: `by group`.
Simplificationhttps://uor.foundation/proof/ProofStrategy—By simplification with cited lemmas. Lean4: `by simp [lemmalist]`.
ChineseRemainderhttps://uor.foundation/proof/ProofStrategy—By Chinese Remainder Theorem. Lean4: `by exact ZMod.chineseRemainder ...`.
EulerPoincarehttps://uor.foundation/proof/ProofStrategy—By Euler-Poincare formula applied to the constraint nerve.
ProductFormulahttps://uor.foundation/proof/ProofStrategy—By Ostrowski product formula or derived valuation arguments.
Compositionhttps://uor.foundation/proof/ProofStrategy—By composing proofs of sub-identities. Lean4: `by exact ...`.
Contradictionhttps://uor.foundation/proof/ProofStrategy—By deriving contradiction for impossibility witnesses. Lean4: `by contradiction`.
Computationhttps://uor.foundation/proof/ProofStrategy—By computation at a specified quantum level. Lean4: `by native_decide`.
prf_criticalIdentityhttps://uor.foundation/proof/CriticalIdentityProof
  • provesIdentity: https://uor.foundation/op/criticalIdentity
  • atWittLevel: https://uor.foundation/schema/W8
  • verified: true
  • strategy: https://uor.foundation/proof/Computation
Computation certificate for the critical identity neg(bnot(x)) = succ(x) at Q0.
prf_criticalIdentity_axiomatichttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/criticalIdentity
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of the critical identity neg(bnot(x)) = succ(x). Holds at all quantum levels.
prf_phi_1https://uor.foundation/proof/ComputationCertificate
  • provesIdentity: https://uor.foundation/op/phi_1
  • atWittLevel: https://uor.foundation/schema/W8
  • verified: true
  • strategy: https://uor.foundation/proof/Computation
Computation certificate for phi_1 at Q0.
prf_phi_2https://uor.foundation/proof/ComputationCertificate
  • provesIdentity: https://uor.foundation/op/phi_2
  • atWittLevel: https://uor.foundation/schema/W8
  • verified: true
  • strategy: https://uor.foundation/proof/Computation
Computation certificate for phi_2 at Q0.
prf_phi_3https://uor.foundation/proof/ComputationCertificate
  • provesIdentity: https://uor.foundation/op/phi_3
  • atWittLevel: https://uor.foundation/schema/W8
  • verified: true
  • strategy: https://uor.foundation/proof/Computation
Computation certificate for phi_3 at Q0.
prf_phi_4https://uor.foundation/proof/ComputationCertificate
  • provesIdentity: https://uor.foundation/op/phi_4
  • atWittLevel: https://uor.foundation/schema/W8
  • verified: true
  • strategy: https://uor.foundation/proof/Computation
Computation certificate for phi_4 at Q0.
prf_phi_5https://uor.foundation/proof/ComputationCertificate
  • provesIdentity: https://uor.foundation/op/phi_5
  • atWittLevel: https://uor.foundation/schema/W8
  • verified: true
  • strategy: https://uor.foundation/proof/Computation
Computation certificate for phi_5 at Q0.
prf_phi_6https://uor.foundation/proof/ComputationCertificate
  • provesIdentity: https://uor.foundation/op/phi_6
  • atWittLevel: https://uor.foundation/schema/W8
  • verified: true
  • strategy: https://uor.foundation/proof/Computation
Computation certificate for phi_6 at Q0.
prf_AD_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AD_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AD_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AD_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AD_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AD_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_R_A1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/R_A1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of R_A1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_R_A2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/R_A2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of R_A2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_R_A3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/R_A3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of R_A3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_R_A4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/R_A4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of R_A4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_R_A5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/R_A5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of R_A5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_R_A6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/R_A6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of R_A6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_R_M1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/R_M1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of R_M1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_R_M2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/R_M2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of R_M2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_R_M3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/R_M3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of R_M3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_R_M4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/R_M4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of R_M4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_R_M5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/R_M5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of R_M5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_7. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_8. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_9https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_9
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_9. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_10https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_10
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_10. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_11https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_11
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_11. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_12https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_12
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_12. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_B_13https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/B_13
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of B_13. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_X_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/X_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of X_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_X_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/X_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of X_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_X_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/X_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of X_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_X_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/X_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of X_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_X_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/X_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of X_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_X_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/X_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of X_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_X_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/X_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of X_7. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_D_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/D_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of D_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_D_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/D_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of D_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_D_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/D_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of D_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_D_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/D_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of D_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_U_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/U_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ChineseRemainder
Axiomatic derivation of U_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_U_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/U_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ChineseRemainder
Axiomatic derivation of U_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_U_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/U_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ChineseRemainder
Axiomatic derivation of U_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_U_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/U_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ChineseRemainder
Axiomatic derivation of U_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_U_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/U_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ChineseRemainder
Axiomatic derivation of U_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AG_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AG_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of AG_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AG_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AG_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of AG_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AG_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AG_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of AG_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AG_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AG_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of AG_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CA_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CA_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CA_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CA_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CA_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CA_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CA_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CA_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CA_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CA_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CA_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CA_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CA_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CA_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CA_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CA_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CA_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CA_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_C_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/C_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of C_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_C_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/C_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of C_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_C_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/C_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of C_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_C_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/C_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of C_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_C_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/C_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of C_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_C_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/C_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of C_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CDIhttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CDI
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CDI. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CL_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CL_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CL_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CL_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CL_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CL_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CL_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CL_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CL_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CL_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CL_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CL_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CL_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CL_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CL_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CM_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CM_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CM_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CM_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CM_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CM_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CM_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CM_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CM_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CR_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CR_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CR_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CR_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CR_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CR_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CR_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CR_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CR_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CR_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CR_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CR_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CR_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CR_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CR_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_F_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/F_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of F_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_F_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/F_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of F_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_F_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/F_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of F_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_F_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/F_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of F_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FL_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FL_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FL_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FL_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FL_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FL_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FL_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FL_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FL_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FL_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FL_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FL_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FPM_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FPM_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FPM_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FPM_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FPM_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FPM_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FPM_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FPM_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FPM_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FPM_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FPM_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FPM_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FPM_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FPM_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FPM_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FPM_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FPM_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FPM_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FPM_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FPM_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FPM_7. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FS_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FS_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FS_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FS_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FS_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FS_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FS_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FS_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FS_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FS_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FS_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FS_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FS_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FS_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FS_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FS_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FS_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FS_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_FS_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FS_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FS_7. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_RE_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RE_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of RE_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_IR_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IR_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of IR_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_IR_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IR_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of IR_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_IR_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IR_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of IR_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_IR_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IR_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of IR_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_SF_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SF_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of SF_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_SF_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SF_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of SF_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_RD_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RD_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of RD_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_RD_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RD_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of RD_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_SE_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SE_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of SE_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_SE_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SE_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of SE_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_SE_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SE_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of SE_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_SE_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SE_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of SE_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OO_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OO_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OO_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OO_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OO_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OO_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OO_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OO_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OO_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OO_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OO_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OO_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OO_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OO_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OO_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CB_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CB_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CB_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CB_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CB_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CB_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CB_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CB_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CB_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CB_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CB_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CB_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CB_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CB_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CB_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CB_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CB_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of CB_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_M1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_M1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_M1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_M2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_M2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_M2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_M3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_M3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_M3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_M4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_M4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_M4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_M5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_M5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_M5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_M6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_M6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_M6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_C1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_C1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_C1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_C2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_C2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_C2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_C3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_C3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_C3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_H1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_H1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_H1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_H2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_H2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_H2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_H3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_H3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_H3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_P1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_P1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_P1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_P2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_P2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_P2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_OB_P3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OB_P3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OB_P3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CT_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CT_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CT_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CT_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CT_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CT_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CT_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CT_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CT_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CT_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CT_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CT_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CF_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CF_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CF_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CF_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CF_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CF_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CF_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CF_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CF_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_CF_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CF_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CF_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_HG_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HG_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of HG_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_HG_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HG_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of HG_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_HG_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HG_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of HG_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_HG_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HG_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of HG_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_HG_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HG_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of HG_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_C1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_C1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_C1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_C2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_C2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_C2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_C3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_C3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_C3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_C4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_C4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_C4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_I1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_I1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_I1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_I2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_I2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_I2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_I3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_I3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_I3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_I4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_I4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_I4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_I5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_I5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_I5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_E1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_E1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_E1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_E2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_E2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_E2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_E3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_E3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_E3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_E4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_E4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_E4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_A1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_A1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_A1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_A2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_A2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_A2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_A3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_A3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_A3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_T_A4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/T_A4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of T_A4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AU_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AU_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of AU_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AU_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AU_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of AU_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AU_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AU_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of AU_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AU_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AU_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of AU_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AU_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AU_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of AU_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_EF_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EF_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of EF_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_EF_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EF_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of EF_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_EF_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EF_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of EF_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_EF_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EF_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of EF_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_EF_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EF_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of EF_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_EF_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EF_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of EF_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_EF_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EF_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Axiomatic derivation of EF_7. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AA_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AA_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AA_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AA_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AA_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AA_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AA_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AA_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AA_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AA_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AA_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AA_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AA_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AA_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AA_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AA_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AA_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AA_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AM_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AM_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AM_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AM_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AM_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AM_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AM_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AM_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AM_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AM_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AM_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AM_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_TH_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TH_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TH_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_TH_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TH_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TH_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_TH_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TH_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TH_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_TH_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TH_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TH_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_TH_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TH_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TH_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_TH_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TH_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TH_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_TH_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TH_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TH_7. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_TH_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TH_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TH_8. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_TH_9https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TH_9
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TH_9. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_TH_10https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TH_10
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TH_10. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AR_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AR_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AR_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AR_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AR_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AR_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AR_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AR_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AR_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AR_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AR_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AR_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_AR_5https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/AR_5
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_AR_5_base
  • inductiveStep: https://uor.foundation/proof/prf_AR_5_step
  • validForKAtLeast: 0
  • strategy: https://uor.foundation/proof/BitwiseInduction
Inductive proof of AR_5: greedy vs adiabatic cost difference is at most 5%. Base case at Q0 by exhaustive evaluation; inductive step by QLS_5 (identity preservation under lift).
prf_PD_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PD_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PD_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_PD_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PD_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PD_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_PD_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PD_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PD_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_PD_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PD_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PD_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_PD_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PD_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PD_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_RC_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RC_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of RC_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_RC_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RC_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of RC_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_RC_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RC_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of RC_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_RC_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RC_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of RC_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_RC_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RC_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of RC_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_DC_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DC_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DC_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_DC_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DC_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DC_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_DC_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DC_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DC_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_DC_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DC_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DC_4. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_DC_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DC_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DC_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_DC_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DC_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DC_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_DC_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DC_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DC_7. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_DC_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DC_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DC_8. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_DC_9https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DC_9
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DC_9. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_DC_10https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DC_10
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DC_10. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_DC_11https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DC_11
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DC_11. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_HA_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HA_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of HA_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_HA_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HA_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of HA_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_HA_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HA_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of HA_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_IT_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IT_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of IT_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_IT_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IT_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of IT_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_IT_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IT_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of IT_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_IT_7ahttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IT_7a
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IT_7a. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_IT_7bhttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IT_7b
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IT_7b. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_IT_7chttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IT_7c
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IT_7c. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_IT_7dhttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IT_7d
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IT_7d. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_psi_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/psi_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of psi_1. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_psi_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/psi_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of psi_2. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_psi_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/psi_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of psi_3. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_psi_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/psi_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of psi_5. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_psi_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/psi_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of psi_6. Holds at all quantum levels by definition of Z/(2^n)Z.
prf_boundarySquaredZerohttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/homology/boundarySquaredZero
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of homology:boundarySquaredZero. Holds at all quantum levels by topological reasoning.
prf_psi_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/homology/psi_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of homology:psi_4. Holds at all quantum levels by topological reasoning.
prf_indexBridgehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/homology/indexBridge
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of homology:indexBridge. Holds at all quantum levels by topological reasoning.
prf_coboundarySquaredZerohttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/cohomology/coboundarySquaredZero
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of cohomology:coboundarySquaredZero. Holds at all quantum levels by topological reasoning.
prf_deRhamDualityhttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/cohomology/deRhamDuality
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of cohomology:deRhamDuality. Holds at all quantum levels by topological reasoning.
prf_sheafCohomologyBridgehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/cohomology/sheafCohomologyBridge
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of cohomology:sheafCohomologyBridge. Holds at all quantum levels by topological reasoning.
prf_localGlobalPrinciplehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/cohomology/localGlobalPrinciple
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of cohomology:localGlobalPrinciple. Holds at all quantum levels by topological reasoning.
prf_surfaceSymmetryhttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/surfaceSymmetry
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of the Surface Symmetry Theorem. Holds at all quantum levels: the composite P∘Π∘G is a well-typed morphism whenever G and P share the same state:Frame. Follows from the definition of the shared-frame condition and the type-equivalence algebra.
prf_CC_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CC_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof that a CompleteType T satisfies: resolution(x, T) terminates in O(1) for all x ∈ R_n. Follows from IT_7d: when χ(N(C)) = n and all β_k = 0, the resolver has no topological obstructions.
prf_CC_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CC_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof that the ψ pipeline is monotone: each constraint application cannot increase the site deficit. Derived from the definition of the partition refinement order.
prf_CC_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CC_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof that a CompletenessCertificate implies CompleteType: the certificate attestation is only issued when IT_7d holds, by construction of the CompletenessResolver.
prf_CC_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CC_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof that the CompletenessAuditTrail witnessCount equals the number of CompletenessWitness records in the trail. Structural invariant of the audit accumulation protocol.
prf_CC_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CC_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof that the CechNerve nerve computation is deterministic: the same constraint set always produces the same nerve topology. Follows from the nerve functor being a functor (functoriality).
prf_QL_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QL_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Universal proof that neg(bnot(x)) = succ(x) in Z/(2^n)Z for all n ≥ 1. Derived symbolically from ring axioms: bnot is bitwise complement, neg is two's complement negation, succ is modular increment. The critical identity in universal form.
prf_QL_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QL_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Universal proof that the ring carrier set size is exactly 2^n for all n ≥ 1. Follows from the definition of Z/(2^n)Z.
prf_QL_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QL_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Universal proof that Landauer erasure cost scales as n × k_B T ln 2 at quantum level n. Follows from the thermodynamic interpretation: each bit erased from an n-bit ring costs k_B T ln 2.
prf_QL_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QL_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Universal proof that the dihedral group D_{2^n} action on Z/(2^n)Z is faithful for all n ≥ 1. The stabilizer of any element is trivial under the full dihedral action.
prf_QL_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QL_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Universal proof that canonical form rewriting terminates at all quantum levels. The rewriting system is terminating by lexicographic descent on the term complexity measure.
prf_QL_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QL_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Universal proof that the completeness criterion χ(N(C)) = n generalizes to all quantum levels. Derived from the definition of the nerve construction and the Euler characteristic formula for simplicial complexes.
prf_QL_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QL_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Universal proof of the ring topology Euler characteristic identity: χ = 1 − n at quantum level n. Derived from the CW decomposition of the n-dimensional torus formed by the ring's cyclic group action.
prf_GR_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GR_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of binding monotonicity: freeRank(B_{i+1}) ≤ freeRank(B_i) for all i in a Session. Follows from the definition of the BindingAccumulator: each appended binding either pins sites or is a no-op; it never frees them.
prf_GR_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GR_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof that the empty session is the identity element of the session algebra: freeRank(B_0) = total site space. The empty accumulator has no pinned sites by definition.
prf_GR_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GR_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of session convergence: a session terminates iff freeRank reaches its minimum (the maximum pinned by the given constraint set). Follows from the compactness of the site space and monotonicity.
prf_GR_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GR_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof that disjoint bindings compose without site conflict: if two bindings address disjoint site sets, their composition is well-defined and their union is also a valid binding.
prf_GR_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GR_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of contradiction detection correctness: ContradictionBoundary fires iff there exist bindings b, b' in the same Context with the same address, different datum, and same constraint. This is the minimal condition for type contradiction.
prf_TS_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TS_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of nerve realisability: for any target profile with χ* ≤ n and β₀* = 1, there exists a ConstrainedType whose constraint nerve realises the target. Follows from the constructive synthesis algorithm.
prf_TS_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TS_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of minimal basis bound: the MinimalConstraintBasis for the IT_7d target has size exactly n. Follows from the site-by-site construction and the minimality criterion.
prf_TS_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TS_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of synthesis monotonicity: adding a constraint never decreases the Euler characteristic of the constraint nerve. Follows from the nerve inclusion principle.
prf_TS_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TS_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of synthesis convergence: the TypeSynthesisResolver terminates in at most n steps. Follows from monotonicity (TS_3) and the finite site budget bound.
prf_TS_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TS_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of synthesis-certification duality: a SynthesizedType achieves IT_7d iff the CompletenessResolver certifies it as CompleteType. The duality follows from the shared topological criterion.
prf_TS_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TS_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of Jacobian-guided synthesis efficiency: the Jacobian oracle reduces expected steps from O(n²) to O(n log n). Follows from the information content of the Jacobian at each synthesis step.
prf_TS_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TS_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of unreachable signatures: β₀ = 0 is unreachable by any non-empty ConstrainedType. Follows from the nerve connectedness of non-empty constraint sets.
prf_WLS_1https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/WLS_1
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_WLS_1_base
  • inductiveStep: https://uor.foundation/proof/prf_WLS_6
  • validForKAtLeast: 0
  • strategy: https://uor.foundation/proof/BitwiseInduction
Proof of lift unobstructedness criterion: WittLift T' is CompleteType iff the spectral sequence collapses at E_2. Follows from the Leray spectral sequence of the quantum level extension.
prf_WLS_2https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/WLS_2
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_WLS_2_base
  • inductiveStep: https://uor.foundation/proof/prf_WLS_2_step
  • validForKAtLeast: 0
  • strategy: https://uor.foundation/proof/BitwiseInduction
Proof of obstruction localisation: a non-trivial LiftObstruction is localised to a specific site at bit position n+1. Follows from the local-to-global structure of the constraint nerve.
prf_WLS_3https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/WLS_3
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_WLS_3_base
  • inductiveStep: https://uor.foundation/proof/prf_WLS_3_step
  • validForKAtLeast: 0
  • strategy: https://uor.foundation/proof/BitwiseInduction
Proof of monotone lifting: basisSize(T') = basisSize(T) + 1 for trivially obstructed lifts. Follows from the minimal basis construction at Q_{n+1}.
prf_WLS_4https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/WLS_4
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_WLS_4_base
  • inductiveStep: https://uor.foundation/proof/prf_WLS_4_step
  • validForKAtLeast: 0
  • strategy: https://uor.foundation/proof/BitwiseInduction
Proof of spectral sequence convergence bound: the spectral sequence converges by page E_{d+2} for depth-d configurations. Follows from the filtration length of the constraint nerve chain complex.
prf_WLS_5https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/WLS_5
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_WLS_5_base
  • inductiveStep: https://uor.foundation/proof/prf_WLS_6
  • validForKAtLeast: 0
  • strategy: https://uor.foundation/proof/BitwiseInduction
Proof of universal identity preservation under quantum lifts: every universallyValid identity holds in the lifted ring. Follows from the universal validity definition and ring extension properties.
prf_WLS_6https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/WLS_6
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_WLS_6_base
  • inductiveStep: https://uor.foundation/proof/prf_WLS_6_step
  • validForKAtLeast: 0
  • strategy: https://uor.foundation/proof/BitwiseInduction
Proof of ψ-pipeline universality for quantum lifts: the ψ-pipeline produces a valid ChainComplex for any WittLift. Follows from the functorial construction of the chain complex.
prf_WLS_1_basehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WLS_1
  • universalScope: false
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Base case for QLS_1 at Q0: lift unobstructedness holds trivially for 8-bit rings where the constraint nerve is contractible.
prf_WLS_2_basehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WLS_2
  • universalScope: false
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Base case for QLS_2 at Q0: obstruction localisation holds at the 8-bit level where sites are directly inspectable.
prf_WLS_2_stephttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WLS_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Inductive step for QLS_2: if obstruction is localised at Q_k, the local-to-global structure of the constraint nerve preserves localisation at Q_{k+1}.
prf_WLS_3_basehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WLS_3
  • universalScope: false
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Base case for QLS_3 at Q0: monotone lifting basis size increment holds trivially for 8-bit to 16-bit extension.
prf_WLS_3_stephttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WLS_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Inductive step for QLS_3: the minimal basis construction at Q_{k+1} adds exactly one element from the trivially obstructed site.
prf_WLS_4_basehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WLS_4
  • universalScope: false
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Base case for QLS_4 at Q0: spectral sequence convergence at E_{d+2} holds for 8-bit filtrations by direct computation.
prf_WLS_4_stephttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WLS_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Inductive step for QLS_4: filtration length at Q_{k+1} extends by at most one page from Q_k, preserving the E_{d+2} bound.
prf_WLS_5_basehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WLS_5
  • universalScope: false
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Base case for QLS_5 at Q0: universallyValid identities hold in the 8-bit ring by definition of universal validity.
prf_WLS_6_basehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WLS_6
  • universalScope: false
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Base case for QLS_6 at Q0: the psi-pipeline produces a valid ChainComplex for 8-bit WittLifts by direct construction.
prf_WLS_6_stephttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WLS_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Inductive step for QLS_6: the functorial construction of the chain complex commutes with quantum level extension.
prf_WT_3_basehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WT_3
  • universalScope: false
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Base case for QT_3: resolved basis size formula holds for chain length 1 by direct construction.
prf_WT_5_basehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WT_5
  • universalScope: false
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Base case for QT_5: LiftChainCertificate existence for tower height 1 follows from single-step certificate issuance.
prf_AR_5_basehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AR_5
  • universalScope: false
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Base case for AR_5 at Q0: greedy vs adiabatic cost difference verified by exhaustive enumeration over Z/256Z.
prf_AR_5_stephttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AR_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Inductive step for AR_5: if greedy vs adiabatic bound holds at Q_k, it holds at Q_{k+1} by QLS_5 (universal identity preservation under quantum lift).
prf_QM_6_basehttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QM_6
  • universalScope: false
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Base case for QM_6 at Q0: amplitude index set equals monotone pinning trajectories by exhaustive trajectory enumeration over the 8-bit site lattice.
prf_QM_6_stephttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QM_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Inductive step for QM_6: monotone pinning trajectories at Q_{k+1} extend those at Q_k by the site lattice ordering (monotone extension property).
prf_MN_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MN_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of holonomy group containment: HolonomyGroup(T) ≤ D_{2^n}. Follows from the fact that all constraint applications are dihedral group elements.
prf_MN_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MN_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of additive flatness: additive constraints (ResidueConstraint, DepthConstraint) generate only the identity in D_{2^n}. Follows from the additive structure of the dihedral action.
prf_MN_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MN_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of dihedral generation: neg and bnot together generate D_{2^n}. Follows from the standard presentation of the dihedral group by involutions.
prf_MN_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MN_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of holonomy-Betti implication: non-trivial holonomy implies β₁ ≥ 1. Follows from the fact that a non-trivial monodromy requires a topological loop in the constraint nerve.
prf_MN_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MN_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of CompleteType holonomy: IT_7d (β₁ = 0) implies trivial holonomy (FlatType). Follows from MN_4 contrapositive: trivial holonomy ← β₁ = 0.
prf_MN_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MN_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of monodromy composition: the monodromy map is a group homomorphism from the loop space to D_{2^n}. Follows from the composition of dihedral group elements.
prf_MN_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MN_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of TwistedType obstruction class: a TwistedType always contributes a non-zero class to H²(N(C(T')); ℤ/2ℤ) for any WittLift T'. Follows from MN_4 and the obstruction theory of dihedral torsors.
prf_PT_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PT_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of PT_1: product type site additivity. siteBudget(A × B) = siteBudget(A) + siteBudget(B). Follows from the definition of ProductType as an independent concatenation of site spaces.
prf_PT_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PT_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of PT_2: product type partition factorisation. partition(A × B) = partition(A) ⊗ partition(B). Follows from the tensor product structure of constraint nerves over independent site spaces.
prf_PT_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PT_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Proof of PT_3: product type Euler characteristic additivity. χ(N(C(A × B))) = χ(N(C(A))) + χ(N(C(B))). Follows from the Künneth formula applied to the join of constraint nerves.
prf_PT_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PT_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of PT_4: product type entropy additivity. S(A × B) = S(A) + S(B). Follows from PT_1 (site additivity) and TH_1 (S = freeRank × ln 2).
prf_ST_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/ST_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of ST_1: sum type site budget maximum. siteBudget(A + B) = max(siteBudget(A), siteBudget(B)). Follows from SumType requiring capacity for the larger variant.
prf_ST_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/ST_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of ST_2: sum type entropy. S(A + B) = ln 2 + max(S(A), S(B)). The ln 2 term accounts for the variant discriminant bit; the max reflects that only one variant is active at a time.
prf_GS_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GS_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of SC_1: context temperature. T_ctx(C) = freeRank(C) × ln 2 / n. Derived from TH_1 normalized per site.
prf_GS_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GS_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of SC_2: saturation degree. σ(C) = (n − freeRank(C)) / n. Definitional identity.
prf_GS_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GS_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of SC_3: saturation monotonicity. Corollary of SR_1 through order-reversing SC_2.
prf_GS_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GS_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of SC_4: ground state equivalence. Four equivalent conditions for full saturation derived from SC_2, TH_1, SC_1.
prf_GS_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GS_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of SC_5: O(1) resolution guarantee at saturation. Derived from SR_2 and FreeRank.isClosed at freeRank = 0.
prf_GS_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GS_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of SC_6: pre-reduction of effective budget. Derived from session-scoped site reduction at partial saturation.
prf_GS_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GS_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of SC_7: thermodynamic cooling cost. n site-closures at Landauer cost each via SR_1 + TH_4.
prf_MS_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MS_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of MS_1: connectivity lower bound β₀ ≥ 1. Formalisation of TS_7.
prf_MS_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MS_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of MS_2: Euler capacity ceiling χ ≤ n. Derived from TS_1 constraint nerve dimension bound.
prf_MS_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MS_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of MS_3: Betti monotonicity under constraint addition. Formalisation of TS_3.
prf_MS_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MS_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of MS_4: level-relative achievability. Derived from WittLift construction (Amendment 29).
prf_MS_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MS_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of MS_5: empirical completeness convergence. Convergence statement for verification accumulation.
prf_GD_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GD_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of GD_1: geodesic condition. Dual condition from AR_1 ordering + DC_10 selection.
prf_GD_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GD_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of GD_2: geodesic entropy bound. Each step on a geodesic erases exactly ln 2 nats.
prf_GD_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GD_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of GD_3: total geodesic cost equals Landauer bound TH_4 with equality.
prf_GD_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GD_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of GD_4: geodesic uniqueness up to step-order equivalence. Equal-J_k permutations are interchangeable.
prf_GD_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GD_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of GD_5: subgeodesic detectability via step-by-step J_k check.
prf_QM_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QM_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Proof of QM_1: von Neumann–Landauer bridge. S_vN equals Landauer erasure cost at the Landauer temperature β* = ln 2.
prf_QM_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QM_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of QM_2: measurement as site topology change. Projective collapse ≅ classical ResidueConstraint pinning.
prf_QM_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QM_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Proof of QM_3: superposition entropy bound. 0 ≤ S_vN ≤ ln 2 for single-site superpositions.
prf_QM_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QM_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of QM_4: collapse idempotence. Re-measurement of a collapsed state is a no-op.
prf_QM_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QM_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Proof of QM_5: amplitude normalization (Born rule). Σ|αᵢ|² = 1 for well-formed SuperposedSiteState.
prf_RC_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RC_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of RC_6: amplitude renormalization. Division by norm yields a normalized SuperposedSiteState.
prf_FPM_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FPM_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/DecideQ0
Proof of FPM_8: partition exhaustiveness. The four component cardinalities sum to 2ⁿ.
prf_FPM_9https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FPM_9
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of FPM_9: exterior membership criterion. x ∈ Ext(T) iff x ∉ carrier(T).
prf_MN_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MN_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of MN_8: holonomy classification covering. Every ConstrainedType is flat xor twisted.
prf_QL_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/QL_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of QL_8: quantum level chain inverse. wittLevelPredecessor is the left inverse of nextLevel.
prf_D_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/D_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Proof of D_7: dihedral composition rule from the semidirect product presentation.
prf_SP_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SP_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of SP_1: classical embedding. Superposition resolution of a classical datum reduces to classical resolution.
prf_SP_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SP_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Proof of SP_2: collapse–resolve commutativity. The collapse and resolve operations commute.
prf_SP_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SP_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of SP_3: amplitude preservation. The SuperpositionResolver preserves the normalized amplitude vector.
prf_SP_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SP_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Proof of SP_4: Born rule outcome probability. P(collapse to site k) = |α_k|².
prf_PT_2ahttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PT_2a
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of PT_2a: product type partition tensor. Π(A × B) = PartitionProduct(Π(A), Π(B)).
prf_PT_2bhttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PT_2b
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of PT_2b: sum type partition coproduct. Π(A + B) = PartitionCoproduct(Π(A), Π(B)).
prf_GD_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GD_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of GD_6: geodesic predicate decomposition. isGeodesic = isAR1Ordered ∧ isDC10Selected.
iw_beta0_boundhttps://uor.foundation/proof/ImpossibilityWitness
  • forbidsSignature: β₀ = 0
  • impossibilityReason: β₀ = 0 violates MS_1: constraint nerve of non-empty set is connected
  • impossibilityDomain: https://uor.foundation/op/Pipeline
  • verified: true
  • strategy: https://uor.foundation/proof/Contradiction
Impossibility witness for MS_1: β₀ = 0 is forbidden for any non-empty ConstrainedType because the constraint nerve is always connected.
iw_chi_ceilinghttps://uor.foundation/proof/ImpossibilityWitness
  • forbidsSignature: χ > n
  • impossibilityReason: χ > n violates MS_2: Euler characteristic bounded by quantum level
  • impossibilityDomain: https://uor.foundation/op/Algebraic
  • verified: true
  • strategy: https://uor.foundation/proof/Contradiction
Impossibility witness for MS_2: χ > n is forbidden at quantum level n. The Euler characteristic cannot exceed the quantum level.
mr_completeness_targethttps://uor.foundation/proof/MorphospaceRecord
  • boundaryType: https://uor.foundation/observable/Achievable
  • verified: true
Morphospace record: the IT_7d completeness target χ = n is achievable (sits at the ceiling of MS_2).
mr_connectivity_lowerhttps://uor.foundation/proof/MorphospaceRecord
  • boundaryType: https://uor.foundation/observable/Forbidden
  • verified: true
Morphospace record: the connectivity lower bound β₀ ≥ 1 marks the forbidden region from below.
prf_WT_1https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/WT_1
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_WLS_1
  • inductiveStep: https://uor.foundation/proof/prf_WLS_6
  • validForKAtLeast: 0
  • strategy: https://uor.foundation/proof/BitwiseInduction
Proof of tower chain validity by induction on chain length.
prf_WT_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WT_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Proof of obstruction count bound: direct from QLS_2 localization.
prf_WT_3https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/WT_3
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_WT_3_base
  • inductiveStep: https://uor.foundation/proof/prf_WLS_3
  • validForKAtLeast: 0
  • strategy: https://uor.foundation/proof/BitwiseInduction
Proof of resolved basis size formula by induction on chain length.
prf_WT_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WT_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of flat tower characterization: isFlat iff trivial holonomy at every step.
prf_WT_5https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/WT_5
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_WT_5_base
  • inductiveStep: https://uor.foundation/proof/prf_WT_1
  • validForKAtLeast: 0
  • strategy: https://uor.foundation/proof/BitwiseInduction
Proof of LiftChainCertificate existence by induction on tower height.
prf_WT_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WT_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Proof of single-step reduction: QT_3 with chainLength=1 reduces to QLS_3.
prf_WT_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WT_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Proof of flat chain basis size formula.
prf_CC_PINShttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CC_PINS
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of CC_PINS: carry-constraint site-pinning map follows from ring carry propagation rule.
prf_CC_COST_SITEhttps://uor.foundation/proof/ComputationCertificate
  • provesIdentity: https://uor.foundation/op/CC_COST_SITE
  • atWittLevel: https://uor.foundation/schema/W8
  • verified: true
  • strategy: https://uor.foundation/proof/Computation
Computation certificate for CC_COST_SITE: exhaustive enumeration at Q0 confirms |pinsSites| = popcount + 1.
prf_jsat_RRhttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/jsat_RR
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of jsat_RR: CRT joint satisfiability follows from the Chinese Remainder Theorem.
prf_jsat_CRhttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/jsat_CR
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of jsat_CR: carry-residue joint satisfiability follows from the carry stopping rule and residue class intersection.
prf_jsat_CChttps://uor.foundation/proof/ComputationCertificate
  • provesIdentity: https://uor.foundation/op/jsat_CC
  • atWittLevel: https://uor.foundation/schema/W8
  • verified: true
  • strategy: https://uor.foundation/proof/Computation
Computation certificate for jsat_CC: bit-pattern exhaustive enumeration at Q0.
prf_D_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/D_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of D_8: dihedral inverse formula follows from D_5 group presentation and D_7 composition rule.
prf_D_9https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/D_9
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of D_9: reflection order 2 follows from D_7 composition: (r^k s)(r^k s) = identity.
prf_EXP_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EXP_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of EXP_1: monotone carrier characterization follows from site lattice monotonicity.
prf_EXP_2https://uor.foundation/proof/ComputationCertificate
  • provesIdentity: https://uor.foundation/op/EXP_2
  • atWittLevel: https://uor.foundation/schema/W8
  • verified: true
  • strategy: https://uor.foundation/proof/Computation
Computation certificate for EXP_2: principal filter count verified by exhaustive enumeration at Q0.
prf_EXP_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EXP_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of EXP_3: SumType carrier is coproduct by definitional architectural decision.
prf_ST_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/ST_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Proof of ST_3: Euler characteristic additivity for disjoint simplicial complexes.
prf_ST_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/ST_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of ST_4: Betti number additivity via Mayer-Vietoris for disjoint union.
prf_ST_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/ST_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Proof of ST_5: SumType completeness transfer follows from ST_3 + ST_4 + IT_7d.
prf_TS_8https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/TS_8
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_HA_1
  • inductiveStep: https://uor.foundation/proof/prf_TS_4
  • validForKAtLeast: 1
  • strategy: https://uor.foundation/proof/BitwiseInduction
Inductive proof of TS_8: minimum constraint count for beta_1 = k is 2k + 1. Base case at k=1 requires 3 mutually overlapping constraints.
prf_TS_9https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/TS_9
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_TS_1
  • inductiveStep: https://uor.foundation/proof/prf_TS_4
  • validForKAtLeast: 1
  • strategy: https://uor.foundation/proof/BitwiseInduction
Inductive proof of TS_9: TypeSynthesisResolver terminates in at most 2^n steps. Base case at n=1 has 2 constraint combinations.
prf_TS_10https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TS_10
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of TS_10: ForbiddenSignature membership follows from exhaustive enumeration bound.
prf_WT_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WT_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Proof of QT_8: ObstructionChain length bound follows from QLS_2 and spectral sequence convergence.
prf_WT_9https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WT_9
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of QT_9: TowerCompletenessResolver termination follows from finite chain length and QT_8 bound.
prf_COEFF_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/COEFF_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of COEFF_1: Z/2Z coefficient ring is definitional, consistent with MN_7.
prf_GO_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GO_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Proof of GO_1: cohomology killing lemma for GluingObstruction feedback.
prf_GR_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GR_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of SR_6: saturation re-entry free count follows from SR_1 monotone accumulation and SC_2.
prf_GR_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GR_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of SR_7: saturation degree degradation follows from SC_2 definition and SR_1 monotonicity.
prf_QM_6https://uor.foundation/proof/InductiveProof
  • provesIdentity: https://uor.foundation/op/QM_6
  • universalScope: true
  • verified: true
  • baseCase: https://uor.foundation/proof/prf_QM_6_base
  • inductiveStep: https://uor.foundation/proof/prf_QM_6_step
  • validForKAtLeast: 0
  • strategy: https://uor.foundation/proof/BitwiseInduction
Inductive proof of QM_6: amplitude index set equals monotone pinning trajectories. Base case at Q0 by exhaustive trajectory enumeration; inductive step by site lattice ordering.
prf_CIC_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CIC_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of CIC_1: TransformCertificate issuance coverage.
prf_CIC_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CIC_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/GroupPresentation
Proof of CIC_2: IsometryCertificate issuance coverage.
prf_CIC_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CIC_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of CIC_3: InvolutionCertificate issuance coverage.
prf_CIC_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CIC_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of CIC_4: GroundingCertificate issuance coverage.
prf_CIC_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CIC_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of CIC_5: GeodesicCertificate issuance coverage.
prf_CIC_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CIC_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Proof of CIC_6: MeasurementCertificate issuance coverage.
prf_CIC_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CIC_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Axiomatic derivation of CIC_7: BornRuleVerification issuance coverage. Follows by composition from corrected OA_4 (product formula chain) and QM_5 (amplitude normalization).
prf_GC_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GC_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of GC_1: GroundingCertificate issuance coverage.
prf_GR_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GR_8
  • universalScope: false
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of SR_8: session composition tower consistency.
prf_GR_9https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GR_9
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of SR_9: ContextLease site disjointness.
prf_GR_10https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GR_10
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of SR_10: ExecutionPolicy confluence.
prf_MC_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MC_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of MC_1: lease partition conserves total budget.
prf_MC_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MC_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of MC_2: per-lease binding monotonicity.
prf_MC_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MC_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of MC_3: composition freeRank inclusion-exclusion.
prf_MC_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MC_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of MC_4: disjoint-lease composition additivity.
prf_MC_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MC_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of MC_5: policy-invariant final binding set.
prf_MC_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MC_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of MC_6: full lease coverage implies composed saturation.
prf_MC_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MC_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Proof of MC_7: distributed O(1) resolution.
prf_MC_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MC_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Proof of MC_8: parallelism bound on per-session resolution work.
prf_WC_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_1: Witt coordinate = bit coordinate at p=2.
prf_WC_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_2: Witt sum correction = carry.
prf_WC_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_3: carry recurrence = Witt polynomial recurrence.
prf_WC_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_4: δ-correction = single-level carry.
prf_WC_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_5: LiftObstruction = δ nonvanishing.
prf_WC_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_6: metric discrepancy = Witt defect.
prf_WC_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_7: D_1 = Witt truncation order.
prf_WC_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_8: D_3 = Witt-Burnside conjugation.
prf_WC_9https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_9
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_9: D_4 = reflection composition.
prf_WC_10https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_10
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_10: Frobenius = identity on W_n(F_2).
prf_WC_11https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_11
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_11: Verschiebung = doubling.
prf_WC_12https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/WC_12
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/BitwiseInduction
Axiomatic derivation of WC_12: δ = squaring defect / 2.
prf_OA_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OA_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Axiomatic derivation of OA_1: Ostrowski product formula at p=2.
prf_OA_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OA_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Axiomatic derivation of OA_2: crossing cost = ln 2.
prf_OA_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OA_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Axiomatic derivation of OA_3: Landauer cost grounding via product formula.
prf_OA_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OA_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Axiomatic derivation of OA_4: Born rule bridge follows from the product formula chain OA_1 (Ostrowski) -> OA_2 (crossing cost) -> OA_3 (Landauer grounding) -> OA_4.
prf_OA_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OA_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/ProductFormula
Axiomatic derivation of OA_5: entropy per δ-level = crossing cost.
prf_HT_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HT_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of HT_1: the constraint nerve satisfies the Kan extension condition.
prf_HT_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HT_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of HT_2: path components recover Betti number β₀.
prf_HT_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HT_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of HT_3: π₁ factors through HolonomyGroup.
prf_HT_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HT_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of HT_4: higher homotopy groups vanish above dimension.
prf_HT_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HT_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of HT_5: 1-truncation determines flat/twisted classification.
prf_HT_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HT_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of HT_6: trivial k-invariants imply spectral collapse.
prf_HT_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HT_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of HT_7: Whitehead product detects lift obstructions.
prf_HT_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HT_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of HT_8: Hurewicz isomorphism for first non-vanishing group.
prf_psi_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/psi_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of ψ_7: KanComplex to PostnikovTower functor.
prf_psi_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/psi_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of ψ_8: PostnikovTower to HomotopyGroups extraction.
prf_psi_9https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/psi_9
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of ψ_9: HomotopyGroups to KInvariants computation.
prf_HP_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HP_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of HP_1: pipeline composition ψ_7 ∘ ψ_1.
prf_HP_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HP_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of HP_2: homotopy extraction agrees with homology on truncation.
prf_HP_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HP_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of HP_3: ψ_9 detects QLS_4 convergence.
prf_HP_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HP_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of HP_4: HomotopyResolver complexity bound.
prf_MD_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MD_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of MD_1: moduli dimension equals basis cardinality.
prf_MD_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MD_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of MD_2: automorphism group is subgroup of D_{2^n}.
prf_MD_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MD_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of MD_3: first-order deformations parameterize tangent space.
prf_MD_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MD_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of MD_4: obstruction space equals LiftObstruction.
prf_MD_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MD_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of MD_5: FlatType stratum is open (codimension 0).
prf_MD_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MD_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of MD_6: TwistedType strata have codimension at least 1.
prf_MD_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MD_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of MD_7: versal deformation exists when unobstructed.
prf_MD_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MD_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of MD_8: completeness-preserving iff obstruction vanishes along path.
prf_MD_9https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MD_9
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of MD_9: tower map site dimension is 1 when unobstructed.
prf_MD_10https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MD_10
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of MD_10: tower map site empty iff twisted at every level.
prf_MR_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MR_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of MR_1: moduli resolver agrees with MorphospaceBoundary.
prf_MR_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MR_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of MR_2: stratification record is complete.
prf_MR_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MR_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of MR_3: moduli resolver complexity bound.
prf_MR_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MR_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of MR_4: moduli-morphospace consistency.
prf_CY_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CY_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CY_1: carry generation condition.
prf_CY_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CY_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CY_2: carry propagation condition.
prf_CY_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CY_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CY_3: carry kill condition.
prf_CY_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CY_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CY_4: d_Δ as carry–Hamming discrepancy.
prf_CY_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CY_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CY_5: optimal encoding theorem.
prf_CY_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CY_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CY_6: site ordering theorem.
prf_CY_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CY_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CY_7: carry lookahead via prefix computation.
prf_BM_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/BM_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of BM_1: saturation metric definition.
prf_BM_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/BM_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of BM_2: Euler characteristic formula.
prf_BM_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/BM_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of BM_3: index theorem linking all six metrics.
prf_BM_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/BM_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of BM_4: Jacobian vanishes on pinned sites.
prf_BM_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/BM_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of BM_5: d_delta equals Witt defect.
prf_BM_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/BM_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of BM_6: metric composition tower.
prf_GL_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GL_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of GL_1: σ as lower adjoint.
prf_GL_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GL_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of GL_2: r as complement of upper adjoint.
prf_GL_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GL_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of GL_3: completeness as Galois fixpoint.
prf_GL_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/GL_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of GL_4: Galois order reversal.
prf_NV_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/NV_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of NV_1: nerve additivity for disjoint domains.
prf_NV_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/NV_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of NV_2: Mayer–Vietoris for constraint nerves.
prf_NV_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/NV_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of NV_3: Betti number bounded change.
prf_NV_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/NV_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of NV_4: accumulation monotonicity.
prf_SD_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SD_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SD_1: scalar grounding identity.
prf_SD_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SD_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SD_2: symbol grounding identity.
prf_SD_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SD_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SD_3: sequence free monoid identity.
prf_SD_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SD_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SD_4: tuple site additivity.
prf_SD_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SD_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SD_5: graph nerve equality.
prf_SD_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SD_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SD_6: set permutation invariance.
prf_SD_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SD_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SD_7: tree acyclicity constraint.
prf_SD_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SD_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SD_8: table functorial decomposition.
prf_DD_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DD_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of DD_1: dispatch determinism.
prf_DD_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DD_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of DD_2: dispatch coverage.
prf_PI_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PI_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PI_1: inference idempotence.
prf_PI_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PI_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PI_2: inference soundness.
prf_PI_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PI_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PI_3: inference composition.
prf_PI_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PI_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PI_4: inference complexity.
prf_PI_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PI_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PI_5: inference coherence.
prf_PA_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PA_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PA_1: accumulation permutation invariance.
prf_PA_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PA_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PA_2: accumulation monotonicity.
prf_PA_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PA_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PA_3: accumulation soundness.
prf_PA_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PA_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PA_4: accumulation base preservation.
prf_PA_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PA_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PA_5: accumulation identity element.
prf_PL_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PL_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PL_1: lease disjointness.
prf_PL_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PL_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PL_2: lease conservation.
prf_PL_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PL_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PL_3: lease coverage.
prf_PK_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PK_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PK_1: composition validity.
prf_PK_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PK_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PK_2: distributed resolution.
prf_PP_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PP_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of PP_1: pipeline unification.
prf_PE_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PE_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PE_1: state initialization.
prf_PE_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PE_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PE_2: resolver dispatch.
prf_PE_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PE_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PE_3: ring address grounding.
prf_PE_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PE_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PE_4: constraint resolution.
prf_PE_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PE_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PE_5: consistent accumulation.
prf_PE_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PE_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PE_6: coherent extraction.
prf_PE_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PE_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PE_7: full pipeline composition.
prf_PM_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PM_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PM_1: phase rotation.
prf_PM_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PM_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PM_2: phase gate check.
prf_PM_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PM_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PM_3: conjugate rollback.
prf_PM_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PM_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PM_4: rollback involution.
prf_PM_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PM_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PM_5: epoch saturation preservation.
prf_PM_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PM_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PM_6: service window context.
prf_PM_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PM_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PM_7: machine determinism.
prf_ER_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/ER_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of ER_1: guard satisfaction.
prf_ER_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/ER_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of ER_2: effect atomicity.
prf_ER_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/ER_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of ER_3: guard purity.
prf_ER_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/ER_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of ER_4: intra-stage commutativity.
prf_EA_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EA_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of EA_1: epoch boundary reset.
prf_EA_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EA_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of EA_2: saturation monotonicity.
prf_EA_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EA_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of EA_3: service window bound.
prf_EA_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EA_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of EA_4: epoch admission exclusivity.
prf_OE_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OE_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OE_1: stage fusion.
prf_OE_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OE_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OE_2: effect commutativity.
prf_OE_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OE_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OE_3: lease parallelism.
prf_OE_4ahttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OE_4a
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OE_4a: fusion semantics preservation.
prf_OE_4bhttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OE_4b
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OE_4b: commutation outcome preservation.
prf_OE_4chttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OE_4c
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of OE_4c: parallelism coverage preservation.
prf_CS_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CS_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CS_1: bounded stage cost.
prf_CS_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CS_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CS_2: additive pipeline cost.
prf_CS_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CS_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CS_3: bounded rollback cost.
prf_CS_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CS_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CS_4: constant preflight cost.
prf_CS_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CS_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CS_5: total reduction cost bound.
prf_FA_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FA_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of FA_1: query liveness.
prf_FA_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FA_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of FA_2: no starvation.
prf_FA_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FA_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of FA_3: fair lease allocation.
prf_SW_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SW_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of SW_1: memory boundedness.
prf_SW_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SW_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of SW_2: saturation invariance.
prf_SW_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SW_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of SW_3: eviction releases resources.
prf_SW_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SW_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of SW_4: non-empty window.
prf_LS_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/LS_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of LS_1: suspension preserves pinned state.
prf_LS_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/LS_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of LS_2: expiry releases resources.
prf_LS_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/LS_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of LS_3: checkpoint restore idempotence.
prf_LS_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/LS_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of LS_4: suspend-resume round-trip.
prf_TJ_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TJ_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TJ_1: AllOrNothing rollback.
prf_TJ_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TJ_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TJ_2: BestEffort partial commit.
prf_TJ_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/TJ_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of TJ_3: epoch-scoped atomicity.
prf_AP_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AP_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AP_1: saturation monotonicity.
prf_AP_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AP_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AP_2: quality improvement.
prf_AP_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AP_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of AP_3: deferred query liveness.
prf_EC_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EC_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of EC_1: phase half-turn convergence.
prf_EC_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EC_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of EC_2: conjugate involution.
prf_EC_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EC_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of EC_3: pairwise commutator convergence.
prf_EC_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EC_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of EC_4: triple associator convergence.
prf_EC_4ahttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EC_4a
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of EC_4a: associator monotonicity.
prf_EC_4bhttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EC_4b
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of EC_4b: associator finiteness.
prf_EC_4chttps://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EC_4c
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of EC_4c: vanishing implies associativity.
prf_EC_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/EC_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of EC_5: Adams termination.
prf_DA_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DA_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of DA_1: Cayley-Dickson R→C.
prf_DA_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DA_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of DA_2: Cayley-Dickson C→H.
prf_DA_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DA_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of DA_3: Cayley-Dickson H→O.
prf_DA_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DA_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of DA_4: Adams dimension restriction.
prf_DA_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DA_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of DA_5: convergence-level algebra correspondence.
prf_DA_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DA_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of DA_6: commutator-commutativity equivalence.
prf_DA_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DA_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of DA_7: associator-associativity equivalence.
prf_IN_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IN_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IN_1: interaction cost.
prf_IN_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IN_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IN_2: disjoint leases commute.
prf_IN_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IN_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IN_3: shared sites nonzero commutator.
prf_IN_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IN_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IN_4: negotiation convergence.
prf_IN_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IN_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IN_5: commutative subspace selection.
prf_IN_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IN_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IN_6: pairwise outcome space.
prf_IN_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IN_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IN_7: associative subalgebra selection.
prf_IN_8https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IN_8
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IN_8: nerve Betti coupling bound.
prf_IN_9https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IN_9
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of IN_9: Betti-disagreement associator bound.
prf_AS_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AS_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of AS_1: δ-ι-κ non-associativity.
prf_AS_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AS_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of AS_2: ι-α-λ non-associativity.
prf_AS_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AS_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of AS_3: λ-κ-δ non-associativity.
prf_AS_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/AS_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Composition
Axiomatic derivation of AS_4: non-associativity root cause.
prf_MO_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MO_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of MO_1: monoidal unit law.
prf_MO_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MO_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of MO_2: monoidal associativity.
prf_MO_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MO_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of MO_3: certificate composition.
prf_MO_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MO_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of MO_4: saturation monotonicity.
prf_MO_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/MO_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of MO_5: residual monotonicity.
prf_OP_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OP_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of OP_1: site additivity.
prf_OP_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OP_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of OP_2: grounding distributivity.
prf_OP_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OP_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of OP_3: d_Δ decomposition.
prf_OP_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OP_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of OP_4: tabular data decomposition.
prf_OP_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/OP_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of OP_5: hierarchical data structure.
prf_FX_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FX_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FX_1: pinning site budget decrement.
prf_FX_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FX_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FX_2: unbinding site budget increment.
prf_FX_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FX_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FX_3: phase budget invariance.
prf_FX_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FX_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FX_4: disjoint commutativity.
prf_FX_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FX_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FX_5: composite delta additivity.
prf_FX_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FX_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FX_6: reversible inverse.
prf_FX_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FX_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of FX_7: external shape compliance.
prf_PR_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PR_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PR_1: predicate totality.
prf_PR_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PR_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PR_2: predicate purity.
prf_PR_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PR_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PR_3: deterministic dispatch.
prf_PR_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PR_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PR_4: deterministic match.
prf_PR_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PR_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PR_5: typed guard transition.
prf_CG_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CG_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CG_1: typed entry guard.
prf_CG_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CG_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CG_2: typed exit guard with effect.
prf_DIS_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DIS_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DIS_1: exhaustive exclusive table.
prf_DIS_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/DIS_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of DIS_2: deterministic resolver selection.
prf_PAR_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PAR_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of PAR_1: disjoint commutativity.
prf_PAR_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PAR_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of PAR_2: delta additivity.
prf_PAR_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PAR_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of PAR_3: exhaustive partitioning.
prf_PAR_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PAR_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of PAR_4: interleaving invariance.
prf_PAR_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/PAR_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of PAR_5: certificate conjunction.
prf_HO_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HO_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of HO_1: content-addressed certification.
prf_HO_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HO_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of HO_2: application certification.
prf_HO_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HO_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of HO_3: composition certification.
prf_HO_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/HO_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of HO_4: saturation equivalence.
prf_STR_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/STR_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of STR_1: epoch termination.
prf_STR_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/STR_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of STR_2: saturation preservation.
prf_STR_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/STR_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of STR_3: finite prefix computability.
prf_STR_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/STR_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of STR_4: unfold seed initialization.
prf_STR_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/STR_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of STR_5: continuation chaining.
prf_STR_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/STR_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of STR_6: lease expiry budget return.
prf_FLR_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FLR_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FLR_1: coproduct exhaustiveness.
prf_FLR_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FLR_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of FLR_2: total computation guarantee.
prf_FLR_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FLR_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FLR_3: sequential propagation.
prf_FLR_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FLR_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of FLR_4: parallel independence.
prf_FLR_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FLR_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of FLR_5: recovery result.
prf_FLR_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/FLR_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of FLR_6: conjugate rollback.
prf_LN_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/LN_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of LN_1: exact coverage.
prf_LN_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/LN_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of LN_2: pinning effect.
prf_LN_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/LN_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of LN_3: consumption linearity.
prf_LN_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/LN_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of LN_4: lease budget decrement.
prf_LN_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/LN_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of LN_5: lease expiry return.
prf_LN_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/LN_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of LN_6: geodesic linearity.
prf_SB_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SB_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SB_1: constraint superset.
prf_SB_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SB_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SB_2: resolution subset.
prf_SB_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SB_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of SB_3: nerve sub-complex.
prf_SB_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SB_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SB_4: covariance.
prf_SB_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SB_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SB_5: contravariance.
prf_SB_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/SB_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of SB_6: lattice depth.
prf_BR_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/BR_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of BR_1: strict descent.
prf_BR_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/BR_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of BR_2: depth bound.
prf_BR_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/BR_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of BR_3: termination guarantee.
prf_BR_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/BR_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of BR_4: structural measure.
prf_BR_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/BR_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of BR_5: base predicate zero.
prf_RG_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RG_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/EulerPoincare
Axiomatic derivation of RG_1: nerve-determined working set.
prf_RG_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RG_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of RG_2: diameter bound.
prf_RG_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RG_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of RG_3: addressable space bound.
prf_RG_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/RG_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of RG_4: working set containment.
prf_IO_1https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IO_1
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of IO_1: ingest type conformance.
prf_IO_2https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IO_2
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of IO_2: emit type conformance.
prf_IO_3https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IO_3
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of IO_3: grounding validity.
prf_IO_4https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IO_4
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of IO_4: projection validity.
prf_IO_5https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/IO_5
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of IO_5: non-vacuous crossing.
prf_CS_6https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CS_6
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/Simplification
Axiomatic derivation of CS_6: budget solvency rejection.
prf_CS_7https://uor.foundation/proof/AxiomaticDerivation
  • provesIdentity: https://uor.foundation/op/CS_7
  • universalScope: true
  • verified: true
  • strategy: https://uor.foundation/proof/RingAxiom
Axiomatic derivation of CS_7: unit address computation.