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.

View documentation reference

This is a bridge-space namespace in the Resolve stage of the PRISM pipeline. It provides the resolution infrastructure — queries, partitions, observables, proofs, derivations, and traces that transform inputs into certified results.

Learn more: Pipeline Overview · Proofs, Derivations & Traces

Class hierarchy
Class hierarchy for UOR Proofs namespace Proof CoherenceProof ComputationCer AxiomaticDeriv CriticalIdenti WitnessData ImpossibilityW MorphospaceRec MorphospaceBou InductiveProof ProofStrategy DerivationTerm TacticApplicat LemmaInvocatio InductionStep ComputationSte

Imports

Classes

NameSubclass OfDisjoint WithComment
ProofThingA kernel-produced attestation that a given algebraic property holds. The root class for all proof types.
CoherenceProofProofA proof of coherence: the type system and ring structure are mutually consistent at a given quantum level.
ComputationCertificateProofA 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.
AxiomaticDerivationProofA 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.
CriticalIdentityProofComputationCertificateA 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.
WitnessDataThingSupporting data for a proof: specific examples, counter-examples checked, or intermediate computation results.
ImpossibilityWitnessProofA 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.
MorphospaceRecordThingA formal record of a morphospace boundary point — either an achievable or forbidden topological signature. Aggregated by MorphospaceBoundary to form the queryable morphospace map.
MorphospaceBoundaryThingAn aggregate of ImpossibilityWitness instances forming the queryable morphospace map. SPARQL over this structure answers achievability queries in O(1).
InductiveProofProofA 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.
ProofStrategyThingA controlled vocabulary of proof methods. Each proof individual carries exactly one strategy from this vocabulary, enabling compilation to verified theorem provers.
DerivationTermThingRoot AST node for proof construction terms. Distinct from schema:TermExpression which represents mathematical terms; DerivationTerm represents proof constructions (tactic applications, lemma invocations, induction scaffolding).
TacticApplicationDerivationTermA proof step applying a named tactic (from ProofStrategy) with arguments. Maps to a Lean4 tactic invocation.
LemmaInvocationDerivationTermA proof step invoking a previously proved identity as a lemma. References the identity via proof:dependsOn.
InductionStepDerivationTermA proof step performing structural induction: base case derivation, inductive hypothesis, and step derivation.
ComputationStepDerivationTermA proof step performing exhaustive computation at a specific quantum level as verification witness.

Properties

NameKindFunctionalDomainRangeComment
verifiedDatatypetrueProofbooleanWhether this proof has been verified by the kernel.
timestampDatatypetrueProofdateTimeThe time at which this proof was produced.
witnessObjectfalseProofWitnessDataSupporting witness data for this proof.
criticalIdentityAnnotationtrueCriticalIdentityProofstringHuman-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.
xDatatypefalseWitnessDataintegerA specific input value used as a witness for the critical identity check.
bnot_xDatatypefalseWitnessDataintegerThe value bnot(x) for a witness x.
neg_bnot_xDatatypefalseWitnessDataintegerThe value neg(bnot(x)) for a witness x.
succ_xDatatypefalseWitnessDataintegerThe value succ(x) for a witness x.
holdsDatatypefalseWitnessDatabooleanWhether the identity neg(bnot(x)) = succ(x) holds for this specific witness.
provesIdentityObjecttrueProofIdentityThe algebraic identity this proof establishes. Provides a canonical object reference alongside the existing proof:criticalIdentity string property, which remains for human readability.
atWittLevelObjecttrueComputationCertificateWittLevelThe 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.
wittNoteAnnotationtrueComputationCertificatestringHuman-readable quantum level note, e.g. 'n=8, 256 inputs'. Annotation only — proof:atWittLevel is the typed assertion.
universalScopeDatatypetrueAxiomaticDerivationbooleanTrue 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.
derivationWitnessObjectfalseAxiomaticDerivationDerivationThe 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.
forbidsSignatureAnnotationtrueImpossibilityWitnessstringThe topological signature (χ, β_k) that this ImpossibilityWitness formally forbids, expressed as a symbolic notation string (e.g., 'β₀ = 0').
impossibilityReasonDatatypetrueImpossibilityWitnessstringHuman-readable statement of the algebraic reason the signature is impossible (e.g., 'β₀ = 0 violates MS_1').
impossibilityDomainObjecttrueImpossibilityWitnessVerificationDomainThe verification domain grounding the impossibility (e.g., Pipeline for β₀ = 0, Algebraic for χ > n).
achievabilityStatusObjecttrueImpossibilityWitnessAchievabilityStatusThe achievability classification of a proof-linked observable signature: Achievable or Forbidden.
verifiedAtLevelObjectfalseProofWittLevelThe specific quantum level at which an empirical verification or impossibility witness was established.
morphospaceRecordObjectfalseMorphospaceBoundaryMorphospaceRecordLinks a MorphospaceBoundary to one of its constituent MorphospaceRecord individuals.
boundaryTypeObjecttrueMorphospaceRecordAchievabilityStatusWhether this MorphospaceRecord represents an impossibility boundary (from below) or an achievability boundary (from above).
baseCaseObjecttrueInductiveProofProofThe proof that the claim holds at the base level k_0.
inductiveStepObjecttrueInductiveProofProofThe proof that if the claim holds at Q_k, it holds at Q_{k+1}.
validForKAtLeastDatatypetrueInductiveProofnonNegativeIntegerThe minimum k for which the induction is valid.
strategyObjecttrueProofProofStrategyThe proof method from the ProofStrategy controlled vocabulary. Determines the compilation target (e.g., `by ring`, `by simp`, `by induction`).
dependsOnObjectfalseProofIdentityAn identity that this proof depends on as a lemma. Forms the proof dependency DAG. Leaf proofs (provable from definitions alone) have no dependsOn assertions.
formalDerivationObjecttrueProofDerivationTermThe formal proof construction term: a DerivationTerm AST node encoding the tactic script, lemma chain, or induction scaffold that constitutes the proof.

Named Individuals

NameTypeComment
RingAxiomProofStrategyFollows from ZMod ring axioms. Lean4 tactic: `by ring`.
DecideQ0ProofStrategyDecidable at Q0 by exhaustive evaluation. Lean4: `by native_decide`.
BitwiseInductionProofStrategyInduction on bit width n. Lean4: `by induction n`.
GroupPresentationProofStrategyFrom dihedral group presentation. Lean4: `by group`.
SimplificationProofStrategyBy simplification with cited lemmas. Lean4: `by simp [lemmalist]`.
ChineseRemainderProofStrategyBy Chinese Remainder Theorem. Lean4: `by exact ZMod.chineseRemainder ...`.
EulerPoincareProofStrategyBy Euler-Poincare formula applied to the constraint nerve.
ProductFormulaProofStrategyBy Ostrowski product formula or derived valuation arguments.
CompositionProofStrategyBy composing proofs of sub-identities. Lean4: `by exact ...`.
ContradictionProofStrategyBy deriving contradiction for impossibility witnesses. Lean4: `by contradiction`.
ComputationProofStrategyBy computation at a specified quantum level. Lean4: `by native_decide`.
prf_criticalIdentityCriticalIdentityProofComputation certificate for the critical identity neg(bnot(x)) = succ(x) at Q0.
  • provesIdentity: criticalIdentity
  • atWittLevel: W8
  • verified: true
  • strategy: Computation
prf_criticalIdentity_axiomaticAxiomaticDerivationAxiomatic derivation of the critical identity neg(bnot(x)) = succ(x). Holds at all quantum levels.
  • provesIdentity: criticalIdentity
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_phi_1ComputationCertificateComputation certificate for phi_1 at Q0.
  • provesIdentity: phi_1
  • atWittLevel: W8
  • verified: true
  • strategy: Computation
prf_phi_2ComputationCertificateComputation certificate for phi_2 at Q0.
  • provesIdentity: phi_2
  • atWittLevel: W8
  • verified: true
  • strategy: Computation
prf_phi_3ComputationCertificateComputation certificate for phi_3 at Q0.
  • provesIdentity: phi_3
  • atWittLevel: W8
  • verified: true
  • strategy: Computation
prf_phi_4ComputationCertificateComputation certificate for phi_4 at Q0.
  • provesIdentity: phi_4
  • atWittLevel: W8
  • verified: true
  • strategy: Computation
prf_phi_5ComputationCertificateComputation certificate for phi_5 at Q0.
  • provesIdentity: phi_5
  • atWittLevel: W8
  • verified: true
  • strategy: Computation
prf_phi_6ComputationCertificateComputation certificate for phi_6 at Q0.
  • provesIdentity: phi_6
  • atWittLevel: W8
  • verified: true
  • strategy: Computation
prf_AD_1AxiomaticDerivationAxiomatic derivation of AD_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AD_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AD_2AxiomaticDerivationAxiomatic derivation of AD_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AD_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_R_A1AxiomaticDerivationAxiomatic derivation of R_A1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: R_A1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_R_A2AxiomaticDerivationAxiomatic derivation of R_A2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: R_A2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_R_A3AxiomaticDerivationAxiomatic derivation of R_A3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: R_A3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_R_A4AxiomaticDerivationAxiomatic derivation of R_A4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: R_A4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_R_A5AxiomaticDerivationAxiomatic derivation of R_A5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: R_A5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_R_A6AxiomaticDerivationAxiomatic derivation of R_A6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: R_A6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_R_M1AxiomaticDerivationAxiomatic derivation of R_M1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: R_M1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_R_M2AxiomaticDerivationAxiomatic derivation of R_M2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: R_M2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_R_M3AxiomaticDerivationAxiomatic derivation of R_M3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: R_M3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_R_M4AxiomaticDerivationAxiomatic derivation of R_M4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: R_M4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_R_M5AxiomaticDerivationAxiomatic derivation of R_M5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: R_M5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_B_1AxiomaticDerivationAxiomatic derivation of B_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_1
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_2AxiomaticDerivationAxiomatic derivation of B_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_2
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_3AxiomaticDerivationAxiomatic derivation of B_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_3
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_4AxiomaticDerivationAxiomatic derivation of B_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_4
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_5AxiomaticDerivationAxiomatic derivation of B_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_5
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_6AxiomaticDerivationAxiomatic derivation of B_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_6
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_7AxiomaticDerivationAxiomatic derivation of B_7. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_7
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_8AxiomaticDerivationAxiomatic derivation of B_8. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_8
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_9AxiomaticDerivationAxiomatic derivation of B_9. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_9
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_10AxiomaticDerivationAxiomatic derivation of B_10. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_10
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_11AxiomaticDerivationAxiomatic derivation of B_11. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_11
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_12AxiomaticDerivationAxiomatic derivation of B_12. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_12
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_B_13AxiomaticDerivationAxiomatic derivation of B_13. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: B_13
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_X_1AxiomaticDerivationAxiomatic derivation of X_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: X_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_X_2AxiomaticDerivationAxiomatic derivation of X_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: X_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_X_3AxiomaticDerivationAxiomatic derivation of X_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: X_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_X_4AxiomaticDerivationAxiomatic derivation of X_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: X_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_X_5AxiomaticDerivationAxiomatic derivation of X_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: X_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_X_6AxiomaticDerivationAxiomatic derivation of X_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: X_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_X_7AxiomaticDerivationAxiomatic derivation of X_7. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: X_7
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_D_1AxiomaticDerivationAxiomatic derivation of D_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: D_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_D_3AxiomaticDerivationAxiomatic derivation of D_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: D_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_D_4AxiomaticDerivationAxiomatic derivation of D_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: D_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_D_5AxiomaticDerivationAxiomatic derivation of D_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: D_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_U_1AxiomaticDerivationAxiomatic derivation of U_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: U_1
  • universalScope: true
  • verified: true
  • strategy: ChineseRemainder
