feat(coq): Wave 8.4 — discharge cell600_J_off_diagonal_KO6 axiom (Strategy A) - #44
Open
gHashTag wants to merge 1 commit into
Open
feat(coq): Wave 8.4 — discharge cell600_J_off_diagonal_KO6 axiom (Strategy A)#44gHashTag wants to merge 1 commit into
gHashTag wants to merge 1 commit into
Conversation
Strategy A: define H = H_L_decomp + H_R_decomp as Coq sum type. J := cell600_J_sum_op swaps summands by pattern matching. Off-diagonal property proved by computation (reflexivity/destruct). New section KO6_HilbertDecomposition adds: - Inductive H_L_decomp, H_R_decomp - Definition cell600_H_sum, cell600_J_sum_op - Lemma cell600_J_maps_L_to_R (Qed) - Lemma cell600_J_maps_R_to_L (Qed) - Lemma cell600_J_no_L_diagonal (Qed) - Lemma cell600_J_no_R_diagonal (Qed) - Lemma cell600_J_squared_id (Qed) - Theorem cell600_J_strictly_off_diagonal (Qed) - Theorem cell600_J_off_diagonal_KO6 (Qed, was Axiom) Axiom count: 5 -> 4. Qed count: 35 -> 42. Ref: Connes 1995, J.Math.Phys. 36:6194 (DOI: 10.1063/1.531241) Ref: Chamseddine-Connes-Marcolli 2007, CMP 273:643
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Wave 8.4: KO-6 Off-Diagonal J Property — Axiom Discharged
Summary
Replaces
Axiom cell600_J_off_diagonal_KO6 : Truewith a Theorem proved viaStrategy A: explicit definitional decomposition of the Hilbert space as a Coq sum type.
Strategy A: H = H_L ⊕ H_R as Coq Sum Type
New section
KO6_HilbertDecompositionadded beforeSection Axiom1_Dimension:Inductive H_L_decomp : Type := mk_H_L : nat -> H_L_decompInductive H_R_decomp : Type := mk_H_R : nat -> H_R_decompDefinition cell600_H_sum : Type := H_L_decomp + H_R_decompDefinition cell600_J_sum_op— mapsinl (mk_H_L n) => inr (mk_H_R n)and vice versareflexivity/destructon sum typeNew Qed Proofs (7)
cell600_J_maps_L_to_Rcell600_J_maps_R_to_Lcell600_J_no_L_diagonalcell600_J_no_R_diagonalcell600_J_squared_idcell600_J_strictly_off_diagonalcell600_J_off_diagonal_KO6Metrics
AxiomcountQedcount (estimated)References
Remaining Axioms (4)
axiom4_commutator_vanishing— [a, JbJ^-1] = 0axiom_first_order_MATH_TODO— First-order conditionaxiom_orientation_hochschild— Hochschild cycleaxiom_poincare_nondegeneracy— K-theory pairing