Mathematics · proofs · software

The K-COS Method · Lean source

AxiomAudit.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

Local imports (1)

AxiomAudit.lean70 lines

Original source pathlean/AxiomAudit.lean

Skip source text

1 import KomorebiQCOS
2 
3 #check KomorebiQCOS.Enclosed
4 #print axioms KomorebiQCOS.Enclosed
5 #check KomorebiQCOS.ErrorBound
6 #print axioms KomorebiQCOS.ErrorBound
7 #check KomorebiQCOS.enclosed_order
8 #print axioms KomorebiQCOS.enclosed_order
9 #check KomorebiQCOS.enclosed_add
10 #print axioms KomorebiQCOS.enclosed_add
11 #check KomorebiQCOS.enclosed_scale
12 #print axioms KomorebiQCOS.enclosed_scale
13 #check KomorebiQCOS.enclosed_widen
14 #print axioms KomorebiQCOS.enclosed_widen
15 #check KomorebiQCOS.enclosed_intersect
16 #print axioms KomorebiQCOS.enclosed_intersect
17 #check KomorebiQCOS.errorBound_iff_enclosed
18 #print axioms KomorebiQCOS.errorBound_iff_enclosed
19 #check KomorebiQCOS.errorBound_compose
20 #print axioms KomorebiQCOS.errorBound_compose
21 #check KomorebiQCOS.errorBound_accept
22 #print axioms KomorebiQCOS.errorBound_accept
23 #check KomorebiQCOS.enclosed_positive
24 #print axioms KomorebiQCOS.enclosed_positive
25 #check KomorebiQCOS.enclosed_monotone
26 #print axioms KomorebiQCOS.enclosed_monotone
27 #check KomorebiQCOS.gramEntry
28 #print axioms KomorebiQCOS.gramEntry
29 #check KomorebiQCOS.matrixAction
30 #print axioms KomorebiQCOS.matrixAction
31 #check KomorebiQCOS.streamedAction
32 #print axioms KomorebiQCOS.streamedAction
33 #check KomorebiQCOS.quadraticForm
34 #print axioms KomorebiQCOS.quadraticForm
35 #check KomorebiQCOS.factorEnergy
36 #print axioms KomorebiQCOS.factorEnergy
37 #check KomorebiQCOS.gramEntry_empty
38 #print axioms KomorebiQCOS.gramEntry_empty
39 #check KomorebiQCOS.gramEntry_singleton
40 #print axioms KomorebiQCOS.gramEntry_singleton
41 #check KomorebiQCOS.gramEntry_symm
42 #print axioms KomorebiQCOS.gramEntry_symm
43 #check KomorebiQCOS.gramEntry_union
44 #print axioms KomorebiQCOS.gramEntry_union
45 #check KomorebiQCOS.gramEntry_reindex
46 #print axioms KomorebiQCOS.gramEntry_reindex
47 #check KomorebiQCOS.matrixAction_gram_eq_streamed
48 #print axioms KomorebiQCOS.matrixAction_gram_eq_streamed
49 #check KomorebiQCOS.matrixAction_add
50 #print axioms KomorebiQCOS.matrixAction_add
51 #check KomorebiQCOS.matrixAction_gram_union
52 #print axioms KomorebiQCOS.matrixAction_gram_union
53 #check KomorebiQCOS.streamedAction_union
54 #print axioms KomorebiQCOS.streamedAction_union
55 #check KomorebiQCOS.quadraticForm_add
56 #print axioms KomorebiQCOS.quadraticForm_add
57 #check KomorebiQCOS.quadraticForm_gram_eq_energy
58 #print axioms KomorebiQCOS.quadraticForm_gram_eq_energy
59 #check KomorebiQCOS.quadraticForm_gram_nonneg
60 #print axioms KomorebiQCOS.quadraticForm_gram_nonneg
61 #check KomorebiQCOS.quadraticForm_gram_union
62 #print axioms KomorebiQCOS.quadraticForm_gram_union
63 #check KomorebiQCOS.weightedSquares
64 #print axioms KomorebiQCOS.weightedSquares
65 #check KomorebiQCOS.weightedSquares_mono
66 #print axioms KomorebiQCOS.weightedSquares_mono
67 #check KomorebiQCOS.weightedSquares_nonneg
68 #print axioms KomorebiQCOS.weightedSquares_nonneg
69 #check KomorebiQCOS.weightedSquares_tail_imp
70 #print axioms KomorebiQCOS.weightedSquares_tail_imp

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: 4e9321d4e024b41f3d862b43e6114faf3a323aa74146eda5aa6c1b1042d38295

Original source on GitHub

Back to COS Method