prf_U_2AxiomaticDerivationAxiomatic derivation of U_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: U_2
  • universalScope: true
  • verified: true
  • strategy: ChineseRemainder
prf_U_3AxiomaticDerivationAxiomatic derivation of U_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: U_3
  • universalScope: true
  • verified: true
  • strategy: ChineseRemainder
prf_U_4AxiomaticDerivationAxiomatic derivation of U_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: U_4
  • universalScope: true
  • verified: true
  • strategy: ChineseRemainder
prf_U_5AxiomaticDerivationAxiomatic derivation of U_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: U_5
  • universalScope: true
  • verified: true
  • strategy: ChineseRemainder
prf_AG_1AxiomaticDerivationAxiomatic derivation of AG_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AG_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_AG_2AxiomaticDerivationAxiomatic derivation of AG_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AG_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_AG_3AxiomaticDerivationAxiomatic derivation of AG_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AG_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_AG_4AxiomaticDerivationAxiomatic derivation of AG_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AG_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CA_1AxiomaticDerivationAxiomatic derivation of CA_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CA_1
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_CA_2AxiomaticDerivationAxiomatic derivation of CA_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CA_2
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_CA_3AxiomaticDerivationAxiomatic derivation of CA_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CA_3
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_CA_4AxiomaticDerivationAxiomatic derivation of CA_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CA_4
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_CA_5AxiomaticDerivationAxiomatic derivation of CA_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CA_5
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_CA_6AxiomaticDerivationAxiomatic derivation of CA_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CA_6
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_C_1AxiomaticDerivationAxiomatic derivation of C_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: C_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_C_2AxiomaticDerivationAxiomatic derivation of C_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: C_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_C_3AxiomaticDerivationAxiomatic derivation of C_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: C_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_C_4AxiomaticDerivationAxiomatic derivation of C_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: C_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_C_5AxiomaticDerivationAxiomatic derivation of C_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: C_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_C_6AxiomaticDerivationAxiomatic derivation of C_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: C_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CDIAxiomaticDerivationAxiomatic derivation of CDI. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CDI
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CL_1AxiomaticDerivationAxiomatic derivation of CL_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CL_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CL_2AxiomaticDerivationAxiomatic derivation of CL_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CL_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CL_3AxiomaticDerivationAxiomatic derivation of CL_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CL_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CL_4AxiomaticDerivationAxiomatic derivation of CL_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CL_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CL_5AxiomaticDerivationAxiomatic derivation of CL_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CL_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CM_1AxiomaticDerivationAxiomatic derivation of CM_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CM_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CM_2AxiomaticDerivationAxiomatic derivation of CM_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CM_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CM_3AxiomaticDerivationAxiomatic derivation of CM_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CM_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CR_1AxiomaticDerivationAxiomatic derivation of CR_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CR_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CR_2AxiomaticDerivationAxiomatic derivation of CR_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CR_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CR_3AxiomaticDerivationAxiomatic derivation of CR_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CR_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CR_4AxiomaticDerivationAxiomatic derivation of CR_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CR_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CR_5AxiomaticDerivationAxiomatic derivation of CR_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CR_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_F_1AxiomaticDerivationAxiomatic derivation of F_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: F_1
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_F_2AxiomaticDerivationAxiomatic derivation of F_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: F_2
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_F_3AxiomaticDerivationAxiomatic derivation of F_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: F_3
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_F_4AxiomaticDerivationAxiomatic derivation of F_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: F_4
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_FL_1AxiomaticDerivationAxiomatic derivation of FL_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FL_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FL_2AxiomaticDerivationAxiomatic derivation of FL_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FL_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FL_3AxiomaticDerivationAxiomatic derivation of FL_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FL_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FL_4AxiomaticDerivationAxiomatic derivation of FL_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FL_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FPM_1AxiomaticDerivationAxiomatic derivation of FPM_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FPM_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FPM_2AxiomaticDerivationAxiomatic derivation of FPM_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FPM_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FPM_3AxiomaticDerivationAxiomatic derivation of FPM_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FPM_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FPM_4AxiomaticDerivationAxiomatic derivation of FPM_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FPM_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FPM_5AxiomaticDerivationAxiomatic derivation of FPM_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FPM_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FPM_6AxiomaticDerivationAxiomatic derivation of FPM_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FPM_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FPM_7AxiomaticDerivationAxiomatic derivation of FPM_7. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FPM_7
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FS_1AxiomaticDerivationAxiomatic derivation of FS_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FS_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FS_2AxiomaticDerivationAxiomatic derivation of FS_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FS_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FS_3AxiomaticDerivationAxiomatic derivation of FS_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FS_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FS_4AxiomaticDerivationAxiomatic derivation of FS_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FS_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FS_5AxiomaticDerivationAxiomatic derivation of FS_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FS_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FS_6AxiomaticDerivationAxiomatic derivation of FS_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FS_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FS_7AxiomaticDerivationAxiomatic derivation of FS_7. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: FS_7
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_RE_1AxiomaticDerivationAxiomatic derivation of RE_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: RE_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_IR_1AxiomaticDerivationAxiomatic derivation of IR_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: IR_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_IR_2AxiomaticDerivationAxiomatic derivation of IR_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: IR_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_IR_3AxiomaticDerivationAxiomatic derivation of IR_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: IR_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_IR_4AxiomaticDerivationAxiomatic derivation of IR_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: IR_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SF_1AxiomaticDerivationAxiomatic derivation of SF_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: SF_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SF_2AxiomaticDerivationAxiomatic derivation of SF_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: SF_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_RD_1AxiomaticDerivationAxiomatic derivation of RD_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: RD_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_RD_2AxiomaticDerivationAxiomatic derivation of RD_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: RD_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SE_1AxiomaticDerivationAxiomatic derivation of SE_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: SE_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SE_2AxiomaticDerivationAxiomatic derivation of SE_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: SE_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SE_3AxiomaticDerivationAxiomatic derivation of SE_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: SE_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SE_4AxiomaticDerivationAxiomatic derivation of SE_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: SE_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OO_1AxiomaticDerivationAxiomatic derivation of OO_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OO_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OO_2AxiomaticDerivationAxiomatic derivation of OO_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OO_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OO_3AxiomaticDerivationAxiomatic derivation of OO_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OO_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OO_4AxiomaticDerivationAxiomatic derivation of OO_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OO_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OO_5AxiomaticDerivationAxiomatic derivation of OO_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OO_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CB_1AxiomaticDerivationAxiomatic derivation of CB_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CB_1
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_CB_2AxiomaticDerivationAxiomatic derivation of CB_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CB_2
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_CB_3AxiomaticDerivationAxiomatic derivation of CB_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CB_3
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_CB_4AxiomaticDerivationAxiomatic derivation of CB_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CB_4
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_CB_5AxiomaticDerivationAxiomatic derivation of CB_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CB_5
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_CB_6AxiomaticDerivationAxiomatic derivation of CB_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CB_6
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_OB_M1AxiomaticDerivationAxiomatic derivation of OB_M1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_M1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_M2AxiomaticDerivationAxiomatic derivation of OB_M2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_M2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_M3AxiomaticDerivationAxiomatic derivation of OB_M3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_M3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_M4AxiomaticDerivationAxiomatic derivation of OB_M4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_M4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_M5AxiomaticDerivationAxiomatic derivation of OB_M5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_M5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_M6AxiomaticDerivationAxiomatic derivation of OB_M6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_M6
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_C1AxiomaticDerivationAxiomatic derivation of OB_C1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_C1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_C2AxiomaticDerivationAxiomatic derivation of OB_C2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_C2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_C3AxiomaticDerivationAxiomatic derivation of OB_C3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_C3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_H1AxiomaticDerivationAxiomatic derivation of OB_H1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_H1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_H2AxiomaticDerivationAxiomatic derivation of OB_H2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_H2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_H3AxiomaticDerivationAxiomatic derivation of OB_H3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_H3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_P1AxiomaticDerivationAxiomatic derivation of OB_P1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_P1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_P2AxiomaticDerivationAxiomatic derivation of OB_P2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_P2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OB_P3AxiomaticDerivationAxiomatic derivation of OB_P3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: OB_P3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CT_1AxiomaticDerivationAxiomatic derivation of CT_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CT_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CT_2AxiomaticDerivationAxiomatic derivation of CT_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CT_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CT_3AxiomaticDerivationAxiomatic derivation of CT_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CT_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CT_4AxiomaticDerivationAxiomatic derivation of CT_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CT_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CF_1AxiomaticDerivationAxiomatic derivation of CF_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CF_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CF_2AxiomaticDerivationAxiomatic derivation of CF_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CF_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CF_3AxiomaticDerivationAxiomatic derivation of CF_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CF_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CF_4AxiomaticDerivationAxiomatic derivation of CF_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: CF_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HG_1AxiomaticDerivationAxiomatic derivation of HG_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: HG_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HG_2AxiomaticDerivationAxiomatic derivation of HG_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: HG_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HG_3AxiomaticDerivationAxiomatic derivation of HG_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: HG_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HG_4AxiomaticDerivationAxiomatic derivation of HG_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: HG_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HG_5AxiomaticDerivationAxiomatic derivation of HG_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: HG_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_T_C1AxiomaticDerivationAxiomatic derivation of T_C1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_C1
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_C2AxiomaticDerivationAxiomatic derivation of T_C2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_C2
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_C3AxiomaticDerivationAxiomatic derivation of T_C3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_C3
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_C4AxiomaticDerivationAxiomatic derivation of T_C4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_C4
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_I1AxiomaticDerivationAxiomatic derivation of T_I1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_I1
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_I2AxiomaticDerivationAxiomatic derivation of T_I2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_I2
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_I3AxiomaticDerivationAxiomatic derivation of T_I3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_I3
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_I4AxiomaticDerivationAxiomatic derivation of T_I4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_I4
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_I5AxiomaticDerivationAxiomatic derivation of T_I5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_I5
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_E1AxiomaticDerivationAxiomatic derivation of T_E1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_E1
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_E2AxiomaticDerivationAxiomatic derivation of T_E2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_E2
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_E3AxiomaticDerivationAxiomatic derivation of T_E3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_E3
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_E4AxiomaticDerivationAxiomatic derivation of T_E4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_E4
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_A1AxiomaticDerivationAxiomatic derivation of T_A1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_A1
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_A2AxiomaticDerivationAxiomatic derivation of T_A2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_A2
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_A3AxiomaticDerivationAxiomatic derivation of T_A3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_A3
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_T_A4AxiomaticDerivationAxiomatic derivation of T_A4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: T_A4
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_AU_1AxiomaticDerivationAxiomatic derivation of AU_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AU_1
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_AU_2AxiomaticDerivationAxiomatic derivation of AU_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AU_2
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_AU_3AxiomaticDerivationAxiomatic derivation of AU_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AU_3
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_AU_4AxiomaticDerivationAxiomatic derivation of AU_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AU_4
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_AU_5AxiomaticDerivationAxiomatic derivation of AU_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AU_5
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_EF_1AxiomaticDerivationAxiomatic derivation of EF_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: EF_1
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_EF_2AxiomaticDerivationAxiomatic derivation of EF_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: EF_2
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_EF_3AxiomaticDerivationAxiomatic derivation of EF_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: EF_3
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_EF_4AxiomaticDerivationAxiomatic derivation of EF_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: EF_4
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_EF_5AxiomaticDerivationAxiomatic derivation of EF_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: EF_5
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_EF_6AxiomaticDerivationAxiomatic derivation of EF_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: EF_6
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_EF_7AxiomaticDerivationAxiomatic derivation of EF_7. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: EF_7
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_AA_1AxiomaticDerivationAxiomatic derivation of AA_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AA_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AA_2AxiomaticDerivationAxiomatic derivation of AA_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AA_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AA_3AxiomaticDerivationAxiomatic derivation of AA_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AA_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AA_4AxiomaticDerivationAxiomatic derivation of AA_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AA_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AA_5AxiomaticDerivationAxiomatic derivation of AA_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AA_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AA_6AxiomaticDerivationAxiomatic derivation of AA_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AA_6
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AM_1AxiomaticDerivationAxiomatic derivation of AM_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AM_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AM_2AxiomaticDerivationAxiomatic derivation of AM_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AM_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AM_3AxiomaticDerivationAxiomatic derivation of AM_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AM_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AM_4AxiomaticDerivationAxiomatic derivation of AM_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AM_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TH_1AxiomaticDerivationAxiomatic derivation of TH_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: TH_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TH_2AxiomaticDerivationAxiomatic derivation of TH_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: TH_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TH_3AxiomaticDerivationAxiomatic derivation of TH_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: TH_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TH_4AxiomaticDerivationAxiomatic derivation of TH_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: TH_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TH_5AxiomaticDerivationAxiomatic derivation of TH_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: TH_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TH_6AxiomaticDerivationAxiomatic derivation of TH_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: TH_6
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TH_7AxiomaticDerivationAxiomatic derivation of TH_7. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: TH_7
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TH_8AxiomaticDerivationAxiomatic derivation of TH_8. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: TH_8
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TH_9AxiomaticDerivationAxiomatic derivation of TH_9. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: TH_9
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TH_10AxiomaticDerivationAxiomatic derivation of TH_10. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: TH_10
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AR_1AxiomaticDerivationAxiomatic derivation of AR_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AR_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AR_2AxiomaticDerivationAxiomatic derivation of AR_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AR_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AR_3AxiomaticDerivationAxiomatic derivation of AR_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AR_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AR_4AxiomaticDerivationAxiomatic derivation of AR_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: AR_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AR_5InductiveProofInductive 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).
  • provesIdentity: AR_5
  • universalScope: true
  • verified: true
  • baseCase: prf_AR_5_base
  • inductiveStep: prf_AR_5_step
  • validForKAtLeast: 0
  • strategy: BitwiseInduction
prf_PD_1AxiomaticDerivationAxiomatic derivation of PD_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: PD_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PD_2AxiomaticDerivationAxiomatic derivation of PD_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: PD_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PD_3AxiomaticDerivationAxiomatic derivation of PD_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: PD_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PD_4AxiomaticDerivationAxiomatic derivation of PD_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: PD_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PD_5AxiomaticDerivationAxiomatic derivation of PD_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: PD_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_RC_1AxiomaticDerivationAxiomatic derivation of RC_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: RC_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_RC_2AxiomaticDerivationAxiomatic derivation of RC_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: RC_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_RC_3AxiomaticDerivationAxiomatic derivation of RC_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: RC_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_RC_4AxiomaticDerivationAxiomatic derivation of RC_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: RC_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_RC_5AxiomaticDerivationAxiomatic derivation of RC_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: RC_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DC_1AxiomaticDerivationAxiomatic derivation of DC_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: DC_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DC_2AxiomaticDerivationAxiomatic derivation of DC_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: DC_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DC_3AxiomaticDerivationAxiomatic derivation of DC_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: DC_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DC_4AxiomaticDerivationAxiomatic derivation of DC_4. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: DC_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DC_5AxiomaticDerivationAxiomatic derivation of DC_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: DC_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DC_6AxiomaticDerivationAxiomatic derivation of DC_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: DC_6
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DC_7AxiomaticDerivationAxiomatic derivation of DC_7. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: DC_7
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DC_8AxiomaticDerivationAxiomatic derivation of DC_8. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: DC_8
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DC_9AxiomaticDerivationAxiomatic derivation of DC_9. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: DC_9
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DC_10AxiomaticDerivationAxiomatic derivation of DC_10. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: DC_10
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DC_11AxiomaticDerivationAxiomatic derivation of DC_11. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: DC_11
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HA_1AxiomaticDerivationAxiomatic derivation of HA_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: HA_1
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_HA_2AxiomaticDerivationAxiomatic derivation of HA_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: HA_2
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_HA_3AxiomaticDerivationAxiomatic derivation of HA_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: HA_3
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_IT_2AxiomaticDerivationAxiomatic derivation of IT_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: IT_2
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_IT_3AxiomaticDerivationAxiomatic derivation of IT_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: IT_3
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_IT_6AxiomaticDerivationAxiomatic derivation of IT_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: IT_6
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_IT_7aAxiomaticDerivationAxiomatic derivation of IT_7a. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: IT_7a
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_IT_7bAxiomaticDerivationAxiomatic derivation of IT_7b. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: IT_7b
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_IT_7cAxiomaticDerivationAxiomatic derivation of IT_7c. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: IT_7c
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_IT_7dAxiomaticDerivationAxiomatic derivation of IT_7d. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: IT_7d
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_psi_1AxiomaticDerivationAxiomatic derivation of psi_1. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: psi_1
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_psi_2AxiomaticDerivationAxiomatic derivation of psi_2. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: psi_2
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_psi_3AxiomaticDerivationAxiomatic derivation of psi_3. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: psi_3
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_psi_5AxiomaticDerivationAxiomatic derivation of psi_5. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: psi_5
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_psi_6AxiomaticDerivationAxiomatic derivation of psi_6. Holds at all quantum levels by definition of Z/(2^n)Z.
  • provesIdentity: psi_6
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_boundarySquaredZeroAxiomaticDerivationAxiomatic derivation of homology:boundarySquaredZero. Holds at all quantum levels by topological reasoning.
  • provesIdentity: boundarySquaredZero
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_psi_4AxiomaticDerivationAxiomatic derivation of homology:psi_4. Holds at all quantum levels by topological reasoning.
  • provesIdentity: psi_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_indexBridgeAxiomaticDerivationAxiomatic derivation of homology:indexBridge. Holds at all quantum levels by topological reasoning.
  • provesIdentity: indexBridge
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_coboundarySquaredZeroAxiomaticDerivationAxiomatic derivation of cohomology:coboundarySquaredZero. Holds at all quantum levels by topological reasoning.
  • provesIdentity: coboundarySquaredZero
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_deRhamDualityAxiomaticDerivationAxiomatic derivation of cohomology:deRhamDuality. Holds at all quantum levels by topological reasoning.
  • provesIdentity: deRhamDuality
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_sheafCohomologyBridgeAxiomaticDerivationAxiomatic derivation of cohomology:sheafCohomologyBridge. Holds at all quantum levels by topological reasoning.
  • provesIdentity: sheafCohomologyBridge
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_localGlobalPrincipleAxiomaticDerivationAxiomatic derivation of cohomology:localGlobalPrinciple. Holds at all quantum levels by topological reasoning.
  • provesIdentity: localGlobalPrinciple
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_surfaceSymmetryAxiomaticDerivationAxiomatic 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.
  • provesIdentity: surfaceSymmetry
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CC_1AxiomaticDerivationProof 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.
  • provesIdentity: CC_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CC_2AxiomaticDerivationProof that the ψ pipeline is monotone: each constraint application cannot increase the site deficit. Derived from the definition of the partition refinement order.
  • provesIdentity: CC_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CC_3AxiomaticDerivationProof that a CompletenessCertificate implies CompleteType: the certificate attestation is only issued when IT_7d holds, by construction of the CompletenessResolver.
  • provesIdentity: CC_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CC_4AxiomaticDerivationProof that the CompletenessAuditTrail witnessCount equals the number of CompletenessWitness records in the trail. Structural invariant of the audit accumulation protocol.
  • provesIdentity: CC_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CC_5AxiomaticDerivationProof 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).
  • provesIdentity: CC_5
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_QL_1AxiomaticDerivationUniversal 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.
  • provesIdentity: QL_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_QL_2AxiomaticDerivationUniversal proof that the ring carrier set size is exactly 2^n for all n ≥ 1. Follows from the definition of Z/(2^n)Z.
  • provesIdentity: QL_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_QL_3AxiomaticDerivationUniversal 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.
  • provesIdentity: QL_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_QL_4AxiomaticDerivationUniversal 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.
  • provesIdentity: QL_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_QL_5AxiomaticDerivationUniversal proof that canonical form rewriting terminates at all quantum levels. The rewriting system is terminating by lexicographic descent on the term complexity measure.
  • provesIdentity: QL_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_QL_6AxiomaticDerivationUniversal 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.
  • provesIdentity: QL_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_QL_7AxiomaticDerivationUniversal 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.
  • provesIdentity: QL_7
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_GR_1AxiomaticDerivationProof 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.
  • provesIdentity: GR_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_GR_2AxiomaticDerivationProof 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.
  • provesIdentity: GR_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_GR_3AxiomaticDerivationProof 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.
  • provesIdentity: GR_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_GR_4AxiomaticDerivationProof 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.
  • provesIdentity: GR_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_GR_5AxiomaticDerivationProof 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.
  • provesIdentity: GR_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_TS_1AxiomaticDerivationProof 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.
  • provesIdentity: TS_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TS_2AxiomaticDerivationProof 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.
  • provesIdentity: TS_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TS_3AxiomaticDerivationProof of synthesis monotonicity: adding a constraint never decreases the Euler characteristic of the constraint nerve. Follows from the nerve inclusion principle.
  • provesIdentity: TS_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TS_4AxiomaticDerivationProof of synthesis convergence: the TypeSynthesisResolver terminates in at most n steps. Follows from monotonicity (TS_3) and the finite site budget bound.
  • provesIdentity: TS_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TS_5AxiomaticDerivationProof of synthesis-certification duality: a SynthesizedType achieves IT_7d iff the CompletenessResolver certifies it as CompleteType. The duality follows from the shared topological criterion.
  • provesIdentity: TS_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TS_6AxiomaticDerivationProof 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.
  • provesIdentity: TS_6
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TS_7AxiomaticDerivationProof of unreachable signatures: β₀ = 0 is unreachable by any non-empty ConstrainedType. Follows from the nerve connectedness of non-empty constraint sets.
  • provesIdentity: TS_7
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_WLS_1InductiveProofProof 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.
  • provesIdentity: WLS_1
  • universalScope: true
  • verified: true
  • baseCase: prf_WLS_1_base
  • inductiveStep: prf_WLS_6
  • validForKAtLeast: 0
  • strategy: BitwiseInduction
prf_WLS_2InductiveProofProof 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.
  • provesIdentity: WLS_2
  • universalScope: true
  • verified: true
  • baseCase: prf_WLS_2_base
  • inductiveStep: prf_WLS_2_step
  • validForKAtLeast: 0
  • strategy: BitwiseInduction
prf_WLS_3InductiveProofProof of monotone lifting: basisSize(T') = basisSize(T) + 1 for trivially obstructed lifts. Follows from the minimal basis construction at Q_{n+1}.
  • provesIdentity: WLS_3
  • universalScope: true
  • verified: true
  • baseCase: prf_WLS_3_base
  • inductiveStep: prf_WLS_3_step
  • validForKAtLeast: 0
  • strategy: BitwiseInduction
prf_WLS_4InductiveProofProof 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.
  • provesIdentity: WLS_4
  • universalScope: true
  • verified: true
  • baseCase: prf_WLS_4_base
  • inductiveStep: prf_WLS_4_step
  • validForKAtLeast: 0
  • strategy: BitwiseInduction
prf_WLS_5InductiveProofProof 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.
  • provesIdentity: WLS_5
  • universalScope: true
  • verified: true
  • baseCase: prf_WLS_5_base
  • inductiveStep: prf_WLS_6
  • validForKAtLeast: 0
  • strategy: BitwiseInduction
prf_WLS_6InductiveProofProof of ψ-pipeline universality for quantum lifts: the ψ-pipeline produces a valid ChainComplex for any WittLift. Follows from the functorial construction of the chain complex.
  • provesIdentity: WLS_6
  • universalScope: true
  • verified: true
  • baseCase: prf_WLS_6_base
  • inductiveStep: prf_WLS_6_step
  • validForKAtLeast: 0
  • strategy: BitwiseInduction
prf_WLS_1_baseAxiomaticDerivationBase case for QLS_1 at Q0: lift unobstructedness holds trivially for 8-bit rings where the constraint nerve is contractible.
  • provesIdentity: WLS_1
  • universalScope: false
  • verified: true
  • strategy: Composition
prf_WLS_2_baseAxiomaticDerivationBase case for QLS_2 at Q0: obstruction localisation holds at the 8-bit level where sites are directly inspectable.
  • provesIdentity: WLS_2
  • universalScope: false
  • verified: true
  • strategy: Composition
prf_WLS_2_stepAxiomaticDerivationInductive 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}.
  • provesIdentity: WLS_2
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_WLS_3_baseAxiomaticDerivationBase case for QLS_3 at Q0: monotone lifting basis size increment holds trivially for 8-bit to 16-bit extension.
  • provesIdentity: WLS_3
  • universalScope: false
  • verified: true
  • strategy: Composition
prf_WLS_3_stepAxiomaticDerivationInductive step for QLS_3: the minimal basis construction at Q_{k+1} adds exactly one element from the trivially obstructed site.
  • provesIdentity: WLS_3
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_WLS_4_baseAxiomaticDerivationBase case for QLS_4 at Q0: spectral sequence convergence at E_{d+2} holds for 8-bit filtrations by direct computation.
  • provesIdentity: WLS_4
  • universalScope: false
  • verified: true
  • strategy: Composition
prf_WLS_4_stepAxiomaticDerivationInductive 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.
  • provesIdentity: WLS_4
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_WLS_5_baseAxiomaticDerivationBase case for QLS_5 at Q0: universallyValid identities hold in the 8-bit ring by definition of universal validity.
  • provesIdentity: WLS_5
  • universalScope: false
  • verified: true
  • strategy: Composition
prf_WLS_6_baseAxiomaticDerivationBase case for QLS_6 at Q0: the psi-pipeline produces a valid ChainComplex for 8-bit WittLifts by direct construction.
  • provesIdentity: WLS_6
  • universalScope: false
  • verified: true
  • strategy: Composition
prf_WLS_6_stepAxiomaticDerivationInductive step for QLS_6: the functorial construction of the chain complex commutes with quantum level extension.
  • provesIdentity: WLS_6
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_WT_3_baseAxiomaticDerivationBase case for QT_3: resolved basis size formula holds for chain length 1 by direct construction.
  • provesIdentity: WT_3
  • universalScope: false
  • verified: true
  • strategy: Composition
prf_WT_5_baseAxiomaticDerivationBase case for QT_5: LiftChainCertificate existence for tower height 1 follows from single-step certificate issuance.
  • provesIdentity: WT_5
  • universalScope: false
  • verified: true
  • strategy: Composition
prf_AR_5_baseAxiomaticDerivationBase case for AR_5 at Q0: greedy vs adiabatic cost difference verified by exhaustive enumeration over Z/256Z.
  • provesIdentity: AR_5
  • universalScope: false
  • verified: true
  • strategy: Simplification
prf_AR_5_stepAxiomaticDerivationInductive 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).
  • provesIdentity: AR_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_QM_6_baseAxiomaticDerivationBase case for QM_6 at Q0: amplitude index set equals monotone pinning trajectories by exhaustive trajectory enumeration over the 8-bit site lattice.
  • provesIdentity: QM_6
  • universalScope: false
  • verified: true
  • strategy: Simplification
prf_QM_6_stepAxiomaticDerivationInductive step for QM_6: monotone pinning trajectories at Q_{k+1} extend those at Q_k by the site lattice ordering (monotone extension property).
  • provesIdentity: QM_6
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_MN_1AxiomaticDerivationProof of holonomy group containment: HolonomyGroup(T) ≤ D_{2^n}. Follows from the fact that all constraint applications are dihedral group elements.
  • provesIdentity: MN_1
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_MN_2AxiomaticDerivationProof of additive flatness: additive constraints (ResidueConstraint, DepthConstraint) generate only the identity in D_{2^n}. Follows from the additive structure of the dihedral action.
  • provesIdentity: MN_2
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_MN_3AxiomaticDerivationProof of dihedral generation: neg and bnot together generate D_{2^n}. Follows from the standard presentation of the dihedral group by involutions.
  • provesIdentity: MN_3
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_MN_4AxiomaticDerivationProof 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.
  • provesIdentity: MN_4
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_MN_5AxiomaticDerivationProof of CompleteType holonomy: IT_7d (β₁ = 0) implies trivial holonomy (FlatType). Follows from MN_4 contrapositive: trivial holonomy ← β₁ = 0.
  • provesIdentity: MN_5
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_MN_6AxiomaticDerivationProof 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.
  • provesIdentity: MN_6
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_MN_7AxiomaticDerivationProof 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.
  • provesIdentity: MN_7
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_PT_1AxiomaticDerivationProof 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.
  • provesIdentity: PT_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_PT_2AxiomaticDerivationProof 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.
  • provesIdentity: PT_2
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_PT_3AxiomaticDerivationProof 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.
  • provesIdentity: PT_3
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PT_4AxiomaticDerivationProof 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).
  • provesIdentity: PT_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_ST_1AxiomaticDerivationProof 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.
  • provesIdentity: ST_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_ST_2AxiomaticDerivationProof 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.
  • provesIdentity: ST_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_GS_1AxiomaticDerivationProof of SC_1: context temperature. T_ctx(C) = freeRank(C) × ln 2 / n. Derived from TH_1 normalized per site.
  • provesIdentity: GS_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_GS_2AxiomaticDerivationProof of SC_2: saturation degree. σ(C) = (n − freeRank(C)) / n. Definitional identity.
  • provesIdentity: GS_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_GS_3AxiomaticDerivationProof of SC_3: saturation monotonicity. Corollary of SR_1 through order-reversing SC_2.
  • provesIdentity: GS_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_GS_4AxiomaticDerivationProof of SC_4: ground state equivalence. Four equivalent conditions for full saturation derived from SC_2, TH_1, SC_1.
  • provesIdentity: GS_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_GS_5AxiomaticDerivationProof of SC_5: O(1) resolution guarantee at saturation. Derived from SR_2 and FreeRank.isClosed at freeRank = 0.
  • provesIdentity: GS_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_GS_6AxiomaticDerivationProof of SC_6: pre-reduction of effective budget. Derived from session-scoped site reduction at partial saturation.
  • provesIdentity: GS_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_GS_7AxiomaticDerivationProof of SC_7: thermodynamic cooling cost. n site-closures at Landauer cost each via SR_1 + TH_4.
  • provesIdentity: GS_7
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_MS_1AxiomaticDerivationProof of MS_1: connectivity lower bound β₀ ≥ 1. Formalisation of TS_7.
  • provesIdentity: MS_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_MS_2AxiomaticDerivationProof of MS_2: Euler capacity ceiling χ ≤ n. Derived from TS_1 constraint nerve dimension bound.
  • provesIdentity: MS_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MS_3AxiomaticDerivationProof of MS_3: Betti monotonicity under constraint addition. Formalisation of TS_3.
  • provesIdentity: MS_3
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_MS_4AxiomaticDerivationProof of MS_4: level-relative achievability. Derived from WittLift construction (Amendment 29).
  • provesIdentity: MS_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_MS_5AxiomaticDerivationProof of MS_5: empirical completeness convergence. Convergence statement for verification accumulation.
  • provesIdentity: MS_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_GD_1AxiomaticDerivationProof of GD_1: geodesic condition. Dual condition from AR_1 ordering + DC_10 selection.
  • provesIdentity: GD_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_GD_2AxiomaticDerivationProof of GD_2: geodesic entropy bound. Each step on a geodesic erases exactly ln 2 nats.
  • provesIdentity: GD_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_GD_3AxiomaticDerivationProof of GD_3: total geodesic cost equals Landauer bound TH_4 with equality.
  • provesIdentity: GD_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_GD_4AxiomaticDerivationProof of GD_4: geodesic uniqueness up to step-order equivalence. Equal-J_k permutations are interchangeable.
  • provesIdentity: GD_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_GD_5AxiomaticDerivationProof of GD_5: subgeodesic detectability via step-by-step J_k check.
  • provesIdentity: GD_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_QM_1AxiomaticDerivationProof of QM_1: von Neumann–Landauer bridge. S_vN equals Landauer erasure cost at the Landauer temperature β* = ln 2.
  • provesIdentity: QM_1
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_QM_2AxiomaticDerivationProof of QM_2: measurement as site topology change. Projective collapse ≅ classical ResidueConstraint pinning.
  • provesIdentity: QM_2
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_QM_3AxiomaticDerivationProof of QM_3: superposition entropy bound. 0 ≤ S_vN ≤ ln 2 for single-site superpositions.
  • provesIdentity: QM_3
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_QM_4AxiomaticDerivationProof of QM_4: collapse idempotence. Re-measurement of a collapsed state is a no-op.
  • provesIdentity: QM_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_QM_5AxiomaticDerivationProof of QM_5: amplitude normalization (Born rule). Σ|αᵢ|² = 1 for well-formed SuperposedSiteState.
  • provesIdentity: QM_5
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_RC_6AxiomaticDerivationProof of RC_6: amplitude renormalization. Division by norm yields a normalized SuperposedSiteState.
  • provesIdentity: RC_6
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_FPM_8AxiomaticDerivationProof of FPM_8: partition exhaustiveness. The four component cardinalities sum to 2ⁿ.
  • provesIdentity: FPM_8
  • universalScope: true
  • verified: true
  • strategy: DecideQ0
prf_FPM_9AxiomaticDerivationProof of FPM_9: exterior membership criterion. x ∈ Ext(T) iff x ∉ carrier(T).
  • provesIdentity: FPM_9
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MN_8AxiomaticDerivationProof of MN_8: holonomy classification covering. Every ConstrainedType is flat xor twisted.
  • provesIdentity: MN_8
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_QL_8AxiomaticDerivationProof of QL_8: quantum level chain inverse. wittLevelPredecessor is the left inverse of nextLevel.
  • provesIdentity: QL_8
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_D_7AxiomaticDerivationProof of D_7: dihedral composition rule from the semidirect product presentation.
  • provesIdentity: D_7
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_SP_1AxiomaticDerivationProof of SP_1: classical embedding. Superposition resolution of a classical datum reduces to classical resolution.
  • provesIdentity: SP_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SP_2AxiomaticDerivationProof of SP_2: collapse–resolve commutativity. The collapse and resolve operations commute.
  • provesIdentity: SP_2
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_SP_3AxiomaticDerivationProof of SP_3: amplitude preservation. The SuperpositionResolver preserves the normalized amplitude vector.
  • provesIdentity: SP_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SP_4AxiomaticDerivationProof of SP_4: Born rule outcome probability. P(collapse to site k) = |α_k|².
  • provesIdentity: SP_4
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_PT_2aAxiomaticDerivationProof of PT_2a: product type partition tensor. Π(A × B) = PartitionProduct(Π(A), Π(B)).
  • provesIdentity: PT_2a
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_PT_2bAxiomaticDerivationProof of PT_2b: sum type partition coproduct. Π(A + B) = PartitionCoproduct(Π(A), Π(B)).
  • provesIdentity: PT_2b
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_GD_6AxiomaticDerivationProof of GD_6: geodesic predicate decomposition. isGeodesic = isAR1Ordered ∧ isDC10Selected.
  • provesIdentity: GD_6
  • universalScope: true
  • verified: true
  • strategy: Simplification
iw_beta0_boundImpossibilityWitnessImpossibility witness for MS_1: β₀ = 0 is forbidden for any non-empty ConstrainedType because the constraint nerve is always connected.
  • forbidsSignature: β₀ = 0
  • impossibilityReason: β₀ = 0 violates MS_1: constraint nerve of non-empty set is connected
  • impossibilityDomain: Pipeline
  • verified: true
  • strategy: Contradiction
iw_chi_ceilingImpossibilityWitnessImpossibility witness for MS_2: χ > n is forbidden at quantum level n. The Euler characteristic cannot exceed the quantum level.
  • forbidsSignature: χ > n
  • impossibilityReason: χ > n violates MS_2: Euler characteristic bounded by quantum level
  • impossibilityDomain: Algebraic
  • verified: true
  • strategy: Contradiction
mr_completeness_targetMorphospaceRecordMorphospace record: the IT_7d completeness target χ = n is achievable (sits at the ceiling of MS_2).
  • boundaryType: Achievable
  • verified: true
mr_connectivity_lowerMorphospaceRecordMorphospace record: the connectivity lower bound β₀ ≥ 1 marks the forbidden region from below.
  • boundaryType: Forbidden
  • verified: true
prf_WT_1InductiveProofProof of tower chain validity by induction on chain length.
  • provesIdentity: WT_1
  • universalScope: true
  • verified: true
  • baseCase: prf_WLS_1
  • inductiveStep: prf_WLS_6
  • validForKAtLeast: 0
  • strategy: BitwiseInduction
prf_WT_2AxiomaticDerivationProof of obstruction count bound: direct from QLS_2 localization.
  • provesIdentity: WT_2
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_WT_3InductiveProofProof of resolved basis size formula by induction on chain length.
  • provesIdentity: WT_3
  • universalScope: true
  • verified: true
  • baseCase: prf_WT_3_base
  • inductiveStep: prf_WLS_3
  • validForKAtLeast: 0
  • strategy: BitwiseInduction
prf_WT_4AxiomaticDerivationProof of flat tower characterization: isFlat iff trivial holonomy at every step.
  • provesIdentity: WT_4
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_WT_5InductiveProofProof of LiftChainCertificate existence by induction on tower height.
  • provesIdentity: WT_5
  • universalScope: true
  • verified: true
  • baseCase: prf_WT_5_base
  • inductiveStep: prf_WT_1
  • validForKAtLeast: 0
  • strategy: BitwiseInduction
prf_WT_6AxiomaticDerivationProof of single-step reduction: QT_3 with chainLength=1 reduces to QLS_3.
  • provesIdentity: WT_6
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_WT_7AxiomaticDerivationProof of flat chain basis size formula.
  • provesIdentity: WT_7
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_CC_PINSAxiomaticDerivationProof of CC_PINS: carry-constraint site-pinning map follows from ring carry propagation rule.
  • provesIdentity: CC_PINS
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CC_COST_SITEComputationCertificateComputation certificate for CC_COST_SITE: exhaustive enumeration at Q0 confirms |pinsSites| = popcount + 1.
  • provesIdentity: CC_COST_SITE
  • atWittLevel: W8
  • verified: true
  • strategy: Computation
prf_jsat_RRAxiomaticDerivationProof of jsat_RR: CRT joint satisfiability follows from the Chinese Remainder Theorem.
  • provesIdentity: jsat_RR
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_jsat_CRAxiomaticDerivationProof of jsat_CR: carry-residue joint satisfiability follows from the carry stopping rule and residue class intersection.
  • provesIdentity: jsat_CR
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_jsat_CCComputationCertificateComputation certificate for jsat_CC: bit-pattern exhaustive enumeration at Q0.
  • provesIdentity: jsat_CC
  • atWittLevel: W8
  • verified: true
  • strategy: Computation
prf_D_8AxiomaticDerivationProof of D_8: dihedral inverse formula follows from D_5 group presentation and D_7 composition rule.
  • provesIdentity: D_8
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_D_9AxiomaticDerivationProof of D_9: reflection order 2 follows from D_7 composition: (r^k s)(r^k s) = identity.
  • provesIdentity: D_9
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_EXP_1AxiomaticDerivationProof of EXP_1: monotone carrier characterization follows from site lattice monotonicity.
  • provesIdentity: EXP_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_EXP_2ComputationCertificateComputation certificate for EXP_2: principal filter count verified by exhaustive enumeration at Q0.
  • provesIdentity: EXP_2
  • atWittLevel: W8
  • verified: true
  • strategy: Computation
prf_EXP_3AxiomaticDerivationProof of EXP_3: SumType carrier is coproduct by definitional architectural decision.
  • provesIdentity: EXP_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_ST_3AxiomaticDerivationProof of ST_3: Euler characteristic additivity for disjoint simplicial complexes.
  • provesIdentity: ST_3
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_ST_4AxiomaticDerivationProof of ST_4: Betti number additivity via Mayer-Vietoris for disjoint union.
  • provesIdentity: ST_4
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_ST_5AxiomaticDerivationProof of ST_5: SumType completeness transfer follows from ST_3 + ST_4 + IT_7d.
  • provesIdentity: ST_5
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_TS_8InductiveProofInductive proof of TS_8: minimum constraint count for beta_1 = k is 2k + 1. Base case at k=1 requires 3 mutually overlapping constraints.
  • provesIdentity: TS_8
  • universalScope: true
  • verified: true
  • baseCase: prf_HA_1
  • inductiveStep: prf_TS_4
  • validForKAtLeast: 1
  • strategy: BitwiseInduction
prf_TS_9InductiveProofInductive proof of TS_9: TypeSynthesisResolver terminates in at most 2^n steps. Base case at n=1 has 2 constraint combinations.
  • provesIdentity: TS_9
  • universalScope: true
  • verified: true
  • baseCase: prf_TS_1
  • inductiveStep: prf_TS_4
  • validForKAtLeast: 1
  • strategy: BitwiseInduction
prf_TS_10AxiomaticDerivationProof of TS_10: ForbiddenSignature membership follows from exhaustive enumeration bound.
  • provesIdentity: TS_10
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_WT_8AxiomaticDerivationProof of QT_8: ObstructionChain length bound follows from QLS_2 and spectral sequence convergence.
  • provesIdentity: WT_8
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_WT_9AxiomaticDerivationProof of QT_9: TowerCompletenessResolver termination follows from finite chain length and QT_8 bound.
  • provesIdentity: WT_9
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_COEFF_1AxiomaticDerivationProof of COEFF_1: Z/2Z coefficient ring is definitional, consistent with MN_7.
  • provesIdentity: COEFF_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_GO_1AxiomaticDerivationProof of GO_1: cohomology killing lemma for GluingObstruction feedback.
  • provesIdentity: GO_1
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_GR_6AxiomaticDerivationProof of SR_6: saturation re-entry free count follows from SR_1 monotone accumulation and SC_2.
  • provesIdentity: GR_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_GR_7AxiomaticDerivationProof of SR_7: saturation degree degradation follows from SC_2 definition and SR_1 monotonicity.
  • provesIdentity: GR_7
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_QM_6InductiveProofInductive 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.
  • provesIdentity: QM_6
  • universalScope: true
  • verified: true
  • baseCase: prf_QM_6_base
  • inductiveStep: prf_QM_6_step
  • validForKAtLeast: 0
  • strategy: BitwiseInduction
prf_CIC_1AxiomaticDerivationProof of CIC_1: TransformCertificate issuance coverage.
  • provesIdentity: CIC_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CIC_2AxiomaticDerivationProof of CIC_2: IsometryCertificate issuance coverage.
  • provesIdentity: CIC_2
  • universalScope: true
  • verified: true
  • strategy: GroupPresentation
prf_CIC_3AxiomaticDerivationProof of CIC_3: InvolutionCertificate issuance coverage.
  • provesIdentity: CIC_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CIC_4AxiomaticDerivationProof of CIC_4: GroundingCertificate issuance coverage.
  • provesIdentity: CIC_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CIC_5AxiomaticDerivationProof of CIC_5: GeodesicCertificate issuance coverage.
  • provesIdentity: CIC_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CIC_6AxiomaticDerivationProof of CIC_6: MeasurementCertificate issuance coverage.
  • provesIdentity: CIC_6
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_CIC_7AxiomaticDerivationAxiomatic derivation of CIC_7: BornRuleVerification issuance coverage. Follows by composition from corrected OA_4 (product formula chain) and QM_5 (amplitude normalization).
  • provesIdentity: CIC_7
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_GC_1AxiomaticDerivationProof of GC_1: GroundingCertificate issuance coverage.
  • provesIdentity: GC_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_GR_8AxiomaticDerivationProof of SR_8: session composition tower consistency.
  • provesIdentity: GR_8
  • universalScope: false
  • verified: true
  • strategy: RingAxiom
prf_GR_9AxiomaticDerivationProof of SR_9: ContextLease site disjointness.
  • provesIdentity: GR_9
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_GR_10AxiomaticDerivationProof of SR_10: ExecutionPolicy confluence.
  • provesIdentity: GR_10
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MC_1AxiomaticDerivationProof of MC_1: lease partition conserves total budget.
  • provesIdentity: MC_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MC_2AxiomaticDerivationProof of MC_2: per-lease binding monotonicity.
  • provesIdentity: MC_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MC_3AxiomaticDerivationProof of MC_3: composition freeRank inclusion-exclusion.
  • provesIdentity: MC_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MC_4AxiomaticDerivationProof of MC_4: disjoint-lease composition additivity.
  • provesIdentity: MC_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MC_5AxiomaticDerivationProof of MC_5: policy-invariant final binding set.
  • provesIdentity: MC_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MC_6AxiomaticDerivationProof of MC_6: full lease coverage implies composed saturation.
  • provesIdentity: MC_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MC_7AxiomaticDerivationProof of MC_7: distributed O(1) resolution.
  • provesIdentity: MC_7
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_MC_8AxiomaticDerivationProof of MC_8: parallelism bound on per-session resolution work.
  • provesIdentity: MC_8
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_WC_1AxiomaticDerivationAxiomatic derivation of WC_1: Witt coordinate = bit coordinate at p=2.
  • provesIdentity: WC_1
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_WC_2AxiomaticDerivationAxiomatic derivation of WC_2: Witt sum correction = carry.
  • provesIdentity: WC_2
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_WC_3AxiomaticDerivationAxiomatic derivation of WC_3: carry recurrence = Witt polynomial recurrence.
  • provesIdentity: WC_3
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_WC_4AxiomaticDerivationAxiomatic derivation of WC_4: δ-correction = single-level carry.
  • provesIdentity: WC_4
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_WC_5AxiomaticDerivationAxiomatic derivation of WC_5: LiftObstruction = δ nonvanishing.
  • provesIdentity: WC_5
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_WC_6AxiomaticDerivationAxiomatic derivation of WC_6: metric discrepancy = Witt defect.
  • provesIdentity: WC_6
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_WC_7AxiomaticDerivationAxiomatic derivation of WC_7: D_1 = Witt truncation order.
  • provesIdentity: WC_7
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_WC_8AxiomaticDerivationAxiomatic derivation of WC_8: D_3 = Witt-Burnside conjugation.
  • provesIdentity: WC_8
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_WC_9AxiomaticDerivationAxiomatic derivation of WC_9: D_4 = reflection composition.
  • provesIdentity: WC_9
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_WC_10AxiomaticDerivationAxiomatic derivation of WC_10: Frobenius = identity on W_n(F_2).
  • provesIdentity: WC_10
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_WC_11AxiomaticDerivationAxiomatic derivation of WC_11: Verschiebung = doubling.
  • provesIdentity: WC_11
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_WC_12AxiomaticDerivationAxiomatic derivation of WC_12: δ = squaring defect / 2.
  • provesIdentity: WC_12
  • universalScope: true
  • verified: true
  • strategy: BitwiseInduction
prf_OA_1AxiomaticDerivationAxiomatic derivation of OA_1: Ostrowski product formula at p=2.
  • provesIdentity: OA_1
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_OA_2AxiomaticDerivationAxiomatic derivation of OA_2: crossing cost = ln 2.
  • provesIdentity: OA_2
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_OA_3AxiomaticDerivationAxiomatic derivation of OA_3: Landauer cost grounding via product formula.
  • provesIdentity: OA_3
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_OA_4AxiomaticDerivationAxiomatic 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.
  • provesIdentity: OA_4
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_OA_5AxiomaticDerivationAxiomatic derivation of OA_5: entropy per δ-level = crossing cost.
  • provesIdentity: OA_5
  • universalScope: true
  • verified: true
  • strategy: ProductFormula
prf_HT_1AxiomaticDerivationAxiomatic derivation of HT_1: the constraint nerve satisfies the Kan extension condition.
  • provesIdentity: HT_1
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_HT_2AxiomaticDerivationAxiomatic derivation of HT_2: path components recover Betti number β₀.
  • provesIdentity: HT_2
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_HT_3AxiomaticDerivationAxiomatic derivation of HT_3: π₁ factors through HolonomyGroup.
  • provesIdentity: HT_3
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_HT_4AxiomaticDerivationAxiomatic derivation of HT_4: higher homotopy groups vanish above dimension.
  • provesIdentity: HT_4
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_HT_5AxiomaticDerivationAxiomatic derivation of HT_5: 1-truncation determines flat/twisted classification.
  • provesIdentity: HT_5
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_HT_6AxiomaticDerivationAxiomatic derivation of HT_6: trivial k-invariants imply spectral collapse.
  • provesIdentity: HT_6
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_HT_7AxiomaticDerivationAxiomatic derivation of HT_7: Whitehead product detects lift obstructions.
  • provesIdentity: HT_7
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_HT_8AxiomaticDerivationAxiomatic derivation of HT_8: Hurewicz isomorphism for first non-vanishing group.
  • provesIdentity: HT_8
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_psi_7AxiomaticDerivationAxiomatic derivation of ψ_7: KanComplex to PostnikovTower functor.
  • provesIdentity: psi_7
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_psi_8AxiomaticDerivationAxiomatic derivation of ψ_8: PostnikovTower to HomotopyGroups extraction.
  • provesIdentity: psi_8
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_psi_9AxiomaticDerivationAxiomatic derivation of ψ_9: HomotopyGroups to KInvariants computation.
  • provesIdentity: psi_9
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HP_1AxiomaticDerivationAxiomatic derivation of HP_1: pipeline composition ψ_7 ∘ ψ_1.
  • provesIdentity: HP_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HP_2AxiomaticDerivationAxiomatic derivation of HP_2: homotopy extraction agrees with homology on truncation.
  • provesIdentity: HP_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HP_3AxiomaticDerivationAxiomatic derivation of HP_3: ψ_9 detects QLS_4 convergence.
  • provesIdentity: HP_3
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_HP_4AxiomaticDerivationAxiomatic derivation of HP_4: HomotopyResolver complexity bound.
  • provesIdentity: HP_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_MD_1AxiomaticDerivationAxiomatic derivation of MD_1: moduli dimension equals basis cardinality.
  • provesIdentity: MD_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MD_2AxiomaticDerivationAxiomatic derivation of MD_2: automorphism group is subgroup of D_{2^n}.
  • provesIdentity: MD_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MD_3AxiomaticDerivationAxiomatic derivation of MD_3: first-order deformations parameterize tangent space.
  • provesIdentity: MD_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MD_4AxiomaticDerivationAxiomatic derivation of MD_4: obstruction space equals LiftObstruction.
  • provesIdentity: MD_4
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_MD_5AxiomaticDerivationAxiomatic derivation of MD_5: FlatType stratum is open (codimension 0).
  • provesIdentity: MD_5
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_MD_6AxiomaticDerivationAxiomatic derivation of MD_6: TwistedType strata have codimension at least 1.
  • provesIdentity: MD_6
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_MD_7AxiomaticDerivationAxiomatic derivation of MD_7: versal deformation exists when unobstructed.
  • provesIdentity: MD_7
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MD_8AxiomaticDerivationAxiomatic derivation of MD_8: completeness-preserving iff obstruction vanishes along path.
  • provesIdentity: MD_8
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_MD_9AxiomaticDerivationAxiomatic derivation of MD_9: tower map site dimension is 1 when unobstructed.
  • provesIdentity: MD_9
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_MD_10AxiomaticDerivationAxiomatic derivation of MD_10: tower map site empty iff twisted at every level.
  • provesIdentity: MD_10
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_MR_1AxiomaticDerivationAxiomatic derivation of MR_1: moduli resolver agrees with MorphospaceBoundary.
  • provesIdentity: MR_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MR_2AxiomaticDerivationAxiomatic derivation of MR_2: stratification record is complete.
  • provesIdentity: MR_2
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_MR_3AxiomaticDerivationAxiomatic derivation of MR_3: moduli resolver complexity bound.
  • provesIdentity: MR_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_MR_4AxiomaticDerivationAxiomatic derivation of MR_4: moduli-morphospace consistency.
  • provesIdentity: MR_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CY_1AxiomaticDerivationAxiomatic derivation of CY_1: carry generation condition.
  • provesIdentity: CY_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CY_2AxiomaticDerivationAxiomatic derivation of CY_2: carry propagation condition.
  • provesIdentity: CY_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CY_3AxiomaticDerivationAxiomatic derivation of CY_3: carry kill condition.
  • provesIdentity: CY_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CY_4AxiomaticDerivationAxiomatic derivation of CY_4: d_Δ as carry–Hamming discrepancy.
  • provesIdentity: CY_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CY_5AxiomaticDerivationAxiomatic derivation of CY_5: optimal encoding theorem.
  • provesIdentity: CY_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CY_6AxiomaticDerivationAxiomatic derivation of CY_6: site ordering theorem.
  • provesIdentity: CY_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CY_7AxiomaticDerivationAxiomatic derivation of CY_7: carry lookahead via prefix computation.
  • provesIdentity: CY_7
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_BM_1AxiomaticDerivationAxiomatic derivation of BM_1: saturation metric definition.
  • provesIdentity: BM_1
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_BM_2AxiomaticDerivationAxiomatic derivation of BM_2: Euler characteristic formula.
  • provesIdentity: BM_2
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_BM_3AxiomaticDerivationAxiomatic derivation of BM_3: index theorem linking all six metrics.
  • provesIdentity: BM_3
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_BM_4AxiomaticDerivationAxiomatic derivation of BM_4: Jacobian vanishes on pinned sites.
  • provesIdentity: BM_4
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_BM_5AxiomaticDerivationAxiomatic derivation of BM_5: d_delta equals Witt defect.
  • provesIdentity: BM_5
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_BM_6AxiomaticDerivationAxiomatic derivation of BM_6: metric composition tower.
  • provesIdentity: BM_6
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_GL_1AxiomaticDerivationAxiomatic derivation of GL_1: σ as lower adjoint.
  • provesIdentity: GL_1
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_GL_2AxiomaticDerivationAxiomatic derivation of GL_2: r as complement of upper adjoint.
  • provesIdentity: GL_2
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_GL_3AxiomaticDerivationAxiomatic derivation of GL_3: completeness as Galois fixpoint.
  • provesIdentity: GL_3
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_GL_4AxiomaticDerivationAxiomatic derivation of GL_4: Galois order reversal.
  • provesIdentity: GL_4
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_NV_1AxiomaticDerivationAxiomatic derivation of NV_1: nerve additivity for disjoint domains.
  • provesIdentity: NV_1
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_NV_2AxiomaticDerivationAxiomatic derivation of NV_2: Mayer–Vietoris for constraint nerves.
  • provesIdentity: NV_2
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_NV_3AxiomaticDerivationAxiomatic derivation of NV_3: Betti number bounded change.
  • provesIdentity: NV_3
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_NV_4AxiomaticDerivationAxiomatic derivation of NV_4: accumulation monotonicity.
  • provesIdentity: NV_4
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_SD_1AxiomaticDerivationAxiomatic derivation of SD_1: scalar grounding identity.
  • provesIdentity: SD_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_SD_2AxiomaticDerivationAxiomatic derivation of SD_2: symbol grounding identity.
  • provesIdentity: SD_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_SD_3AxiomaticDerivationAxiomatic derivation of SD_3: sequence free monoid identity.
  • provesIdentity: SD_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_SD_4AxiomaticDerivationAxiomatic derivation of SD_4: tuple site additivity.
  • provesIdentity: SD_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_SD_5AxiomaticDerivationAxiomatic derivation of SD_5: graph nerve equality.
  • provesIdentity: SD_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_SD_6AxiomaticDerivationAxiomatic derivation of SD_6: set permutation invariance.
  • provesIdentity: SD_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_SD_7AxiomaticDerivationAxiomatic derivation of SD_7: tree acyclicity constraint.
  • provesIdentity: SD_7
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_SD_8AxiomaticDerivationAxiomatic derivation of SD_8: table functorial decomposition.
  • provesIdentity: SD_8
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_DD_1AxiomaticDerivationAxiomatic derivation of DD_1: dispatch determinism.
  • provesIdentity: DD_1
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_DD_2AxiomaticDerivationAxiomatic derivation of DD_2: dispatch coverage.
  • provesIdentity: DD_2
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PI_1AxiomaticDerivationAxiomatic derivation of PI_1: inference idempotence.
  • provesIdentity: PI_1
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PI_2AxiomaticDerivationAxiomatic derivation of PI_2: inference soundness.
  • provesIdentity: PI_2
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PI_3AxiomaticDerivationAxiomatic derivation of PI_3: inference composition.
  • provesIdentity: PI_3
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PI_4AxiomaticDerivationAxiomatic derivation of PI_4: inference complexity.
  • provesIdentity: PI_4
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PI_5AxiomaticDerivationAxiomatic derivation of PI_5: inference coherence.
  • provesIdentity: PI_5
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PA_1AxiomaticDerivationAxiomatic derivation of PA_1: accumulation permutation invariance.
  • provesIdentity: PA_1
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PA_2AxiomaticDerivationAxiomatic derivation of PA_2: accumulation monotonicity.
  • provesIdentity: PA_2
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PA_3AxiomaticDerivationAxiomatic derivation of PA_3: accumulation soundness.
  • provesIdentity: PA_3
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PA_4AxiomaticDerivationAxiomatic derivation of PA_4: accumulation base preservation.
  • provesIdentity: PA_4
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PA_5AxiomaticDerivationAxiomatic derivation of PA_5: accumulation identity element.
  • provesIdentity: PA_5
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PL_1AxiomaticDerivationAxiomatic derivation of PL_1: lease disjointness.
  • provesIdentity: PL_1
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PL_2AxiomaticDerivationAxiomatic derivation of PL_2: lease conservation.
  • provesIdentity: PL_2
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PL_3AxiomaticDerivationAxiomatic derivation of PL_3: lease coverage.
  • provesIdentity: PL_3
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PK_1AxiomaticDerivationAxiomatic derivation of PK_1: composition validity.
  • provesIdentity: PK_1
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PK_2AxiomaticDerivationAxiomatic derivation of PK_2: distributed resolution.
  • provesIdentity: PK_2
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PP_1AxiomaticDerivationAxiomatic derivation of PP_1: pipeline unification.
  • provesIdentity: PP_1
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_PE_1AxiomaticDerivationAxiomatic derivation of PE_1: state initialization.
  • provesIdentity: PE_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PE_2AxiomaticDerivationAxiomatic derivation of PE_2: resolver dispatch.
  • provesIdentity: PE_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PE_3AxiomaticDerivationAxiomatic derivation of PE_3: ring address grounding.
  • provesIdentity: PE_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PE_4AxiomaticDerivationAxiomatic derivation of PE_4: constraint resolution.
  • provesIdentity: PE_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PE_5AxiomaticDerivationAxiomatic derivation of PE_5: consistent accumulation.
  • provesIdentity: PE_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PE_6AxiomaticDerivationAxiomatic derivation of PE_6: coherent extraction.
  • provesIdentity: PE_6
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PE_7AxiomaticDerivationAxiomatic derivation of PE_7: full pipeline composition.
  • provesIdentity: PE_7
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PM_1AxiomaticDerivationAxiomatic derivation of PM_1: phase rotation.
  • provesIdentity: PM_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PM_2AxiomaticDerivationAxiomatic derivation of PM_2: phase gate check.
  • provesIdentity: PM_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PM_3AxiomaticDerivationAxiomatic derivation of PM_3: conjugate rollback.
  • provesIdentity: PM_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PM_4AxiomaticDerivationAxiomatic derivation of PM_4: rollback involution.
  • provesIdentity: PM_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PM_5AxiomaticDerivationAxiomatic derivation of PM_5: epoch saturation preservation.
  • provesIdentity: PM_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PM_6AxiomaticDerivationAxiomatic derivation of PM_6: service window context.
  • provesIdentity: PM_6
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PM_7AxiomaticDerivationAxiomatic derivation of PM_7: machine determinism.
  • provesIdentity: PM_7
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_ER_1AxiomaticDerivationAxiomatic derivation of ER_1: guard satisfaction.
  • provesIdentity: ER_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_ER_2AxiomaticDerivationAxiomatic derivation of ER_2: effect atomicity.
  • provesIdentity: ER_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_ER_3AxiomaticDerivationAxiomatic derivation of ER_3: guard purity.
  • provesIdentity: ER_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_ER_4AxiomaticDerivationAxiomatic derivation of ER_4: intra-stage commutativity.
  • provesIdentity: ER_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_EA_1AxiomaticDerivationAxiomatic derivation of EA_1: epoch boundary reset.
  • provesIdentity: EA_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_EA_2AxiomaticDerivationAxiomatic derivation of EA_2: saturation monotonicity.
  • provesIdentity: EA_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_EA_3AxiomaticDerivationAxiomatic derivation of EA_3: service window bound.
  • provesIdentity: EA_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_EA_4AxiomaticDerivationAxiomatic derivation of EA_4: epoch admission exclusivity.
  • provesIdentity: EA_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OE_1AxiomaticDerivationAxiomatic derivation of OE_1: stage fusion.
  • provesIdentity: OE_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OE_2AxiomaticDerivationAxiomatic derivation of OE_2: effect commutativity.
  • provesIdentity: OE_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OE_3AxiomaticDerivationAxiomatic derivation of OE_3: lease parallelism.
  • provesIdentity: OE_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OE_4aAxiomaticDerivationAxiomatic derivation of OE_4a: fusion semantics preservation.
  • provesIdentity: OE_4a
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OE_4bAxiomaticDerivationAxiomatic derivation of OE_4b: commutation outcome preservation.
  • provesIdentity: OE_4b
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_OE_4cAxiomaticDerivationAxiomatic derivation of OE_4c: parallelism coverage preservation.
  • provesIdentity: OE_4c
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CS_1AxiomaticDerivationAxiomatic derivation of CS_1: bounded stage cost.
  • provesIdentity: CS_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CS_2AxiomaticDerivationAxiomatic derivation of CS_2: additive pipeline cost.
  • provesIdentity: CS_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CS_3AxiomaticDerivationAxiomatic derivation of CS_3: bounded rollback cost.
  • provesIdentity: CS_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CS_4AxiomaticDerivationAxiomatic derivation of CS_4: constant preflight cost.
  • provesIdentity: CS_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CS_5AxiomaticDerivationAxiomatic derivation of CS_5: total reduction cost bound.
  • provesIdentity: CS_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_FA_1AxiomaticDerivationAxiomatic derivation of FA_1: query liveness.
  • provesIdentity: FA_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_FA_2AxiomaticDerivationAxiomatic derivation of FA_2: no starvation.
  • provesIdentity: FA_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_FA_3AxiomaticDerivationAxiomatic derivation of FA_3: fair lease allocation.
  • provesIdentity: FA_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SW_1AxiomaticDerivationAxiomatic derivation of SW_1: memory boundedness.
  • provesIdentity: SW_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SW_2AxiomaticDerivationAxiomatic derivation of SW_2: saturation invariance.
  • provesIdentity: SW_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SW_3AxiomaticDerivationAxiomatic derivation of SW_3: eviction releases resources.
  • provesIdentity: SW_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_SW_4AxiomaticDerivationAxiomatic derivation of SW_4: non-empty window.
  • provesIdentity: SW_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_LS_1AxiomaticDerivationAxiomatic derivation of LS_1: suspension preserves pinned state.
  • provesIdentity: LS_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_LS_2AxiomaticDerivationAxiomatic derivation of LS_2: expiry releases resources.
  • provesIdentity: LS_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_LS_3AxiomaticDerivationAxiomatic derivation of LS_3: checkpoint restore idempotence.
  • provesIdentity: LS_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_LS_4AxiomaticDerivationAxiomatic derivation of LS_4: suspend-resume round-trip.
  • provesIdentity: LS_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TJ_1AxiomaticDerivationAxiomatic derivation of TJ_1: AllOrNothing rollback.
  • provesIdentity: TJ_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TJ_2AxiomaticDerivationAxiomatic derivation of TJ_2: BestEffort partial commit.
  • provesIdentity: TJ_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_TJ_3AxiomaticDerivationAxiomatic derivation of TJ_3: epoch-scoped atomicity.
  • provesIdentity: TJ_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AP_1AxiomaticDerivationAxiomatic derivation of AP_1: saturation monotonicity.
  • provesIdentity: AP_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AP_2AxiomaticDerivationAxiomatic derivation of AP_2: quality improvement.
  • provesIdentity: AP_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_AP_3AxiomaticDerivationAxiomatic derivation of AP_3: deferred query liveness.
  • provesIdentity: AP_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_EC_1AxiomaticDerivationAxiomatic derivation of EC_1: phase half-turn convergence.
  • provesIdentity: EC_1
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_EC_2AxiomaticDerivationAxiomatic derivation of EC_2: conjugate involution.
  • provesIdentity: EC_2
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_EC_3AxiomaticDerivationAxiomatic derivation of EC_3: pairwise commutator convergence.
  • provesIdentity: EC_3
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_EC_4AxiomaticDerivationAxiomatic derivation of EC_4: triple associator convergence.
  • provesIdentity: EC_4
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_EC_4aAxiomaticDerivationAxiomatic derivation of EC_4a: associator monotonicity.
  • provesIdentity: EC_4a
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_EC_4bAxiomaticDerivationAxiomatic derivation of EC_4b: associator finiteness.
  • provesIdentity: EC_4b
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_EC_4cAxiomaticDerivationAxiomatic derivation of EC_4c: vanishing implies associativity.
  • provesIdentity: EC_4c
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_EC_5AxiomaticDerivationAxiomatic derivation of EC_5: Adams termination.
  • provesIdentity: EC_5
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_DA_1AxiomaticDerivationAxiomatic derivation of DA_1: Cayley-Dickson R→C.
  • provesIdentity: DA_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_DA_2AxiomaticDerivationAxiomatic derivation of DA_2: Cayley-Dickson C→H.
  • provesIdentity: DA_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_DA_3AxiomaticDerivationAxiomatic derivation of DA_3: Cayley-Dickson H→O.
  • provesIdentity: DA_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_DA_4AxiomaticDerivationAxiomatic derivation of DA_4: Adams dimension restriction.
  • provesIdentity: DA_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_DA_5AxiomaticDerivationAxiomatic derivation of DA_5: convergence-level algebra correspondence.
  • provesIdentity: DA_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_DA_6AxiomaticDerivationAxiomatic derivation of DA_6: commutator-commutativity equivalence.
  • provesIdentity: DA_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_DA_7AxiomaticDerivationAxiomatic derivation of DA_7: associator-associativity equivalence.
  • provesIdentity: DA_7
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_IN_1AxiomaticDerivationAxiomatic derivation of IN_1: interaction cost.
  • provesIdentity: IN_1
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_IN_2AxiomaticDerivationAxiomatic derivation of IN_2: disjoint leases commute.
  • provesIdentity: IN_2
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_IN_3AxiomaticDerivationAxiomatic derivation of IN_3: shared sites nonzero commutator.
  • provesIdentity: IN_3
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_IN_4AxiomaticDerivationAxiomatic derivation of IN_4: negotiation convergence.
  • provesIdentity: IN_4
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_IN_5AxiomaticDerivationAxiomatic derivation of IN_5: commutative subspace selection.
  • provesIdentity: IN_5
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_IN_6AxiomaticDerivationAxiomatic derivation of IN_6: pairwise outcome space.
  • provesIdentity: IN_6
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_IN_7AxiomaticDerivationAxiomatic derivation of IN_7: associative subalgebra selection.
  • provesIdentity: IN_7
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_IN_8AxiomaticDerivationAxiomatic derivation of IN_8: nerve Betti coupling bound.
  • provesIdentity: IN_8
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_IN_9AxiomaticDerivationAxiomatic derivation of IN_9: Betti-disagreement associator bound.
  • provesIdentity: IN_9
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_AS_1AxiomaticDerivationAxiomatic derivation of AS_1: δ-ι-κ non-associativity.
  • provesIdentity: AS_1
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_AS_2AxiomaticDerivationAxiomatic derivation of AS_2: ι-α-λ non-associativity.
  • provesIdentity: AS_2
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_AS_3AxiomaticDerivationAxiomatic derivation of AS_3: λ-κ-δ non-associativity.
  • provesIdentity: AS_3
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_AS_4AxiomaticDerivationAxiomatic derivation of AS_4: non-associativity root cause.
  • provesIdentity: AS_4
  • universalScope: true
  • verified: true
  • strategy: Composition
prf_MO_1AxiomaticDerivationAxiomatic derivation of MO_1: monoidal unit law.
  • provesIdentity: MO_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MO_2AxiomaticDerivationAxiomatic derivation of MO_2: monoidal associativity.
  • provesIdentity: MO_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MO_3AxiomaticDerivationAxiomatic derivation of MO_3: certificate composition.
  • provesIdentity: MO_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MO_4AxiomaticDerivationAxiomatic derivation of MO_4: saturation monotonicity.
  • provesIdentity: MO_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_MO_5AxiomaticDerivationAxiomatic derivation of MO_5: residual monotonicity.
  • provesIdentity: MO_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_OP_1AxiomaticDerivationAxiomatic derivation of OP_1: site additivity.
  • provesIdentity: OP_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_OP_2AxiomaticDerivationAxiomatic derivation of OP_2: grounding distributivity.
  • provesIdentity: OP_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_OP_3AxiomaticDerivationAxiomatic derivation of OP_3: d_Δ decomposition.
  • provesIdentity: OP_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_OP_4AxiomaticDerivationAxiomatic derivation of OP_4: tabular data decomposition.
  • provesIdentity: OP_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_OP_5AxiomaticDerivationAxiomatic derivation of OP_5: hierarchical data structure.
  • provesIdentity: OP_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FX_1AxiomaticDerivationAxiomatic derivation of FX_1: pinning site budget decrement.
  • provesIdentity: FX_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FX_2AxiomaticDerivationAxiomatic derivation of FX_2: unbinding site budget increment.
  • provesIdentity: FX_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FX_3AxiomaticDerivationAxiomatic derivation of FX_3: phase budget invariance.
  • provesIdentity: FX_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FX_4AxiomaticDerivationAxiomatic derivation of FX_4: disjoint commutativity.
  • provesIdentity: FX_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FX_5AxiomaticDerivationAxiomatic derivation of FX_5: composite delta additivity.
  • provesIdentity: FX_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FX_6AxiomaticDerivationAxiomatic derivation of FX_6: reversible inverse.
  • provesIdentity: FX_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FX_7AxiomaticDerivationAxiomatic derivation of FX_7: external shape compliance.
  • provesIdentity: FX_7
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PR_1AxiomaticDerivationAxiomatic derivation of PR_1: predicate totality.
  • provesIdentity: PR_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PR_2AxiomaticDerivationAxiomatic derivation of PR_2: predicate purity.
  • provesIdentity: PR_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PR_3AxiomaticDerivationAxiomatic derivation of PR_3: deterministic dispatch.
  • provesIdentity: PR_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PR_4AxiomaticDerivationAxiomatic derivation of PR_4: deterministic match.
  • provesIdentity: PR_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PR_5AxiomaticDerivationAxiomatic derivation of PR_5: typed guard transition.
  • provesIdentity: PR_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CG_1AxiomaticDerivationAxiomatic derivation of CG_1: typed entry guard.
  • provesIdentity: CG_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CG_2AxiomaticDerivationAxiomatic derivation of CG_2: typed exit guard with effect.
  • provesIdentity: CG_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DIS_1AxiomaticDerivationAxiomatic derivation of DIS_1: exhaustive exclusive table.
  • provesIdentity: DIS_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_DIS_2AxiomaticDerivationAxiomatic derivation of DIS_2: deterministic resolver selection.
  • provesIdentity: DIS_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_PAR_1AxiomaticDerivationAxiomatic derivation of PAR_1: disjoint commutativity.
  • provesIdentity: PAR_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_PAR_2AxiomaticDerivationAxiomatic derivation of PAR_2: delta additivity.
  • provesIdentity: PAR_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_PAR_3AxiomaticDerivationAxiomatic derivation of PAR_3: exhaustive partitioning.
  • provesIdentity: PAR_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_PAR_4AxiomaticDerivationAxiomatic derivation of PAR_4: interleaving invariance.
  • provesIdentity: PAR_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_PAR_5AxiomaticDerivationAxiomatic derivation of PAR_5: certificate conjunction.
  • provesIdentity: PAR_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HO_1AxiomaticDerivationAxiomatic derivation of HO_1: content-addressed certification.
  • provesIdentity: HO_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_HO_2AxiomaticDerivationAxiomatic derivation of HO_2: application certification.
  • provesIdentity: HO_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HO_3AxiomaticDerivationAxiomatic derivation of HO_3: composition certification.
  • provesIdentity: HO_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_HO_4AxiomaticDerivationAxiomatic derivation of HO_4: saturation equivalence.
  • provesIdentity: HO_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_STR_1AxiomaticDerivationAxiomatic derivation of STR_1: epoch termination.
  • provesIdentity: STR_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_STR_2AxiomaticDerivationAxiomatic derivation of STR_2: saturation preservation.
  • provesIdentity: STR_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_STR_3AxiomaticDerivationAxiomatic derivation of STR_3: finite prefix computability.
  • provesIdentity: STR_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_STR_4AxiomaticDerivationAxiomatic derivation of STR_4: unfold seed initialization.
  • provesIdentity: STR_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_STR_5AxiomaticDerivationAxiomatic derivation of STR_5: continuation chaining.
  • provesIdentity: STR_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_STR_6AxiomaticDerivationAxiomatic derivation of STR_6: lease expiry budget return.
  • provesIdentity: STR_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FLR_1AxiomaticDerivationAxiomatic derivation of FLR_1: coproduct exhaustiveness.
  • provesIdentity: FLR_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FLR_2AxiomaticDerivationAxiomatic derivation of FLR_2: total computation guarantee.
  • provesIdentity: FLR_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_FLR_3AxiomaticDerivationAxiomatic derivation of FLR_3: sequential propagation.
  • provesIdentity: FLR_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FLR_4AxiomaticDerivationAxiomatic derivation of FLR_4: parallel independence.
  • provesIdentity: FLR_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_FLR_5AxiomaticDerivationAxiomatic derivation of FLR_5: recovery result.
  • provesIdentity: FLR_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_FLR_6AxiomaticDerivationAxiomatic derivation of FLR_6: conjugate rollback.
  • provesIdentity: FLR_6
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_LN_1AxiomaticDerivationAxiomatic derivation of LN_1: exact coverage.
  • provesIdentity: LN_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_LN_2AxiomaticDerivationAxiomatic derivation of LN_2: pinning effect.
  • provesIdentity: LN_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_LN_3AxiomaticDerivationAxiomatic derivation of LN_3: consumption linearity.
  • provesIdentity: LN_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_LN_4AxiomaticDerivationAxiomatic derivation of LN_4: lease budget decrement.
  • provesIdentity: LN_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_LN_5AxiomaticDerivationAxiomatic derivation of LN_5: lease expiry return.
  • provesIdentity: LN_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_LN_6AxiomaticDerivationAxiomatic derivation of LN_6: geodesic linearity.
  • provesIdentity: LN_6
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_SB_1AxiomaticDerivationAxiomatic derivation of SB_1: constraint superset.
  • provesIdentity: SB_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_SB_2AxiomaticDerivationAxiomatic derivation of SB_2: resolution subset.
  • provesIdentity: SB_2
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_SB_3AxiomaticDerivationAxiomatic derivation of SB_3: nerve sub-complex.
  • provesIdentity: SB_3
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_SB_4AxiomaticDerivationAxiomatic derivation of SB_4: covariance.
  • provesIdentity: SB_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_SB_5AxiomaticDerivationAxiomatic derivation of SB_5: contravariance.
  • provesIdentity: SB_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_SB_6AxiomaticDerivationAxiomatic derivation of SB_6: lattice depth.
  • provesIdentity: SB_6
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_BR_1AxiomaticDerivationAxiomatic derivation of BR_1: strict descent.
  • provesIdentity: BR_1
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_BR_2AxiomaticDerivationAxiomatic derivation of BR_2: depth bound.
  • provesIdentity: BR_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_BR_3AxiomaticDerivationAxiomatic derivation of BR_3: termination guarantee.
  • provesIdentity: BR_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_BR_4AxiomaticDerivationAxiomatic derivation of BR_4: structural measure.
  • provesIdentity: BR_4
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_BR_5AxiomaticDerivationAxiomatic derivation of BR_5: base predicate zero.
  • provesIdentity: BR_5
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_RG_1AxiomaticDerivationAxiomatic derivation of RG_1: nerve-determined working set.
  • provesIdentity: RG_1
  • universalScope: true
  • verified: true
  • strategy: EulerPoincare
prf_RG_2AxiomaticDerivationAxiomatic derivation of RG_2: diameter bound.
  • provesIdentity: RG_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_RG_3AxiomaticDerivationAxiomatic derivation of RG_3: addressable space bound.
  • provesIdentity: RG_3
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_RG_4AxiomaticDerivationAxiomatic derivation of RG_4: working set containment.
  • provesIdentity: RG_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_IO_1AxiomaticDerivationAxiomatic derivation of IO_1: ingest type conformance.
  • provesIdentity: IO_1
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_IO_2AxiomaticDerivationAxiomatic derivation of IO_2: emit type conformance.
  • provesIdentity: IO_2
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_IO_3AxiomaticDerivationAxiomatic derivation of IO_3: grounding validity.
  • provesIdentity: IO_3
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_IO_4AxiomaticDerivationAxiomatic derivation of IO_4: projection validity.
  • provesIdentity: IO_4
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_IO_5AxiomaticDerivationAxiomatic derivation of IO_5: non-vacuous crossing.
  • provesIdentity: IO_5
  • universalScope: true
  • verified: true
  • strategy: RingAxiom
prf_CS_6AxiomaticDerivationAxiomatic derivation of CS_6: budget solvency rejection.
  • provesIdentity: CS_6
  • universalScope: true
  • verified: true
  • strategy: Simplification
prf_CS_7AxiomaticDerivationAxiomatic derivation of CS_7: unit address computation.
  • provesIdentity: CS_7
  • universalScope: true
  • verified: true
  • strategy: RingAxiom

Related Concepts